Search Results

Documents authored by Hirschkoff, Daniel

Document
DOI: 10.4230/LIPIcs.CONCUR.2025.23
First-Order Store and Visibility in Name-Passing Calculi

Authors: Daniel Hirschkoff, Iwan Quémerais, and Davide Sangiorgi

Published in: LIPIcs, Volume 348, 36th International Conference on Concurrency Theory (CONCUR 2025)

Abstract
The π-calculus is the paradigmatical name-passing calculus. While being purely name-passing, it allows the representation of higher-order functions and store. We study how π-calculus processes can be controlled so that computations can only involve storage of first-order values. The discipline is enforced by a type system that is based on the notion of visibility, coming from game semantics. We discuss the impact of visibility on the behavioural theory. We propose characterisations of may-testing and barbed equivalence, based on (variants of) trace equivalence and labelled bisimilarity, in the case where computation is sequential, and in the case where computation is well-bracketed.
Cite as

Daniel Hirschkoff, Iwan Quémerais, and Davide Sangiorgi. First-Order Store and Visibility in Name-Passing Calculi. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 23:1-23:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{hirschkoff_et_al:LIPIcs.CONCUR.2025.23,
  author =	{Hirschkoff, Daniel and Qu\'{e}merais, Iwan and Sangiorgi, Davide},
  title =	{{First-Order Store and Visibility in Name-Passing Calculi}},
  booktitle =	{36th International Conference on Concurrency Theory (CONCUR 2025)},
  pages =	{23:1--23:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-389-8},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{348},
  editor =	{Bouyer, Patricia and van de Pol, Jaco},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2025.23},
  URN =		{urn:nbn:de:0030-drops-239737},
  doi =		{10.4230/LIPIcs.CONCUR.2025.23},
  annote =	{Keywords: process calculi, behavioural equivalence, type system}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2020.34
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.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
DOI: 10.4230/LIPIcs.CONCUR.2017.11
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.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}
}
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
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact