Document Open Access Logo

Wiring the π-Calculus to Denotational Semantics

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

PDF

File

Thumbnail PDF
PDF
LIPIcs.LICS.2026.79.pdf
  • Filesize: 0.97 MB
  • 28 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Denotational semantics
  • Theory of computation → Process calculi
  • Theory of computation → Categorical semantics
  • Theory of computation → Interactive computation
Keywords
  • π-calculus
  • denotational semantics
  • game semantics
  • wire process

Metrics

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 Get BibTex

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) https://doi.org/10.4230/LIPIcs.LICS.2026.79

Author Details

Ken Sakayori
  • The University of Tokyo, Japan
Davide Sangiorgi
  • University of Bologna, Italy
  • Inria Centre d'Université Côte d'Azur, Sophia Antipolis, France
Simon Castellan
  • Inria, Univ Rennes, CNRS, IRISA, France
Pierre Clairambault
  • CNRS, Aix Marseille Univ, LIS, France

Funding

  • Sakayori, Ken: JSPS KAKENHI Grant Number JP24K20731.
  • Sangiorgi, Davide: MIUR11PRIN project "Resource Awareness in Programming: Algebra, Rewriting, and Analysis" (RAP, ID P2022HXNSC).
  • Clairambault, Pierre: ANR project DyVerSe (ANR-19-CE48-0010-01).

Acknowledgements

We are grateful to the anonymous reviewers for their feedback.

