|
Foundations of Modular SOS
Peter D. Mosses December 1999 |
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. Available as PostScript, PDF, DVI. |