Modularity is an important pragmatic aspect of semantic<br />descriptions. In denotational semantics, the issue of modularity has <br />received much attention, and appropriate abstractions have been <br />introduced, so that definitions of semantic functions may be independent of<br />the details of how computations are modeled. In structural operational<br />semantics (SOS), however, this issue has largely been neglected, and<br />SOS descriptions of programming languages typically exhibit rather poor<br />modularity| - for instance, extending the described language may entail<br />a complete reformulation of the description of the original constructs.<br />A proposal has recently been made for a modular approach to SOS, called<br />MSOS. The basic definitions of the Modular SOS framework are recalled<br />here, but the reader is referred to other papers for a full introduction.<br />This paper focuses on illustrating the applicability of Modular SOS, by<br />using it to give a description of a sublanguage of Concurrent ML (CML);<br />the transition rules for the purely functional constructs do not have to be<br />reformulated at all when adding references and/or processes. The paper<br />concludes by comparing the MSOS description with previous operational<br />descriptions of similar languages.<br />The reader is assumed to be familiar with conventional SOS, with the<br />concepts of functional programming languages such as Standard ML, and<br />with fundamental notions of concurrency.
Functional programming languages for verification tools: a comparison of Standard ML and Haskell