Document Open Access Logo

Games, Mobile Processes, and Functions

Authors Guilhem Jaber, Davide Sangiorgi

PDF

File

Thumbnail PDF
PDF
LIPIcs.CSL.2022.25.pdf
  • Filesize: 0.68 MB
  • 18 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Program semantics
Keywords
  • λ-calculus
  • π-calculus
  • game semantics

Metrics

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

Abstract

We establish a tight connection between two models of the λ-calculus, namely Milner’s encoding into the π-calculus (precisely, the Internal π-calculus), and operational game semantics (OGS). We first investigate the operational correspondence between the behaviours of the encoding provided by π and OGS. 
We do so for various LTSs: the standard LTS for π and a new "concurrent" LTS for OGS; an "output-prioritised" LTS for π and the standard alternating LTS for OGS. We then show that the equivalences induced on λ-terms by all these LTSs (for π and OGS) coincide. 
These connections allow us to transfer results and techniques between π and OGS. In particular we import up-to techniques from π onto OGS and we derive congruence and compositionality results for OGS from those of π. The study is illustrated for call-by-value; similar results hold for call-by-name.

Cite As Get BibTex

Guilhem Jaber and Davide Sangiorgi. Games, Mobile Processes, and Functions. In 30th EACSL Annual Conference on Computer Science Logic (CSL 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 216, pp. 25:1-25:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022) https://doi.org/10.4230/LIPIcs.CSL.2022.25

Author Details

Guilhem Jaber
  • Université de Nantes, France
Davide Sangiorgi
  • Università di Bologna, Italy
  • Inria Sophia Antipolis, France

Funding

  • Sangiorgi, Davide: supported by the MIUR-PRIN project "Analysis of Program Analyses" (ASPRA, ID 201784YSZ5_004).

