A Modular SOS for ML Concurrency Primitives
Peter D. Mosses December 1999 |
Abstract:
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--for
instance, extending the described language may entail a complete
reformulation of the description of the original constructs.
A proposal has recently been made for a modular approach to SOS, called MSOS. The basic definitions of the Modular SOS framework are recalled here, but the reader is referred to other papers for a full introduction. This paper focusses on illustrating the applicability of Modular SOS, 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. The reader is assumed to be familiar with conventional SOS, with the concepts of functional programming languages such as Standard ML, and with fundamental notions of concurrency Available as PostScript, PDF, DVI. |