From CML to its Process Algebra

Reppy's (1991) language CML (Concurrent ML) extends the Standard ML of Milner et al. (1990) with primitives for communication. It thus inherits a notion of strong polymorphic typing and may be equipped with a structural operational semantics. As a first step, we formulate an effect system for statically expressing the communication behaviours of CML programs as these are not reflected in the types. As a second step, we adapt the structural operational semantics of CML so as to incorporate behaviours. We then show how types and behaviours evolve in the course of computation: types may decrease and behaviours may lose prefixes as well as decrease. As the syntax of behaviours is rather similar to that of a process algebra, our main result may therefore be viewed as regarding the semantics of a process algebra as an abstraction of the semantics of an underlying programming language. This establishes a new kind of connection between "realistic" concurrent programming languages and "theoretical" process algebras