Functions and References in the Pi-Calculus: Full Abstraction and Proof Techniques - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2022

Functions and References in the Pi-Calculus: Full Abstraction and Proof Techniques

Résumé

We present a fully abstract encoding of λ ref , the call-by-value λ-calculus with references, in the πcalculus. By contrast with previous full abstraction results for sequential languages in the π-calculus, the characterisation of contextual equivalence in the source language uses a labelled bisimilarity. To define the latter equivalence, we refine existing notions of typed bisimulation in the π-calculus, and introduce in particular a specific component to handle divergences. We obtain a proof technique that allows us to prove equivalences between λ ref programs via the encoding. The resulting proofs correspond closely to normal form bisimulations in the λ-calculus, making proofs in the π-calculus expressible as if reasoning in λ ref. We study how standard and new up-to techniques can be used to reason about diverging terms and simplify proofs of equivalence using the bisimulation we introduce. This shows how the π-calculus theory can be used to prove interesting equivalences between λ ref programs, using algebraic reasoning and up-to techniques.
Fichier principal
Vignette du fichier
lambda_ref.pdf (668.74 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)

Dates et versions

hal-03920025 , version 1 (06-01-2023)

Identifiants

Citer

Enguerrand Prebet. Functions and References in the Pi-Calculus: Full Abstraction and Proof Techniques. ICALP 2022 - 49th International Colloquium on Automata, Languages, and Programming, Jul 2022, Paris, France. ⟨10.4230/LIPIcs.ICALP.2022.114⟩. ⟨hal-03920025⟩
25 Consultations
50 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More