×

zbMATH — the first resource for mathematics

A theory of bisimulation for a fragment of concurrent ML with local names. (English) Zbl 1105.68354
Summary: Concurrent ML is an extension of Standard ML with \(\pi\)-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 \(\mu v\)CML which includes features not covered before: dynamically generated local channels and thread identifiers. We show that weak bisimilarity for \(\mu v\)CML is a congruence, and coincides with barbed bisimulation congruence. We also provide a variant of Sangiorgi’s normal bisimulation for \(\mu v\)CML, and show that this too coincides with bisimilarity.

MSC:
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
Software:
ML
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] K.L. Bernstein, E.W. Stark, Operational semantics of a focussing debugger, in: Proc. MFPS 95, Electronic Notes in Computer Science, Vol. 1, Springer, Berlin, 1995. · Zbl 0910.68128
[2] D. Berry, R. Milner, D. Turner, A semantics for ML concurrency primitives, in: Proc. 19th ACM Symp. on Principles of Programmings Languages, 1992.
[3] G. Boudol, Asynchrony and the π-calculus, Tech. Report 1702, INRIA, Sophia-Antipolis, 1991.
[4] Boudol, G., The π-calculus in direct style, Higher-order symbolic comput., 11, (1998) · Zbl 0934.68037
[5] L. Cardelli, A. Gordon, Mobile ambients, in: Proc. FoSSaCS ’98, Lecture Notes in Computer Science, Springer, Berlin, 1998.
[6] Ferreira, W.; Hennessy, M.; Jeffrey, A.S.A, A theory of weak bisimulation for core CML, J. funct. programming, 8, 5, 447-491, (1998) · Zbl 0916.68093
[7] C. Fournet, G. Gonthier, The reflexive CHAM and the join-calculus, in: Proc. ACM-POPL, 1996.
[8] C. Fournet, G. Gonthier, A hierarchy of equivalences for asynchronous calculi, in: Proc. ICALP, Lecture Notes in Computer Science, Vol. 1443, Springer, Berlin, 1998. · Zbl 0909.03030
[9] C. Fournet, G. Gonthier, J.-J. Levy, L. Maranget, D. Remy, A calculus of mobile agents, in: Proc. CONCUR, Lecture Notes in Computer Science, Vol. 1119, Springer, Berlin, 1996.
[10] A. Gordon, Bisimilarity as a theory of functional programming, in: Proc. MFPS 95, Electronic Notes in Computer Science, Vol. 1, Springer, Berlin, 1995. · Zbl 0910.68118
[11] A. Gordon, P.D. Hankin, A concurrent object calculus, in: Proc. HLCL, 1998. · Zbl 0917.68064
[12] K. Honda, M. Tokoro, An object calculus for asynchronous communication, in: Proc. ECOOP 91, Geneve, 1991.
[13] Honda, K.; Yoshida, N., On reduction-based process semantics, Theoret. comput. sci., 152, 2, 437-486, (1995) · Zbl 0871.68122
[14] D. Howe, Equality in lazy computation systems, in: Proc. IEEE Logic in Computer Science, IEEE Computer Society Press, Silver Spring, MD, 1989, pp. 198-203. · Zbl 0716.68065
[15] A.S.A. Jeffrey, J. Rathke, Towards a theory of bisimilarity for local names, in: Proc. IEEE Logic in Computer Science, IEEE Computer Society Press, Silver Spring, MD, 1999, pp. 56-66.
[16] A.S.A. Jeffrey, J. Rathke, Towards a theory of bisimilarity for local names, in: Proc. IEEE Logic in Computer Science, IEEE Computer Society Press, Silver Spring, MD, 2000, pp. 311-321.
[17] A.S.A. Jeffrey, J. Rathke, A fully abstract may testing semantics for concurrent objects, in: Proc. IEEE Logic in Computer Science, IEEE Computer Society Press, Silver Spring, MD, 2002, pp. 101-112. · Zbl 1078.68107
[18] Leifer, J.J.; Milner, R., Deriving bisimulation congruences for reactive systems, () · Zbl 0999.68141
[19] Milner, R., A calculus of communicating systems, Lecture notes in computer science, Vol. 92, (1980), Springer Berlin · Zbl 0452.68027
[20] Milner, R., Communication and mobile systems: the π-calculus, (1999), Cambridge University Press Cambridge · Zbl 0942.68002
[21] Milner, R.; Parrow, J.; Walker, D., A calculus of mobile processes, part I + II, Inform. and comput., 100, 1, 1-77, (1992)
[22] R. Milner, D. Sangiorgi, Barbed bisimulation, in: Proc. ICALP, Lecture Notes in Computer Science, Vol. 623, Springer, Berlin, 1992.
[23] Moggi, E., Notions of computation and monads, Inform. and comput., 93, 55-92, (1991) · Zbl 0723.68073
[24] A.M. Pitts, I.D.B. Stark, Observable properties of higher order functions that dynamically create local names, or: what’s new?, in: Proc. MFCS 93, Lecture Notes in Computer Science, Vol. 711, Springer, Berlin, 1993, pp. 122-141.
[25] A.M. Pitts, I.D.B. Stark, Operational reasoning for functions with local state, in: A.D. Gordon, A.M. Pitts (Eds.), Higher Order Operational Techniques in Semantics, Cambridge University Press, Cambridge, 1998, Publications of the Newton Institute, pp. 227-273. · Zbl 0967.68035
[26] J. Reppy, Higher-order concurrency, Ph.D. Thesis, Cornell University, 1992, Technical Report TR 92-1285.
[27] J. Riely, M. Hennessy, A typed language for distributed mobile processes, in: Proc. POPL, ACM Press, New York, 1998. · Zbl 0917.68047
[28] D. Sangiorgi, Expressing mobility in process algebras: first-order and higher-order paradigms, Ph.D. Thesis, University of Edinburgh, 1993.
[29] D. Sangiorgi, R. Milner, On the problem of ‘weak bisimulation up to’, in: Proc. CONCUR, Lecture Notes in Computer Science, Vol. 630, Springer, Berlin, 1992, pp. 32-46.
[30] P. Sewell, From rewrite rules to bisimulation congruences, in: Proc. CONCUR, Lecture Notes in Computer Science, Vol. 1466, Springer, Berlin, 1992, pp. 269-284.
[31] P. Sewell, Global/local subtyping and capability inference for a distributed π-calculus, in: Proc. ICALP, Lecture Notes in Computer Science, Vol. 1443, Springer, Berlin, 1998, pp. 695-706. · Zbl 0910.03021
[32] B. Thomsen, Calculi for higher-order communicating systems, Ph.D. Thesis, University of London, 1990.
[33] Tofte, M.; Milner, R.; Harper, R., The definition of standard ML, (1990), MIT Press Cambridge, MA
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.