3 Search Results for "Hirschkoff, Daniel"


Document
Track B: Automata, Logic, Semantics, and Theory of Programming
Functions and References in the Pi-Calculus: Full Abstraction and Proof Techniques

Authors: Enguerrand Prebet

Published in: LIPIcs, Volume 229, 49th International Colloquium on Automata, Languages, and Programming (ICALP 2022)


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.

Cite as

Enguerrand Prebet. Functions and References in the Pi-Calculus: Full Abstraction and Proof Techniques. In 49th International Colloquium on Automata, Languages, and Programming (ICALP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 229, pp. 130:1-130:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)


Copy BibTex To Clipboard

@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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2022.130},
  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}
}
Document
On the Representation of References in the Pi-Calculus

Authors: Daniel Hirschkoff, Enguerrand Prebet, and Davide Sangiorgi

Published in: LIPIcs, Volume 171, 31st International Conference on Concurrency Theory (CONCUR 2020)


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.

Cite as

Daniel Hirschkoff, Enguerrand Prebet, and Davide Sangiorgi. On the Representation of References in the Pi-Calculus. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 34:1-34:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)


Copy BibTex To Clipboard

@InProceedings{hirschkoff_et_al:LIPIcs.CONCUR.2020.34,
  author =	{Hirschkoff, Daniel and Prebet, Enguerrand and Sangiorgi, Davide},
  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 =	{Konnov, Igor and Kov\'{a}cs, Laura},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.34},
  URN =		{urn:nbn:de:0030-drops-128466},
  doi =		{10.4230/LIPIcs.CONCUR.2020.34},
  annote =	{Keywords: Process calculus, Bisimulation, Asynchrony, Imperative programming}
}
Document
Divergence and Unique Solution of Equations

Authors: Adrien Durier, Daniel Hirschkoff, and Davide Sangiorgi

Published in: LIPIcs, Volume 85, 28th International Conference on Concurrency Theory (CONCUR 2017)


Abstract
We study proof techniques for bisimilarity based on unique solution of equations. We draw inspiration from a result by Roscoe in the denotational setting of CSP and for failure semantics, essentially stating that an equation (or a system of equations) whose infinite unfolding never produces a divergence has the unique-solution property. We transport this result onto the operational setting of CCS and for bisimilarity. We then exploit the operational approach to: refine the theorem, distinguishing between different forms of divergence; derive an abstract formulation of the theorems, on generic LTSs; adapt the theorems to other equivalences such as trace equivalence, and to preorders such as trace inclusion. We compare the resulting techniques to enhancements of the bisimulation proof method (the ‘up-to techniques’). Finally, we study the theorems in name-passing calculi such as the asynchronous pi-calculus, and revisit the completeness proof of Milner’s encoding of the lambda-calculus into the pi-calculus for Lévy-Longo Trees.

Cite as

Adrien Durier, Daniel Hirschkoff, and Davide Sangiorgi. Divergence and Unique Solution of Equations. In 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, pp. 11:1-11:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)


Copy BibTex To Clipboard

@InProceedings{durier_et_al:LIPIcs.CONCUR.2017.11,
  author =	{Durier, Adrien and Hirschkoff, Daniel and Sangiorgi, Davide},
  title =	{{Divergence and Unique Solution of Equations}},
  booktitle =	{28th International Conference on Concurrency Theory (CONCUR 2017)},
  pages =	{11:1--11:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-048-4},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{85},
  editor =	{Meyer, Roland and Nestmann, Uwe},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2017.11},
  URN =		{urn:nbn:de:0030-drops-77849},
  doi =		{10.4230/LIPIcs.CONCUR.2017.11},
  annote =	{Keywords: Bisimilarity, unique solution of equations, termination, process calculi}
}
  • Refine by Author
  • 2 Hirschkoff, Daniel
  • 2 Prebet, Enguerrand
  • 2 Sangiorgi, Davide
  • 1 Durier, Adrien

  • Refine by Classification
  • 2 Theory of computation → Semantics and reasoning

  • Refine by Keyword
  • 2 Bisimulation
  • 1 Asynchrony
  • 1 Bisimilarity
  • 1 Call-by-value λ-calculus
  • 1 Imperative programming
  • Show More...

  • Refine by Type
  • 3 document

  • Refine by Publication Year
  • 1 2017
  • 1 2020
  • 1 2022

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail