Semantics for core Concurrent ML using computation types
Alan Jeffrey · 1999
This paper presents two typed higher-order concurrent functional programming languages, based on Reppy's Concurrent ML. The first is a simplified, monomorphic variant of CML, which allows reduction of terms of any type. The second uses an explicit type constructor for computation, in the style of Moggi's monadic metalanguage. Each of these languages is given an operational semantics, which can be used as the basis of bisimulation equivalence. We show how Moggi's translation of the call-by-value lambdacalculus into the mondadic metalanguage can be extended to these concurrent languages, and that this translation is correct up to weak bisimulation. 1 Introduction Reppy's (1991, 1992) Concurrent ML is an extension of New Jersey ML with features for spawning threads, which can communicate by one-to-one synchronous handshake in the style of Milner's (1989) CCS. There are (at least) two approaches to giving the operational semantics to CML. The `functional language definition' tradition (Mi...