A theory of bisimulation for a fragment of Concurrent ML with local names

Author

Jeffrey, Alan ; Rathke, Julian

Author_Institution

CTI, DePaul Univ., Chicago, IL, USA

fYear

2000

fDate

2000

Firstpage

311

Lastpage

321

Abstract

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

Keywords

ML language; bisimulation equivalence; multi-threading; programming language semantics; μvCML; π-calculus-like primitives; CML fragment; Concurrent ML; Standard ML; barbed bisimulation congruence; bisimulation theory; dynamically generated local channels; labelled transitions semantics; local names; multi-threaded programming; normal bisimulation; reduction semantics; thread identifiers; weak bisimulation; Calculus; Carbon capture and storage; Communication channels; Communication system control; Concurrent computing; Electrical capacitance tomography; Equations; Optimizing compilers; Program processors; Yarn;

fLanguage

English

Publisher

ieee

Conference_Titel

Logic in Computer Science, 2000. Proceedings. 15th Annual IEEE Symposium on

Conference_Location

Santa Barbara, CA

ISSN

1043-6871

Print_ISBN

0-7695-0725-5

Type

conf

DOI

10.1109/LICS.2000.855780

Filename

855780