A Modular SOS for ML Concurrency Primitives

Open Access
Publisher Website
Google Scholar
Abstract
Modularity is an important pragmatic aspect of semanticdescriptions. 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 ofthe details of how computations are modeled. In structural operationalsemantics (SOS), however, this issue has largely been neglected, andSOS descriptions of programming languages typically exhibit rather poormodularity| - for instance, extending the described language may entaila complete reformulation of the description of the original constructs.A proposal has recently been made for a modular approach to SOS, calledMSOS. The basic definitions of the Modular SOS framework are recalledhere, but the reader is referred to other papers for a full introduction.This paper focuses on illustrating the applicability of Modular SOS, byusing it to give a description of a sublanguage of Concurrent ML (CML);the transition rules for the purely functional constructs do not have to bereformulated at all when adding references and/or processes. The paperconcludes by comparing the MSOS description with previous operationaldescriptions of similar languages.The reader is assumed to be familiar with conventional SOS, with theconcepts of functional programming languages such as Standard ML, andwith fundamental notions of concurrency.

This publication has 0 references indexed in Scilit: