License: 
Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CONCUR.2020.34
URN: urn:nbn:de:0030-drops-128466
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2020/12846/
Hirschkoff, Daniel ;
Prebet, Enguerrand ;
Sangiorgi, Davide
On the Representation of References in the Pi-Calculus
Abstract
The π-calculus has been advocated as a model to interpret, and give semantics to, languages with higher-order features. Often these languages make use of forms of references (and hence viewing a store as set of references). While translations of references in π-calculi (and CCS) have appeared, the precision of such translations has not been fully investigated. In this paper we address this issue.
We focus on the asynchronous π-calculus (Aπ), where translations of references are simpler. We first define π^ref, an extension of Aπ with references and operators to manipulate them, and illustrate examples of the subtleties of behavioural equivalence in π^ref. We then consider a translation of π^ref into Aπ. References of π^ref are mapped onto names of Aπ belonging to a dedicated "reference" type. We show how the presence of reference names affects the definition of barbed congruence. We establish full abstraction of the translation w.r.t. barbed congruence and barbed equivalence in the two calculi. We investigate proof techniques for barbed equivalence in Aπ, based on two forms of labelled bisimilarities. For one bisimilarity we derive both soundness and completeness; for another, more efficient and involving an inductive "game" on reference names, we derive soundness, leaving completeness open. Finally, we discuss examples of uses of the bisimilarities.
BibTeX - Entry
@InProceedings{hirschkoff_et_al:LIPIcs:2020:12846,
author = {Daniel Hirschkoff and Enguerrand Prebet and Davide Sangiorgi},
title = {{On the Representation of References in the Pi-Calculus}},
booktitle = {31st International Conference on Concurrency Theory (CONCUR 2020)},
pages = {34:1--34:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-160-3},
ISSN = {1868-8969},
year = {2020},
volume = {171},
editor = {Igor Konnov and Laura Kov{\'a}cs},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2020/12846},
URN = {urn:nbn:de:0030-drops-128466},
doi = {10.4230/LIPIcs.CONCUR.2020.34},
annote = {Keywords: Process calculus, Bisimulation, Asynchrony, Imperative programming}
}
|
Keywords: |
|
Process calculus, Bisimulation, Asynchrony, Imperative programming |
|
Collection: |
|
31st International Conference on Concurrency Theory (CONCUR 2020) |
|
Issue Date: |
|
2020 |
|
Date of publication: |
|
26.08.2020 |
