Document Open Access Logo

Functions and References in the Pi-Calculus: Full Abstraction and Proof Techniques

Author Enguerrand Prebet

PDF

File

Thumbnail PDF
PDF
LIPIcs.ICALP.2022.130.pdf
  • Filesize: 0.78 MB
  • 19 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Semantics and reasoning
Keywords
  • Call-by-value λ-calculus
  • imperative Programming
  • π-calculus
  • Bisimulation
  • Type System

Metrics

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

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

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

Author Details

Enguerrand Prebet
  • Université de Lyon, ENS de Lyon, UCB Lyon 1, CNRS, INRIA, LIP

Funding

This work has been supported by the Université Franco-Italienne under the programme Vinci 2020.

Acknowledgements

Many thanks to Daniel Hirschkoff and Davide Sangiorgi for fruitful discussions and helpful comments on earlier versions of this article.

References

  1. Martin Berger, Kohei Honda, and Nobuko Yoshida. Sequentiality and the pi-calculus. In Samson Abramsky, editor, Typed Lambda Calculi and Applications, 5th International Conference, TLCA 2001, Proceedings, volume 2044 of Lecture Notes in Computer Science, pages 29-45. Springer, 2001. URL: https://doi.org/10.1007/3-540-45413-6_7.
  2. Dariusz Biernacki, Sergueï Lenglet, and Piotr Polesiuk. A complete normal-form bisimilarity for state. In Mikolaj Bojanczyk and Alex Simpson, editors, Foundations of Software Science and Computation Structures - 22nd International Conference, FOSSACS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, volume 11425 of Lecture Notes in Computer Science, pages 98-114. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-17127-8_6.
  3. Adrien Durier, Daniel Hirschkoff, and Davide Sangiorgi. Eager Functions as Processes (long version). working paper or preprint, December 2021. URL: https://hal.archives-ouvertes.fr/hal-03466150.
  4. Daniel Hirschkoff, Enguerrand Prebet, and Davide Sangiorgi. On the representation of references in the pi-calculus. In Igor Konnov and Laura Kovács, editors, 31st International Conference on Concurrency Theory, CONCUR 2020, volume 171 of LIPIcs, pages 34:1-34:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2020.34.
  5. 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.
  6. Guilhem Jaber. Syteci: automating contextual equivalence for higher-order programs with references. Proc. ACM Program. Lang., 4(POPL):59:1-59:28, 2020. URL: https://doi.org/10.1145/3371127.
  7. Guilhem Jaber and Davide Sangiorgi. Games, mobile processes, and functions. In 30th EACSL Annual Conference on Computer Science Logic (CSL 2022)., Göttingen, Germany, February 2022. URL: https://hal.archives-ouvertes.fr/hal-03407123.
  8. Vasileios Koutavas, Yu-Yang Lin, and Nikos Tzevelekos. From bounded checking to verification of equivalence via symbolic up-to techniques. In Dana Fisman and Grigore Rosu, editors, Tools and Algorithms for the Construction and Analysis of Systems - 28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings, Part II, volume 13244 of Lecture Notes in Computer Science, pages 178-195. Springer, 2022. URL: https://doi.org/10.1007/978-3-030-99527-0_10.
  9. 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.
  10. Jean-Marie Madiot, Damien Pous, and Davide Sangiorgi. Bisimulations up-to: Beyond first-order transition systems. In Paolo Baldan and Daniele Gorla, editors, CONCUR 2014 - Concurrency Theory - 25th International Conference, CONCUR 2014. Proceedings, volume 8704 of Lecture Notes in Computer Science, pages 93-108. Springer, 2014. URL: https://doi.org/10.1007/978-3-662-44584-6_8.
  11. Robin Milner. Functions as processes. Math. Struct. Comput. Sci., 2(2):119-141, 1992. URL: https://doi.org/10.1017/S0960129500001407.
  12. Andrzej S. Murawski and Nikos Tzevelekos. Game semantics for good general references. In Proceedings of the 26th Annual IEEE Symposium on Logic in Computer Science, LICS 2011, June 21-24, 2011, Toronto, Ontario, Canada, pages 75-84. IEEE Computer Society, 2011. URL: https://doi.org/10.1109/LICS.2011.31.
  13. Andrzej S. Murawski and Nikos Tzevelekos. Algorithmic games for full ground references. Formal Methods Syst. Des., 52(3):277-314, 2018. URL: https://doi.org/10.1007/s10703-017-0292-9.
  14. Andrzej S. Murawski and Nikos Tzevelekos. Game Semantics for Interface Middleweight Java. J. ACM, 68(1):4:1-4:51, 2021. URL: https://doi.org/10.1145/3428676.
  15. Gordon D. Plotkin. Call-by-name, call-by-value and the lambda-calculus. Theor. Comput. Sci., 1(2):125-159, 1975. URL: https://doi.org/10.1016/0304-3975(75)90017-1.
  16. Damien Pous. Coinduction all the way up. 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 307-316. ACM, 2016. URL: https://doi.org/10.1145/2933575.2934564.
  17. Davide Sangiorgi. Locality and interleaving semantics in calculi for mobile processes. Theor. Comput. Sci., 155(1):39-83, 1996. URL: https://doi.org/10.1016/0304-3975(95)00020-8.
  18. Davide Sangiorgi. Lazy functions and mobile processes. In Gordon D. Plotkin, Colin Stirling, and Mads Tofte, editors, Proof, Language, and Interaction, Essays in Honour of Robin Milner, pages 691-720. The MIT Press, 2000. Google Scholar
  19. Davide Sangiorgi and David Walker. The Pi-Calculus - a theory of mobile processes. Cambridge University Press, 2001. Google Scholar
  20. Kristian Støvring and Søren B. Lassen. A complete, co-inductive syntactic theory of sequential control and state. In Martin Hofmann and Matthias Felleisen, editors, Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2007, Nice, France, January 17-19, 2007, pages 161-172. ACM, 2007. URL: https://doi.org/10.1145/1190216.1190244.
  21. Bernardo Toninho and Nobuko Yoshida. On polymorphic sessions and functions: A tale of two (fully abstract) encodings. ACM Trans. Program. Lang. Syst., 43(2):7:1-7:55, 2021. URL: https://doi.org/10.1145/3457884.
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