DROPS

Document

DOI: 10.4230/LIPIcs.LICS.2026.79

Wiring the π-Calculus to Denotational Semantics

Authors: Ken Sakayori, Davide Sangiorgi, Simon Castellan, and Pierre Clairambault

Published in: LIPIcs, Volume 380, 41st Annual Symposium on Logic in Computer Science (LICS 2026)

Abstract

We introduce a dialect of the Asynchronous π-calculus, called AWπ, in which (1) an input name may be owned, at any time, by at most one process; (2) each name has either only the input or only the output capability. As a result, special processes called wires (aka forwarders, that is, processes that receive values at one name and re-transmit) behave as substitutions when composed with any AWπ process. Thus AWπ naturally yields a category, whose morphisms are AWπ processes (modulo the reference behavioural equivalence, barbed congruence) and whose objects are types; and where wires act as identity morphisms. We show that the category of processes can be further organised into (sub)categories with the structures needed for the interpretation of common higher-order language features in the literature by drawing on insights from game semantics; notably, we construct a relative Seely category, the categorical structure that concurrent game semantics has. At the same time, AWπ follows the tradition of ordinary π-calculi in that expressiveness is preserved and the operational and algebraic theory are developed in a similar manner, notwithstanding substantial technical differences in their development and proofs. In short, the goal of AWπ is to remain faithful to the operational and algebraic tradition of the π-calculi while connecting to the tradition of denotational models for programming languages.

Cite as

Ken Sakayori, Davide Sangiorgi, Simon Castellan, and Pierre Clairambault. Wiring the π-Calculus to Denotational Semantics. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 79:1-79:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{sakayori_et_al:LIPIcs.LICS.2026.79,
  author =	{Sakayori, Ken and Sangiorgi, Davide and Castellan, Simon and Clairambault, Pierre},
  title =	{{Wiring the \pi-Calculus to Denotational Semantics}},
  booktitle =	{41st Annual Symposium on Logic in Computer Science (LICS 2026)},
  pages =	{79:1--79:28},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-434-5},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{380},
  editor =	{Faggian, Claudia and Katoen, Joost-Pieter},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.79},
  URN =		{urn:nbn:de:0030-drops-268669},
  doi =		{10.4230/LIPIcs.LICS.2026.79},
  annote =	{Keywords: \pi-calculus, denotational semantics, game semantics, wire process}
}

Document

DOI: 10.4230/LIPIcs.FSCD.2021.32

Output Without Delay: A π-Calculus Compatible with Categorical Semantics

Authors: Ken Sakayori and Takeshi Tsukada

Published in: LIPIcs, Volume 195, 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)

Abstract

The quest for logical or categorical foundations of the π-calculus (not limited to session-typed variants) remains an important challenge. A categorical type theory correspondence for a variant of the i/o-typed π-calculus was recently revealed by Sakayori and Tsukada, but, at the same time, they exposed that this categorical semantics contradicts with most of the behavioural equivalences. This paper diagnoses the nature of this problem and attempts to fill the gap between categorical and operational semantics. We first identify the source of the problem to be the mismatch between the operational and categorical interpretation of a process called the forwarder. From the operational viewpoint, a forwarder may add an arbitrary delay when forwarding a message, whereas, from the categorical viewpoint, a forwarder must not add any delay when forwarding a message. Led by this observation, we introduce a calculus that can express forwarders that do not introduce delay. More specifically, the calculus we introduce is a variant of the π-calculus with a new operational semantics in which output actions are forced to happen as soon as they get unguarded. We show that this calculus (i) is compatible with the categorical semantics and (ii) can encode the standard π-calculus.

Cite as

Ken Sakayori and Takeshi Tsukada. Output Without Delay: A π-Calculus Compatible with Categorical Semantics. In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 32:1-32:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{sakayori_et_al:LIPIcs.FSCD.2021.32,
  author =	{Sakayori, Ken and Tsukada, Takeshi},
  title =	{{Output Without Delay: A \pi-Calculus Compatible with Categorical Semantics}},
  booktitle =	{6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)},
  pages =	{32:1--32:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-191-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{195},
  editor =	{Kobayashi, Naoki},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2021.32},
  URN =		{urn:nbn:de:0030-drops-142705},
  doi =		{10.4230/LIPIcs.FSCD.2021.32},
  annote =	{Keywords: \pi-calculus, categorical semantics, linear approximation}
}

Search Results

Documents authored by Sakayori, Ken

Wiring the π-Calculus to Denotational Semantics

Abstract

Cite as

Output Without Delay: A π-Calculus Compatible with Categorical Semantics

Abstract

Cite as

Thanks for your feedback!

Could not send message