A Modular SOS for ML Concurrency Primitives

Modularity is an important pragmatic aspect of semantic descriptions. In denotational semantics, the issue of modularity has received much attention, and appropriate abstractions have been introduced, so that definitions of semantic functions may be independent of the details of how computations are modelled. In structural operational semantics (SOS), however, this issue has largely been neglected, and SOS descriptions of programming languages typically exhibit rather poor modularity. A proposal has recently been made for a modular approach to SOS, called MSOS. This paper focusses on illustrating the applicability of MSOS, by using it to give a description of a sublanguage of Concurrent ML (CML); the transition rules for the purely functional constructs do not have to be reformulated at all when adding references and/or processes. The paper concludes by comparing the MSOS description with previous operational descriptions of similar languages. 1 Modular SOS In the conventional SOS fra..