License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ICALP.2022.130
URN: urn:nbn:de:0030-drops-164715
URL: https://drops.dagstuhl.de/opus/volltexte/2022/16471/
 Go to the corresponding LIPIcs Volume Portal

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

 pdf-format:

### Abstract

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.

### BibTeX - Entry

@InProceedings{prebet:LIPIcs.ICALP.2022.130,
author =	{Prebet, Enguerrand},
title =	{{Functions and References in the Pi-Calculus: Full Abstraction and Proof Techniques}},
booktitle =	{49th International Colloquium on Automata, Languages, and Programming (ICALP 2022)},
pages =	{130:1--130:19},
series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN =	{978-3-95977-235-8},
ISSN =	{1868-8969},
year =	{2022},
volume =	{229},
editor =	{Boja\'{n}czyk, Miko{\l}aj and Merelli, Emanuela and Woodruff, David P.},
publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address =	{Dagstuhl, Germany},
URL =		{https://drops.dagstuhl.de/opus/volltexte/2022/16471},
URN =		{urn:nbn:de:0030-drops-164715},
doi =		{10.4230/LIPIcs.ICALP.2022.130},
annote =	{Keywords: Call-by-value \lambda-calculus, imperative Programming, \pi-calculus, Bisimulation, Type System}
}

 Keywords: Call-by-value λ-calculus, imperative Programming, π-calculus, Bisimulation, Type System Collection: 49th International Colloquium on Automata, Languages, and Programming (ICALP 2022) Issue Date: 2022 Date of publication: 28.06.2022

DROPS-Home | Fulltext Search | Imprint | Privacy