References

  1. Samson Abramsky. The lazy lambda calculus. In D. Turner, editor, Research Topics in Functional Programming, pages 65-116. Addison-Wesley, 1989. Google Scholar
  2. Samson Abramsky. Game semantics for programming languages (abstract). In Proceedings of the 22nd International Symposium on Mathematical Foundations of Computer Science, MFCS '97, pages 3-4, Berlin, Heidelberg, 1997. Springer-Verlag. Google Scholar
  3. Samson Abramsky, Kohei Honda, and Guy McCusker. A fully abstract game semantics for general references. In Proceedings of the 13th Annual IEEE Symposium on Logic in Computer Science, LICS '98, page 334, USA, 1998. IEEE Computer Society. Google Scholar
  4. Samson Abramsky, Radha Jagadeesan, and Pasquale Malacaria. Full abstraction for pcf. Inf. Comput., 163(2):409-470, December 2000. URL: https://doi.org/10.1006/inco.2000.2930.
  5. Samson Abramsky and Guy McCusker. Linearity, sharing and state: a fully abstract game semantics for Idealized Algol with active expressions. In Algol-like languages, pages 297-329. Springer, 1997. Google Scholar
  6. Martin Berger, Kohei Honda, and Nobuko Yoshida. Sequentiality and the π-calculus. In International Conference on Typed Lambda Calculi and Applications, pages 29-45. Springer, 2001. Google Scholar
  7. Dariusz Biernacki, Sergueï Lenglet, and Piotr Polesiuk. A complete normal-form bisimilarity for state. In International Conference on Foundations of Software Science and Computation Structures, pages 98-114. Springer, 2019. Google Scholar
  8. 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., January 2019. URL: https://doi.org/10.1145/3290340.
  9. Tim Disney and Cormac Flanagan. Game semantics for type soundness. In Proceedings of the 2015 30th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), LICS '15, pages 104-114, USA, 2015. IEEE Computer Society. URL: https://doi.org/10.1109/LICS.2015.20.
  10. Adrien Durier. Unique solution techniques for processes and functions. PhD thesis, University of Lyon, France, 2020. Google Scholar
  11. Adrien Durier, Daniel Hirschkoff, and Davide Sangiorgi. Eager functions as processes. In 33nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018. IEEE Computer Society, 2018. Google Scholar
  12. Clovis Eberhart, Tom Hirschowitz, and Thomas Seiller. An intensionally fully-abstract sheaf model for pi. In 6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015). Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2015. Google Scholar
  13. Thomas Ehrhard. An introduction to differential linear logic: proof-nets, models and antiderivatives. Mathematical Structures in Computer Science, 28(7):995-1060, 2018. Google Scholar
  14. Marcelo Fiore and Kohei Honda. Recursive types in games: Axiomatics and process representation. In Proceedings of the 13th Annual IEEE Symposium on Logic in Computer Science, LICS ’98, page 345, USA, 1998. IEEE Computer Society. Google Scholar
  15. Dan R. Ghica and Andrzej S. Murawski. Angelic semantics of fine-grained concurrency. In International Conference on Foundations of Software Science and Computation Structures, pages 211-225. Springer, 2004. Google Scholar
  16. Dan R. Ghica and Nikos Tzevelekos. A system-level game semantics. Electron. Notes Theor. Comput. Sci., 286:191-211, September 2012. URL: https://doi.org/10.1016/j.entcs.2012.08.013.
  17. Kohei Honda. Processes and games. Electron. Notes Theor. Comput. Sci., 71:40-69, 2002. URL: https://doi.org/10.1016/S1571-0661(05)82528-9.
  18. Kohei Honda and Nobuko Yoshida. Game-theoretic analysis of call-by-value computation. Theor. Comput. Sci., 221(1–2):393-456, June 1999. URL: https://doi.org/10.1016/S0304-3975(99)00039-0.
  19. J. M. E. Hyland and C.-H. L. Ong. Pi-calculus, dialogue games and full abstraction PCF. In Proceedings of the Seventh International Conference on Functional Programming Languages and Computer Architecture, FPCA ’95, pages 96-107, New York, NY, USA, 1995. Association for Computing Machinery. URL: https://doi.org/10.1145/224164.224189.
  20. J.M.E. Hyland and C.-H. L. Ong. On full abstraction for PCF. Inf. Comput., 163(2):285-408, December 2000. URL: https://doi.org/10.1006/inco.2000.2917.
  21. Guilhem Jaber and Davide Sangiorgi. Games, mobile processes, and functions (long version), 2021. URL: https://hal.archives-ouvertes.fr/hal-03407123.
  22. Guilhem Jaber and Nikos Tzevelekos. Trace semantics for polymorphic references. In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '16, pages 585-594, New York, NY, USA, 2016. Association for Computing Machinery. URL: https://doi.org/10.1145/2933575.2934509.
  23. Radha Jagadeesan, Corin Pitcher, and James Riely. Open bisimulation for aspects. In Transactions on Aspect-Oriented Software Development V, pages 72-132. Springer, 2009. Google Scholar
  24. Alan Jeffrey and Julian Rathke. Java jr: Fully abstract trace semantics for a core java language. In European symposium on programming, pages 423-438. Springer, 2005. Google Scholar
  25. James Laird. Full abstraction for functional languages with control. In Proceedings of the 12th Annual IEEE Symposium on Logic in Computer Science, LICS '97, page 58, USA, 1997. IEEE Computer Society. Google Scholar
  26. James Laird. A game semantics of the asynchronous π-calculus. In International Conference on Concurrency Theory, pages 51-65. Springer, 2005. Google Scholar
  27. James Laird. Game semantics for higher-order concurrency. In Proceedings of the 26th International Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS'06, pages 417-428, Berlin, Heidelberg, 2006. Springer-Verlag. URL: https://doi.org/10.1007/11944836.38.
  28. James Laird. A fully abstract trace semantics for general references. In Proceedings of the 34th International Conference on Automata, Languages and Programming, ICALP’07, pages 667-679, Berlin, Heidelberg, 2007. Springer-Verlag. Google Scholar
  29. Søren B. Lassen. Eager normal form bisimulation. In 20th IEEE Symposium on Logic in Computer Science (LICS 2005), 26-29 June 2005, Chicago, IL, USA, Proceedings, pages 345-354, 2005. URL: https://doi.org/10.1109/LICS.2005.15.
  30. Paul Blain Levy and Sam Staton. Transition systems over games. In Proceedings of the 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, New York, NY, USA, 2014. Association for Computing Machinery. URL: https://doi.org/10.1145/2603088.2603150.
  31. R. Milner. Communication and Concurrency. Prentice Hall, 1989. Google Scholar
  32. 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
  33. R. Milner. Functions as processes. MSCS, 2(2):119-141, 1992. Google Scholar
  34. B. Pierce and D. Sangiorgi. Typing and subtyping for mobile processes. MSCS, 6(5):409-454, 1996. Google Scholar
  35. G.D. Plotkin. Call by name, call by value and the λ-calculus. TCS, 1:125-159, 1975. Google Scholar
  36. Damien Pous and Davide Sangiorgi. Enhancements of the bisimulation proof method. In Davide Sangiorgi and Jan Rutten, editors, Advanced Topics in Bisimulation and Coinduction. Cambridge University Press, 2012. Google Scholar
  37. Damien Pous and Davide Sangiorgi. Bisimulation and coinduction enhancements: A historical perspective. Formal Asp. Comput., 31(6):733-749, 2019. URL: https://doi.org/10.1007/s00165-019-00497-w.
  38. Ken Sakayori and Takeshi Tsukada. A truly concurrent game model of the asynchronous π-calculus. In International Conference on Foundations of Software Science and Computation Structures, pages 389-406. Springer, 2017. Google Scholar
  39. Ken Sakayori and Takeshi Tsukada. A categorical model of an i/o-typed π-calculus. In European Symposium on Programming, pages 640-667. Springer, 2019. Google Scholar
  40. D. Sangiorgi. Locality and non-interleaving semantics in calculi for mobile processes. TCS, 155:39-83, 1996. Google Scholar
  41. D. Sangiorgi. π-calculus, internal mobility and agent-passing calculi. TCS, 167(2):235-274, 1996. Google Scholar
  42. D. Sangiorgi. Lazy functions and mobile processes. In G. Plotkin, C. Stirling, and M. Tofte, editors, Proof, Language and Interaction: Essays in Honour of Robin Milner. MIT Press, 2000. Google Scholar
  43. Kristian Støvring and Soren B. Lassen. A complete, co-inductive syntactic theory of sequential control and state. In Proceedings of the 34th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’07, pages 161-172, New York, NY, USA, 2007. Association for Computing Machinery. URL: https://doi.org/10.1145/1190216.1190244.
  44. Glynn Winskel, Silvain Rideau, Pierre Clairambault, and Simon Castellan. Games and strategies as event structures. Logical Methods in Computer Science, 13, 2017. Google Scholar
  45. Nobuko Yoshida, Martin Berger, and Kohei Honda. Strong normalisation in the π-Calculus. In 16th Annual IEEE Symposium on Logic in Computer Science (LICS'01), pages 311-322. IEEE Computer Society, 2001. Google Scholar
  46. Nobuko Yoshida, Simon Castellan, and Léo Stefanesco. Game semantics: Easy as pi. arXiv preprint, 2020. URL: http://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