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 transitions semantics provided for the entire language. We present a labelled transition semantics for a fragment of CML called μvCML which includes features not covered before: dynamically generated local channels and thread identifiers. We show that weak bisimulation for μvCML is a congruence, and coincides with barbed bisimulation congruence. We also provide a variant of D. Sangiorgi´s (1993) normal bisimulation for μvCML, and show that this too coincides with bisimulation