On the Representation of References in the pi-calculus

The π-calculus has been advocated as a model to interpret, and give semantics to, languages with\r\nhigher-order features. Often these languages make use of forms of references (and hence viewing a\r\nstore as set of references). While translations of references in π-calculi (and CCS) have appeared,\r\nthe precision of such translations has not been fully investigated. In this paper we address this issue.\r\n\r\nWe focus on the asynchronous π-calculus (Aπ), where translations of references are simpler. We\r\nfirst define π ref , an extension of Aπ with references and operators to manipulate them, and illustrate\r\nexamples of the subtleties of behavioural equivalence in π ref . We then consider a translation of\r\nπ ref into Aπ. References of π ref are mapped onto names of Aπ belonging to a dedicated \"reference\"\r\ntype. We show how the presence of reference names affects the definition of barbed congruence. We\r\nestablish full abstraction of the translation w.r.t. barbed congruence and barbed equivalence in the\r\ntwo calculi. We investigate proof techniques for barbed equivalence in Aπ, based on two forms of\r\nlabelled bisimilarities. For one bisimilarity we derive both soundness and completeness; for another,\r\nmore efficient and involving an inductive ‘game’ on reference names, we derive soundness, leaving\r\ncompleteness open. Finally, we discuss examples of uses of the bisimilarities.