References

  1. Samson Abramsky, Simon J. Gay, and Rajagopal Nagarajan. Interaction categories and the foundations of typed concurrent programming. In Manfred Broy, editor, Proceedings of the NATO Advanced Study Institute on Deductive Program Design, Marktoberdorf, Germany, pages 35-113, 1996. Google Scholar
  2. Thorsten Altenkirch, James Chapman, and Tarmo Uustalu. Monads need not be endofunctors. Log. Methods Comput. Sci., 11(1), 2015. URL: https://doi.org/10.2168/LMCS-11(1:3)2015.
  3. Roberto M. Amadio. An asynchronous model of locality, failure and process mobility. In David Garlan and Daniel Le Métayer, editors, Coordination Languages and Models, Second International Conference, COORDINATION '97, Berlin, Germany, September 1-3, 1997, Proceedings, volume 1282 of Lecture Notes in Computer Science, pages 374-391. Springer, 1997. URL: https://doi.org/10.1007/3-540-63383-9_92.
  4. Roberto M. Amadio, Gérard Boudol, and Cédric Lhoussaine. The receptive distributed pi-calculus. ACM Trans. Program. Lang. Syst., 25(5):549-577, 2003. URL: https://doi.org/10.1145/937563.937564.
  5. Nathanael Arkor and Dylan McDermott. The formal theory of relative monads. Journal of Pure and Applied Algebra, 228(9):107676, 2024. URL: https://doi.org/10.1016/j.jpaa.2024.107676.
  6. David Baelde, Andrew Gacek, Dale Miller, Gopalan Nadathur, and Alwen Tiu. The bedwyr system for model checking over syntactic expressions. In Frank Pfenning, editor, 21st Conf. on Automated Deduction (CADE), volume 4603 of Lecture Notes in Computer Science, pages 391-397. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-73595-3_28.
  7. Gianluigi Bellin and Philip J. Scott. On the pi-calculus and linear logic. Theor. Comput. Sci., 135(1):11-65, 1994. URL: https://doi.org/10.1016/0304-3975(94)00104-9.
  8. Martin Berger, Kohei Honda, and Nobuko Yoshida. Sequentiality and the pi-calculus. In Samson Abramsky, editor, Typed Lambda Calculi and Applications TLCA 2001, volume 2044 of Lecture Notes in Computer Science, pages 29-45. Springer, 2001. URL: https://doi.org/10.1007/3-540-45413-6_7.
  9. Michele Boreale. On the expressiveness of internal mobility in name-passing calculi. Theor. Comput. Sci., 195(2):205-226, 1998. URL: https://doi.org/10.1016/S0304-3975(97)00220-X.
  10. Michele Boreale and Rocco De Nicola. A symbolic semantics for the pi-calculus. Inf. Comput., 126(1):34-52, 1996. URL: https://doi.org/10.1006/INCO.1996.0032.
  11. Michele Boreale, Rocco De Nicola, and Rosario Pugliese. Trace and testing equivalence on asynchronous processes. Inf. Comput., 172(2):139-164, 2002. URL: https://doi.org/10.1006/INCO.2001.3080.
  12. Luís Caires, Frank Pfenning, and Bernardo Toninho. Linear logic propositions as session types. Mathematical Structures in Computer Science, 26(3):367-423, 2016. URL: https://doi.org/10.1017/S0960129514000218.
  13. Simon Castellan, Pierre Clairambault, Silvain Rideau, and Glynn Winskel. Games and strategies as event structures. Log. Methods Comput. Sci., 13(3), 2017. URL: https://doi.org/10.23638/LMCS-13(3:35)2017.
  14. Simon Castellan, Pierre Clairambault, and Glynn Winskel. Thin games with symmetry and concurrent hyland-ong games. Log. Methods Comput. Sci., 15(1), 2019. URL: https://doi.org/10.23638/LMCS-15(1:18)2019.
  15. Simon Castellan, Léo Stefanesco, and Nobuko Yoshida. Game semantics: Easy as pi. CoRR, abs/2011.05248, 2020. URL: https://arxiv.org/abs/2011.05248.
  16. Simon Castellan and Nobuko Yoshida. Two sides of the same coin: session types and game semantics: a synchronous side and an asynchronous side. Proc. ACM Program. Lang., 3(POPL):27:1-27:29, 2019. URL: https://doi.org/10.1145/3290340.
  17. Ilaria Castellani. Process algebras with localities. In Jan A. Bergstra, Alban Ponse, and Scott A. Smolka, editors, Handbook of Process Algebra, pages 945-1045. North-Holland / Elsevier, 2001. URL: https://doi.org/10.1016/B978-044482830-9/50033-3.
  18. Gian Luca Cattani, Ian Stark, and Glynn Winskel. Presheaf models for the pi-calculus. In Eugenio Moggi and Giuseppe Rosolini, editors, Category Theory and Computer Science, 7th International Conference, CTCS '97, Santa Margherita Ligure, Italy, September 4-6, 1997, Proceedings, Lecture Notes in Computer Science, pages 106-126. Springer, 1997. URL: https://doi.org/10.1007/BFB0026984.
  19. Pierre Clairambault. Causal Investigations in Interactive Semantics. Habilitation à diriger des recherches, Aix-Marseile Université, 2024. URL: https://hal.science/tel-04523273.
  20. Clovis Eberhart, Tom Hirschowitz, and Thomas Seiller. An intensionally fully-abstract sheaf model for pi. In Lawrence S. Moss and Pawel Sobocinski, editors, 6th Conference on Algebra and Coalgebra in Computer Science, CALCO 2015, Nijmegen, The Netherlands, June 24-26, 2015, volume 35 of LIPIcs, pages 86-100. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2015. URL: https://doi.org/10.4230/LIPIcs.CALCO.2015.86.
  21. Marcelo P. Fiore and Kohei Honda. Recursive types in games: Axiomatics and process representation. In Thirteenth Annual IEEE Symposium on Logic in Computer Science, Indianapolis, Indiana, USA, June 21-24, 1998, pages 345-356. IEEE Computer Society, 1998. URL: https://doi.org/10.1109/LICS.1998.705670.
  22. Marcelo P. Fiore, Eugenio Moggi, and Davide Sangiorgi. A fully abstract model for the pi-calculus. Inf. Comput., 179(1):76-117, 2002. URL: https://doi.org/10.1006/INCO.2002.2968.
  23. Cédric Fournet and Georges Gonthier. The reflexive CHAM and the join-calculus. In Hans-Juergen Boehm and Guy L. Steele Jr., editors, 23rd ACM Symposium on Principles of Programming Languages, pages 372-385. ACM Press, 1996. URL: https://doi.org/10.1145/237721.237805.
  24. Simon J. Gay and Vasco T. Vasconcelos. Session Types. Cambridge University Press, 2025. URL: https://doi.org/10.1017/9781009000062.
  25. Dan R. Ghica and Andrzej S. Murawski. Angelic semantics of fine-grained concurrency. Ann. Pure Appl. Log., 151(2-3):89-114, 2008. URL: https://doi.org/10.1016/J.APAL.2007.10.005.
  26. Matthew Hennessy. A fully abstract denotational semantics for the pi-calculus. Theor. Comput. Sci., 278(1-2):53-89, 2002. URL: https://doi.org/10.1016/S0304-3975(00)00331-5.
  27. Daniel Hirschkoff, Enguerrand Prebet, and Davide Sangiorgi. On sequentiality and well-bracketing in the π-calculus. In 36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021, Rome, Italy, June 29 - July 2, 2021, pages 1-13. IEEE, 2021. URL: https://doi.org/10.1109/LICS52264.2021.9470559.
  28. Daniel Hirschkoff, Iwan Quémerais, and Davide Sangiorgi. First-order store and visibility in name-passing calculi. In Patricia Bouyer and Jaco van de Pol, editors, 36th International Conference on Concurrency Theory, CONCUR 2025, Aarhus, Denmark, August 26-29, 2025, volume 348 of LIPIcs, pages 23:1-23:21. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2025. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2025.23.
  29. K. Honda and N. Yoshida. On reduction-based process semantics. Theor. Comput. Sci., 152(2):437-486, 1995. URL: https://doi.org/10.1016/0304-3975(95)00074-7.
  30. Kohei Honda and Nobuko Yoshida. Game-theoretic analysis of call-by-value computation. Theor. Comput. Sci., 221(1-2):393-456, 1999. URL: https://doi.org/10.1016/S0304-3975(99)00039-0.
  31. J. M. E. Hyland and C.-H. Luke Ong. Pi-calculus, dialogue games and PCF. In John Williams, editor, Proceedings of conf. on Functional programming languages and computer architecture (FPCA), pages 96-107. ACM, 1995. URL: https://doi.org/10.1145/224164.224189.
  32. Guilhem Jaber and Davide Sangiorgi. Games, mobile processes, and functions. In Florin Manea and Alex Simpson, editors, 30th EACSL Annual Conference on Computer Science Logic, CSL 2022, volume 216 of LIPIcs, pages 25:1-25:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. URL: https://doi.org/10.4230/LIPIcs.CSL.2022.25.
  33. Lalita Jategaonkar Jagadeesan and Radha Jagadeesan. Causality and true concurrency: A data-flow analysis of the pi-calculus (extended abstract). In Vangalur S. Alagar and Maurice Nivat, editors, Algebraic Methodology and Software Technology, 4th International Conference, AMAST '95, Montreal, Canada, July 3-7, 1995, Proceedings, Lecture Notes in Computer Science, pages 277-291. Springer, 1995. URL: https://doi.org/10.1007/3-540-60043-4_59.
  34. Cliff B. Jones. A pi-calculus semantics for an object-based design notation. In Eike Best, editor, CONCUR '93, 4th International Conference on Concurrency Theory, Hildesheim, Germany, August 23-26, 1993, Proceedings, volume 715 of Lecture Notes in Computer Science, pages 158-172. Springer, 1993. URL: https://doi.org/10.1007/3-540-57208-2_12.
  35. André Joyal. Remarques sur la théorie des jeux à deux personnes. Gazette des sciences mathématiques du Québec, 1(4):46-52, 1977. Google Scholar
  36. Naoki Kobayashi, Benjamin C. Pierce, and David N. Turner. Linearity and the pi-calculus. ACM Trans. Program. Lang. Syst., 21(5):914-947, 1999. URL: https://doi.org/10.1145/330249.330251.
  37. Wen Kokke, Fabrizio Montesi, and Marco Peressotti. Better late than never: a fully-abstract semantics for classical processes. Proc. ACM Program. Lang., 3(POPL):24:1-24:29, 2019. URL: https://doi.org/10.1145/3290337.
  38. James Laird. A categorical semantics of higher order store. In Richard Blute and Peter Selinger, editors, Category Theory and Computer Science, CTCS 2002, Ottawa, Canada, August 15-17, 2002, volume 69 of Electronic Notes in Theoretical Computer Science, pages 209-226. Elsevier, 2002. URL: https://doi.org/10.1016/S1571-0661(04)80566-8.
  39. Jim Laird. A game semantics of the asynchronous pi-calculus. In Martín Abadi and Luca de Alfaro, editors, CONCUR 2005 - Concurrency Theory, 16th International Conference, CONCUR 2005, San Francisco, CA, USA, August 23-26, 2005, Proceedings, volume 3653 of Lecture Notes in Computer Science, pages 51-65. Springer, 2005. URL: https://doi.org/10.1007/11539452_8.
  40. Jim Laird. From global to local state, coalgebraically and compositionally. In Barbara König, editor, Proceedings of the Thirty-Fifth Conference on the Mathematical Foundations of Programming Semantics, MFPS 2019, London, UK, June 4-7, 2019, volume 347 of Electronic Notes in Theoretical Computer Science, pages 203-222. Elsevier, 2019. URL: https://doi.org/10.1016/J.ENTCS.2019.09.011.
  41. Joachim Lambek and Philip J Scott. Introduction to higher-order categorical logic, volume 7. Cambridge University Press, 1988. Google Scholar
  42. The Rust Standard Library. Module mpsc, Rust documentation. https://doc.rust-lang.org/stable/std/sync/mpsc/. Last accessed: 2025-12-26.
  43. Tiange Liu, Alwen Tiu, and Ross Horne. Open bisimilarity for the π-calculus with mismatch. In 36th Conf. on Concurrency Theory (CONCUR), volume 348 of LIPIcs, pages 30:1-30:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2025. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2025.30.
  44. Paul-André Melliès. Asynchronous games 3 an innocent model of linear logic. In Lars Birkedal, editor, Proceedings of the 10th Conference on Category Theory in Computer Science, CTCS 2004, Copenhagen, Denmark, August 12-14, 2004, volume 122 of Electronic Notes in Theoretical Computer Science, pages 171-192. Elsevier, 2004. URL: https://doi.org/10.1016/J.ENTCS.2004.06.057.
  45. Massimo Merro. On equators in asynchronous name-passing calculi without matching. In Ilaria Castellani and Björn Victor, editors, 6th International Workshop on Expressiveness in Concurrency, EXPRESS 1999, Eindhoven, The Netherlands, August 23, 1999, volume 27 of Electronic Notes in Theoretical Computer Science, pages 57-70. Elsevier, 1999. URL: https://doi.org/10.1016/S1571-0661(05)80295-6.
  46. Massimo Merro and Davide Sangiorgi. On asynchrony in name-passing calculi. In Proc. 25th ICALP, volume 1443 of Lecture Notes in Computer Science. Springer Verlag, 1998. URL: https://doi.org/10.1007/BFB0055108.
  47. Massimo Merro and Davide Sangiorgi. On asynchrony in name-passing calculi. Mathematical Structures in Computer Science, 14(5):715-767, 2004. URL: https://doi.org/10.1017/S0960129504004323.
  48. Robin Milner. Functions as processes. Research Report RR-1154, INRIA, 1990. URL: https://hal.inria.fr/inria-00075405.
  49. Robin Milner. Functions as processes. Math. Struct. Comput. Sci., 2(2):119-141, 1992. URL: https://doi.org/10.1017/S0960129500001407.
  50. Dimitris Mostrous, Nobuko Yoshida, and Kohei Honda. Global principal typing in partially commutative asynchronous sessions. In Giuseppe Castagna, editor, Programming Languages and Systems, 18th European Symposium on Programming, ESOP 2009, York, UK, March 22-29, 2009. Proceedings, volume 5502 of Lecture Notes in Computer Science, pages 316-332. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-00590-9_23.
  51. Jorge A. Pérez, Luís Caires, Frank Pfenning, and Bernardo Toninho. Linear logical relations and observational equivalences for session-based concurrency. Inf. Comput., 239:254-302, 2014. URL: https://doi.org/10.1016/J.IC.2014.08.001.
  52. Ken Sakayori and Davide Sangiorgi. Extensional and non-extensional functions as processes. Log. Methods Comput. Sci., 21(3), 2025. URL: https://doi.org/10.46298/LMCS-21(3:25)2025.
  53. Ken Sakayori and Takeshi Tsukada. A truly concurrent game model of the asynchronous pi -calculus. In Javier Esparza and Andrzej S. Murawski, editors, Foundations of Software Science and Computation Structures - 20th International Conference, FOSSACS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, volume 10203 of Lecture Notes in Computer Science, pages 389-406, 2017. URL: https://doi.org/10.1007/978-3-662-54458-7_23.
  54. Ken Sakayori and Takeshi Tsukada. A categorical model of an i/o-typed pi-calculus. In Luís Caires, editor, Programming Languages and Systems - 28th European Symposium on Programming, ESOP 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, volume 11423 of Lecture Notes in Computer Science, pages 640-667. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-17184-1_23.
  55. Ken Sakayori and Takeshi Tsukada. Output without delay: A π-calculus compatible with categorical semantics. In Naoki Kobayashi, editor, 6th International Conference on Formal Structures for Computation and Deduction, FSCD 2021, Buenos Aires, Argentina (Virtual Conference), July 17-24, 2021, volume 195 of LIPIcs, pages 32:1-32:22. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPIcs.FSCD.2021.32.
  56. Davide Sangiorgi. A theory of bisimulation for the pi-calculus. In Eike Best, editor, Proc. CONCUR '93, volume 715 of Lecture Notes in Computer Science, pages 127-142. Springer, 1993. URL: https://doi.org/10.1007/3-540-57208-2_10.
  57. Davide Sangiorgi. π-Calculus, internal mobility, and agent-passing calculi. Theor. Comput. Sci., 167(1&2):235-274, 1996. URL: https://doi.org/10.1016/0304-3975(96)00075-8.
  58. Davide Sangiorgi. The name discipline of uniform receptiveness. In Proc. 24th ICALP, volume 1256 of Lecture Notes in Computer Science. Springer Verlag, 1997. URL: https://doi.org/10.1016/S0304-3975(99)00040-7.
  59. Davide Sangiorgi and David Walker. The π-calculus - A Theory of Mobile Processes. Cambridge University Press, 2001. URL: https://doi.org/10.1017/9781316134924.
  60. Ian Stark. A fully abstract domain model for the pi-calculus. In Proceedings, 11th Annual IEEE Symposium on Logic in Computer Science, New Brunswick, New Jersey, USA, July 27-30, 1996, pages 36-42. IEEE Computer Society, 1996. URL: https://doi.org/10.1109/LICS.1996.561301.
  61. Alwen Tiu and Jeremy E. Dawson. Automating open bisimulation checking for the spi calculus. In 23rd IEEE Computer Security Foundations Symposium, pages 307-321. IEEE Computer Society, 2010. URL: https://doi.org/10.1109/CSF.2010.28.
  62. Alwen Tiu and Dale Miller. Proof search specifications of bisimulation and modal logics for the pi-calculus. ACM Trans. Comput. Log., 11(2):13:1-13:35, 2010. URL: https://doi.org/10.1145/1656242.1656248.
  63. Vasco T. Vasconcelos. Fundamentals of session types. Inf. Comput., 217:52-70, 2012. URL: https://doi.org/10.1016/J.IC.2012.05.002.
  64. Björn Victor and Faron Moller. The mobility workbench - A tool for the pi-calculus. In David L. Dill, editor, Computer Aided Verification (CAV), volume 818 of Lecture Notes in Computer Science, pages 428-440. Springer, 1994. URL: https://doi.org/10.1007/3-540-58179-0_73.
  65. Philip Wadler. Propositions as sessions. J. Funct. Program., 24(2-3):384-418, 2014. URL: https://doi.org/10.1017/S095679681400001X.
  66. David Walker. Pi-calculus semantics of object-oriented programming languages. In Takayasu Ito and Albert R. Meyer, editors, Theoretical Aspects of Computer Software, International Conference TACS '91, Sendai, Japan, September 24-27, 1991, Proceedings, volume 526 of Lecture Notes in Computer Science, pages 532-547. Springer, 1991. URL: https://doi.org/10.1007/3-540-54415-1_63.
  67. Nobuko Yoshida. Minimality and separation results on asynchronous mobile processes - representability theorems by concurrent combinators. Theor. Comput. Sci., 274(1-2):231-276, 2002. URL: https://doi.org/10.1016/S0304-3975(00)00310-8.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact