2026-07-25T14:32:11Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:16471 2024-03-06T10:57:34Z ddc:004 open_access

Functions and References in the Pi-Calculus: Full Abstraction and Proof Techniques Prebet, Enguerrand Call-by-value λ-calculus imperative Programming π-calculus Bisimulation Type System 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Enguerrand Prebet 2022 Is Part Of LIPIcs, Volume 229, 49th International Colloquium on Automata, Languages, and Programming (ICALP 2022) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ICALP.2022.130 urn:nbn:de:0030-drops-164715 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2022.130 eng https://creativecommons.org/licenses/by/4.0/legalcode