A theory of bisimulation for a fragment of concurrent ML with local names.

Jeffrey, A and Rathke, J (2000) A theory of bisimulation for a fragment of concurrent ML with local names. In: Unset, Proceedings of the 15th Annual Symposium on Logic in Computer Science Santa Barbara. IEEE Computer Society Press..

Full text not available from this repository.

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.

Item Type: Conference or Workshop Item (Paper)
Schools and Departments: School of Engineering and Informatics > Informatics
Depositing User: EPrints Services
Date Deposited: 06 Feb 2012 20:51
Last Modified: 13 Apr 2012 11:24
URI: http://sro.sussex.ac.uk/id/eprint/28451
📧 Request an update