[go: up one dir, main page]

Pré-Publication, Document De Travail Année : 2020
On the Representation of References in the pi-calculus
1 ENS de Lyon - École normale supérieure de Lyon (15 parvis René Descartes - BP 7000 - 69342 Lyon Cedex 07 - France)
"> ENS de Lyon - École normale supérieure de Lyon
2 LIP - Laboratoire de l'Informatique du Parallélisme (46 Allée d'Italie 69364 LYON CEDEX 07 - France)
"> LIP - Laboratoire de l'Informatique du Parallélisme
3 PLUME - Preuves et Langages (France)
"> PLUME - Preuves et Langages
4 FOCUS - Foundations of Component-based Ubiquitous Systems (Dipartimento di Informatica - Scienza e Ingegneria (DISI) Universita' di Bologna Mura Anteo Zamboni, 7 40126 Bologna ITALY - Italie)
"> FOCUS - Foundations of Component-based Ubiquitous Systems
5 UNIBO - Alma Mater Studiorum Università di Bologna = University of Bologna (Via Zamboni, 33 - 40126 Bologna - Italie) "> UNIBO - Alma Mater Studiorum Università di Bologna = University of Bologna

Résumé

The π-calculus has been advocated as a model to interpret, and give semantics to, languages withhigher-order features. Often these languages make use of forms of references (and hence viewing astore 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. Wefirst define π ref , an extension of Aπ with references and operators to manipulate them, and illustrateexamples 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. Weestablish full abstraction of the translation w.r.t. barbed congruence and barbed equivalence in thetwo calculi. We investigate proof techniques for barbed equivalence in Aπ, based on two forms oflabelled 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, leavingcompleteness open. Finally, we discuss examples of uses of the bisimilarities.
Fichier principal
Vignette du fichier
refapi_full.pdf (652) Télécharger le fichier
Origine Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-02895654 , version 1 (10-07-2020)
hal-02895654 , version 2 (10-07-2020)
Identifiants
  • HAL Id : hal-02895654 , version 2

Citer

Daniel Hirschkoff, Enguerrand Prebet, Davide Sangiorgi. On the Representation of References in the pi-calculus. 2020. ⟨hal-02895654v2⟩
361 Consultations
143 Téléchargements

Partager

More