A Theory of Bisimulation for a Fragment of Concurrent ML with Local Names

Concurrent ML is an extension of Standard ML with π-calculus-like primitives for multi-threaded programming. CML has a reduction semantics, but to date there has been no labelled transition system semantics provided for the entire language. In this paper, we present a labelled transition semantics for a fragment of CML called µνCML which includes features not covered before: dynamically generated local channels and thread identifiers. We show that weak bisimilarity for µνCML is a congruence, and coincides with barbed bisimulation congruence. We also provide a variant of Sangiorgi’s normal bisimulation for µνCML, and show that this too coincides with bisimilarity.

• Type: Conference
• Year: 2000
• Where: LICS
• Authors: Alan Jeffrey, Julian Rathke
• Keywords: Automated Reasoning, CML Called µνCML, Labelled Transition, Labelled Transition Semantics, LICS 2000