Document Open Access Logo

First-Order Store and Visibility in Name-Passing Calculi

Authors Daniel Hirschkoff , Iwan Quémerais , Davide Sangiorgi

PDF

File

Thumbnail PDF
PDF
LIPIcs.CONCUR.2025.23.pdf
  • Filesize: 0.85 MB
  • 21 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Process calculi
Keywords
  • process calculi
  • behavioural equivalence
  • type system

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

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

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

Author Details

Daniel Hirschkoff
  • LIP, ENS de Lyon, France
Iwan Quémerais
  • LIP, ENS de Lyon, France
Davide Sangiorgi
  • Università di Bologna, Italy
  • INRIA, Sophia Antipolis, France

Funding

Work partly supported by the MIUR-PRIN project "Resource Awareness in Programming: Algebra, Rewriting, and Analysis" (RAP, ID P2022HXNSC).

Acknowledgements

We have benefited from discussions with G. Jaber and E. Prebet.

References

  1. Davide Ancona, Viviana Bono, Mario Bravetti, Joana Campos, Giuseppe Castagna, Pierre-Malo Deniélou, Simon J. Gay, Nils Gesbert, Elena Giachino, Raymond Hu, Einar Broch Johnsen, Francisco Martins, Viviana Mascardi, Fabrizio Montesi, Rumyana Neykova, Nicholas Ng, Luca Padovani, Vasco T. Vasconcelos, and Nobuko Yoshida. Behavioral types in programming languages. Found. Trends Program. Lang., 3(2-3):95-230, 2016. URL: https://doi.org/10.1561/2500000031.
  2. 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.
  3. Daniel Hirschkoff, Enguerrand Prebet, and Davide Sangiorgi. On sequentiality and well-bracketing in the π-calculus. In 2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). IEEE, June 2021. URL: https://doi.org/10.1109/lics52264.2021.9470559.
  4. Daniel Hirschkoff, Iwan Quémerais, and Davide Sangiorgi. First-order store and visibility in name-passing calculi. CoRR, abs/2504.17350, 2025. Extended online version of this paper. URL: https://doi.org/10.48550/arXiv.2504.17350.
  5. Kohei Honda. Processes and games. In Fabio Gadducci and Ugo Montanari, editors, Fourth International Workshop on Rewriting logic and Its Applications, WRLA2002, Pisa, Italy, 19-21, 2002, volume 71 of Electronic Notes in Theoretical Computer Science, pages 40-69. Elsevier, 2002. URL: https://doi.org/10.1016/S1571-0661(05)82528-9.
  6. Kohei Honda, Vasco Thudichum Vasconcelos, and Makoto Kubo. Language primitives and type discipline for structured communication-based programming. In Chris Hankin, editor, Programming Languages and Systems - ESOP'98, 7th European Symposium on Programming, Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS'98, Lisbon, Portugal, March 28 - April 4, 1998, Proceedings, volume 1381 of Lecture Notes in Computer Science, pages 122-138. Springer, 1998. URL: https://doi.org/10.1007/BFB0053567.
  7. Guilhem Jaber and Andrzej S. Murawski. Complete trace models of state and control. In Programming Languages and Systems: 30th European Symposium on Programming, ESOP 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 – April 1, 2021, Proceedings, pages 348-374, Berlin, Heidelberg, 2021. Springer-Verlag. URL: https://doi.org/10.1007/978-3-030-72019-3_13.
  8. Guilhem Jaber and Davide Sangiorgi. Games, Mobile Processes, and functions. In CSL 2022 - 30th EACSL Annual Conference on Computer Science Logic, pages 1-35, Göttingen, Germany, February 2022. URL: https://hal.science/hal-03407123.
  9. Guilhem Jaber and Nikos Tzevelekos. Trace semantics for polymorphic references. In Martin Grohe, Eric Koskinen, and Natarajan Shankar, editors, Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '16, New York, NY, USA, July 5-8, 2016, pages 585-594. ACM, 2016. URL: https://doi.org/10.1145/2933575.2934509.
  10. Ohad Kammar, Paul B. Levy, Sean K. Moss, and Sam Staton. A monad for full ground reference cells. In 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), Reykjavik, Iceland, 2017. IEEE. URL: https://doi.org/10.1109/LICS.2017.8005109.
  11. 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.
  12. Naoki Kobayashi and Davide Sangiorgi. A hybrid type system for lock-freedom of mobile processes. ACM Trans. Program. Lang. Syst., 32(5):16:1-16:49, 2010. URL: https://doi.org/10.1145/1745312.1745313.
  13. James Laird. A fully abstract trace semantics for general references. In Lars Arge, Christian Cachin, Tomasz Jurdzinski, and Andrzej Tarlecki, editors, Automata, Languages and Programming, 34th International Colloquium, ICALP 2007, Wroclaw, Poland, July 9-13, 2007, Proceedings, volume 4596 of Lecture Notes in Computer Science, pages 667-679. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-73420-8_58.
  14. Paul-André Melliès and Nicolas Tabareau. An algebraic account of references in game semantics. In Samson Abramsky, Michael W. Mislove, and Catuscia Palamidessi, editors, Proceedings of the 25th Conference on Mathematical Foundations of Programming Semantics, MFPS 2009, Oxford, UK, April 3-7, 2009, volume 249 of Electronic Notes in Theoretical Computer Science, pages 377-405. Elsevier, 2009. URL: https://doi.org/10.1016/J.ENTCS.2009.07.099.
  15. R. Milner. The polyadic π-calculus: a tutorial. Technical Report ECS-LFCS-91-180, LFCS, 1991. Also in Logic and Algebra of Specification, ed. F.L. Bauer, W. Brauer and H. Schwichtenberg, Springer Verlag, 1993. Google Scholar
  16. Robin Milner. Functions as processes. Mathematical Structures in Computer Science, 2(2):119-141, June 1992. URL: https://doi.org/10.1017/S0960129500001407.
  17. Andrzej S. Murawski and Nikos Tzevelekos. Algorithmic games for full ground references. Formal Methods in System Design, 52(3):277-314, 2018. URL: https://doi.org/10.1007/s10703-017-0292-9.
  18. Luca Padovani. Deadlock and lock freedom in the linear π-calculus. In Thomas A. Henzinger and Dale Miller, editors, Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS '14, Vienna, Austria, July 14 - 18, 2014, pages 72:1-72:10. ACM, 2014. URL: https://doi.org/10.1145/2603088.2603116.
  19. Benjamin C. Pierce and Davide Sangiorgi. Typing and subtyping for mobile processes. Math. Struct. Comput. Sci., 6(5):409-453, 1996. URL: https://doi.org/10.1017/S096012950007002X.
  20. Enguerrand Prebet. Typed Behavioural Equivalences in the Pi-Calculus. Theses, Ecole normale supérieure de lyon - ENS LYON ; Università degli studi (Bologne, Italie), September 2022. URL: https://hal.science/tel-03920089.
  21. Davide Sangiorgi. The lazy lambda calculus in a concurrency scenario. Inf. Comput., 111(1):120-153, 1994. URL: https://doi.org/10.1006/INCO.1994.1042.
  22. Davide Sangiorgi. pi-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.
  23. Davide Sangiorgi. The name discipline of uniform receptiveness. Theor. Comput. Sci., 221(1-2):457-493, 1999. URL: https://doi.org/10.1016/S0304-3975(99)00040-7.
  24. Nobuko Yoshida, Martin Berger, and Kohei Honda. Strong normalisation in the pi -calculus. Inf. Comput., 191(2):145-202, 2004. URL: https://doi.org/10.1016/J.IC.2003.08.004.
  25. Nobuko Yoshida, Simon Castellan, and Léo Stefanesco. Game semantics: Easy as pi. CoRR, abs/2011.05248, 2020. URL: https://arxiv.org/abs/2011.05248.
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