×

zbMATH — the first resource for mathematics

A theory of weak bisimulation for core CML. (English) Zbl 0916.68093
Summary: Concurrent ML (CML) is an extension of Standard ML of New Jersey with concurrent features similar to those of process algebra. In this paper, we build upon John Reppy’s reduction semantics for CML by constructing a compositional operational semantics for a fragment of CML, based on higher-order process algebra. Using the operational semantics, we generalize the notion of weak bisimulation equivalence to build a semantic theory of CML. We give some small examples of proofs about CML expressions, and show that our semantics corresponds to Reppy’s up to weak first-order bisimulation.

MSC:
68Q55 Semantics in the theory of computing
68N15 Theory of programming languages
68N18 Functional programming and lambda calculus
Keywords:
Concurrent ML; CML
Software:
Facile
PDF BibTeX XML Cite
Full Text: DOI