Foundations of Modular SOS

Abstract

A novel form of labelled transition system is proposed, where
the labels are the arrows of a category, and adjacent labels in computations
are required to be composable. Such transition systems provide the
foundations for modular SOS descriptions of programming languages.
Three fundamental ways of transforming label categories, analogous to
monad transformers, are provided, and it is shown that their applications
preserve computations in modular SOS. The approach is illustrated with
fragments taken from a modular SOS for ML concurrency primitives.