Document Open Access Logo

Towards A Rosetta Stone of Interactive and Quantitative Semantics (Invited Talk)

Author Pierre Clairambault

PDF

File

Thumbnail PDF
PDF
LIPIcs.CSL.2026.4.pdf
  • Filesize: 417 kB
  • 4 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Denotational semantics
Keywords
  • Denotational semantics
  • Game semantics

Metrics

Abstract

Quantitative semantics are those denotational semantics that inherit from linear logic [Jean-Yves Girard, 1987] a sensitivity to the multiplicity of resources involved in computation. Those include the relational model [Jean-Yves Girard, 1987] and its numerous variations (such as finiteness spaces [Thomas Ehrhard, 2005], weighted relational models [Jim Laird et al., 2013] and their extensions [Thomas Ehrhard et al., 2011; Thomas Ehrhard, 2002], generalized species of structure [Fiore et al., 2008], span models [Paul-André Melliès, 2019; Pierre Clairambault and Simon Forest, 2023], etc), as well as related syntactic methods such as non-idempotent intersection types [Daniel de Carvalho, 2018] and Taylor expansion of lambda-terms [Thomas Ehrhard and Laurent Regnier, 2003]. Interactive semantics are usually also quantitative, but in addition they present the interactive behaviour of proofs and programs, generally organized chronologically - those include the many variants of game semantics (starting with [J. M. E. Hyland and C.-H. Luke Ong, 2000; Samson Abramsky et al., 2000]), and other frameworks such as Geometry of Interaction [Girard, 1989] or ludics [Jean-Yves Girard, 2001]. Both families are cornerstones of modern denotational semantics, and both have associated Alonzo Church awards: game semantics in 2017, and quantitative semantics (in particular, differential linear logic and the differential λ-calculus) in 2024.
It has more or less always been clear to the experts that the two, sharing an origin in linear logic, are conceptually related. Yet there are differences, which seem fundamental: in particular, while quantitative models compose relationally, the composition of strategies follows an intricate "parallel interaction plus hiding" process inspired from concurrency theory [Abramsky, 1997]. The two families of models have also historically targeted different kinds of languages: whereas quantitative semantics focused on theoretical calculi (and the λ-calculus in particular), game semantics is known for fully abstract models for languages with elaborate combinations of effects including local state [Samson Abramsky and Guy McCusker, 1996], control operators [James Laird, 1997], and concurrent primitives [Dan R. Ghica and Andrzej S. Murawski, 2008]. Early on, researchers have explored the relationship between the two [Thomas Ehrhard, 1996; Patrick Baillot et al., 1997], and investigations on this question have spanned decades [Pierre Boudes, 2009; Ana C. Calderon and Guy McCusker, 2010; Takeshi Tsukada and C.-H. Luke Ong, 2016; C.-H. Luke Ong, 2017]. In particular, Melliès' work on asynchronous games [Paul-André Melliès, 2006; Paul-André Melliès, 2005] made significant conceptual contributions, showing that the issue was enlightened by adopting a positional formulation of game semantics, where points in the relational model simply arise as certain positions.
This talk surveys recent developments in this line of work, shedding light on the connection between those two families. Our work is set in so-called "thin concurrent games" [Simon Castellan et al., 2019; Pierre Clairambault, 2024], an extension with symmetry of Rideau and Winskel’s concurrent games on event structures [Silvain Rideau and Glynn Winskel, 2011]. Event structures being one of the main "truly concurrent" models of concurrency [Glynn Winskel, 1986], it is perhaps expected that thin concurrent games can model concurrent languages: they provide a truly concurrent refinement of Ghica and Murawski’s fully abstract model of Idealized Concurrent Algol [Simon Castellan and Pierre Clairambault, 2024; Pierre Clairambault, 2024]. But beyond the semantics of concurrency, thin concurrent games are also a deep reworking on game semantics built from causal principles, inheriting from asynchronous games a positional flavour. In thin concurrent games, strategies have a dual nature: an event-based nature where they appear as certain event structures composed via parallel interaction plus hiding; or a positional nature where they appear as certain spans of groupoids, composed by pullback (modulo a technical condition on strategies called visibility) - they can be regarded both as a games and a relational model!
Leveraging this dual nature, in a sequence of papers with Castellan, de Visme, Olimpieri and Paquet, we have been able to link the single framework of thin concurrent games with numerous other models. This includes various traditional alternating or non-alternating games models [Simon Castellan and Pierre Clairambault, 2024; Pierre Clairambault, 2024], the weighted relational model [Pierre Clairambault and Hugo Paquet, 2021], the quantum relational model [Pierre Clairambault and Marc de Visme, 2020], generalized species of structure [Pierre Clairambault et al., 2023], and - going beyond quantitative semantics - the linear Scott model [Clairambault, 2025], a linear decomposition of standard Scott domain semantics [Thomas Ehrhard, 2012]. All these distinct models are obtained by projecting away certain aspects of thin concurrent games, giving some support to the claim that thin concurrent games are a Rosetta stone for interactive and quantitative semantics.

Cite As Get BibTex

Pierre Clairambault. Towards A Rosetta Stone of Interactive and Quantitative Semantics (Invited Talk). In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 4:1-4:4, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.CSL.2026.4

Author Details

Pierre Clairambault
  • CNRS, Aix Marseille Univ, LIS, France

References

  1. Samson Abramsky. Semantics of interaction: an introduction to game semantics. In Semantics and Logics of Computation. Cambridge University Press, 1997. Google Scholar
  2. Samson Abramsky, Radha Jagadeesan, and Pasquale Malacaria. Full abstraction for PCF. Inf. Comput., 163(2):409-470, 2000. URL: https://doi.org/10.1006/INCO.2000.2930.
  3. Samson Abramsky and Guy McCusker. Linearity, sharing and state: a fully abstract game semantics for idealized algol with active expressions. In Jean-Yves Girard, Mitsuhiro Okada, and Andre Scedrov, editors, Linear Logic Tokyo Meeting 1996, Keio University, Mita Campus, Tokyo, Japan, March 29 - April 2, 1996, volume 3 of Electronic Notes in Theoretical Computer Science, pages 2-14. Elsevier, 1996. URL: https://doi.org/10.1016/S1571-0661(05)80398-6.
  4. Patrick Baillot, Vincent Danos, Thomas Ehrhard, and Laurent Regnier. Timeless games. In Mogens Nielsen and Wolfgang Thomas, editors, Computer Science Logic, 11th International Workshop, CSL '97, Annual Conference of the EACSL, Aarhus, Denmark, August 23-29, 1997, Selected Papers, volume 1414 of Lecture Notes in Computer Science, pages 56-77. Springer, 1997. URL: https://doi.org/10.1007/BFB0028007.
  5. Pierre Boudes. Thick subtrees, games and experiments. In Pierre-Louis Curien, editor, Typed Lambda Calculi and Applications, 9th International Conference, TLCA 2009, Brasilia, Brazil, July 1-3, 2009. Proceedings, volume 5608 of Lecture Notes in Computer Science, pages 65-79. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-02273-9_7.
  6. Ana C. Calderon and Guy McCusker. Understanding game semantics through coherence spaces. In Michael W. Mislove and Peter Selinger, editors, Proceedings of the 26th Conference on the Mathematical Foundations of Programming Semantics, MFPS 2010, Ottawa, Ontario, Canada, May 6-10, 2010, volume 265 of Electronic Notes in Theoretical Computer Science, pages 231-244. Elsevier, 2010. URL: https://doi.org/10.1016/J.ENTCS.2010.08.014.
  7. Simon Castellan and Pierre Clairambault. Disentangling parallelism and interference in game semantics. Log. Methods Comput. Sci., 20(3), 2024. URL: https://doi.org/10.46298/LMCS-20(3:24)2024.
  8. 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.
  9. Pierre Clairambault. Causal Investigations in Interactive Semantics. Aix-Marseille Université, 2024. Habilitation à Diriger les Recherches. URL: https://tel.archives-ouvertes.fr/tel-04523273.
  10. Pierre Clairambault. The qualitative collapse of concurrent games. In 2025 40th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 513-526. IEEE, 2025. URL: https://doi.org/10.1109/LICS65433.2025.00045.
  11. Pierre Clairambault and Marc de Visme. Full abstraction for the quantum lambda-calculus. Proc. ACM Program. Lang., 4(POPL):63:1-63:28, 2020. URL: https://doi.org/10.1145/3371131.
  12. Pierre Clairambault and Simon Forest. The cartesian closed bicategory of thin spans of groupoids. In 38th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2023, Boston, MA, USA, June 26-29, 2023, pages 1-13. IEEE, 2023. URL: https://doi.org/10.1109/LICS56636.2023.10175754.
  13. Pierre Clairambault, Federico Olimpieri, and Hugo Paquet. From thin concurrent games to generalized species of structures. In 38th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2023, Boston, MA, USA, June 26-29, 2023, pages 1-14. IEEE, 2023. URL: https://doi.org/10.1109/LICS56636.2023.10175681.
  14. Pierre Clairambault and Hugo Paquet. The quantitative collapse of concurrent games with symmetry. CoRR, abs/2107.03155, 2021. URL: https://arxiv.org/abs/2107.03155.
  15. Daniel de Carvalho. Execution time of λ-terms via denotational semantics and intersection types. Math. Struct. Comput. Sci., 28(7):1169-1203, 2018. URL: https://doi.org/10.1017/S0960129516000396.
  16. Thomas Ehrhard. Projecting sequential algorithms on strongly stable functions. Ann. Pure Appl. Log., 77(3):201-244, 1996. URL: https://doi.org/10.1016/0168-0072(95)00026-7.
  17. Thomas Ehrhard. On köthe sequence spaces and linear logic. Math. Struct. Comput. Sci., 12(5):579-623, 2002. URL: https://doi.org/10.1017/S0960129502003729.
  18. Thomas Ehrhard. Finiteness spaces. Math. Struct. Comput. Sci., 15(4):615-646, 2005. URL: https://doi.org/10.1017/S0960129504004645.
  19. Thomas Ehrhard. The scott model of linear logic is the extensional collapse of its relational model. Theor. Comput. Sci., 424:20-45, 2012. URL: https://doi.org/10.1016/J.TCS.2011.11.027.
  20. Thomas Ehrhard, Michele Pagani, and Christine Tasson. The computational meaning of probabilistic coherence spaces. In Proceedings of the 26th Annual IEEE Symposium on Logic in Computer Science, LICS 2011, June 21-24, 2011, Toronto, Ontario, Canada, pages 87-96. IEEE Computer Society, 2011. URL: https://doi.org/10.1109/LICS.2011.29.
  21. Thomas Ehrhard and Laurent Regnier. The differential lambda-calculus. Theor. Comput. Sci., 309(1-3):1-41, 2003. URL: https://doi.org/10.1016/S0304-3975(03)00392-X.
  22. Marcelo Fiore, Nicola Gambino, Martin Hyland, and Glynn Winskel. The cartesian closed bicategory of generalised species of structures. Journal of the London Mathematical Society, 77(1):203-220, 2008. Google Scholar
  23. 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.
  24. Jean-Yves Girard. Linear logic. Theor. Comput. Sci., 50:1-102, 1987. URL: https://doi.org/10.1016/0304-3975(87)90045-4.
  25. Jean-Yves Girard. Geometry of interaction 1: Interpretation of system f. In Studies in Logic and the Foundations of Mathematics, volume 127, pages 221-260. Elsevier, 1989. Google Scholar
  26. Jean-Yves Girard. Locus solum: From the rules of logic to the logic of rules. Math. Struct. Comput. Sci., 11(3):301-506, 2001. URL: https://doi.org/10.1017/S096012950100336X.
  27. J. M. E. Hyland and C.-H. Luke Ong. On full abstraction for PCF: i, ii, and III. Inf. Comput., 163(2):285-408, 2000. URL: https://doi.org/10.1006/INCO.2000.2917.
  28. James Laird. Full abstraction for functional languages with control. In Proceedings, 12th Annual IEEE Symposium on Logic in Computer Science, Warsaw, Poland, June 29 - July 2, 1997, pages 58-67. IEEE Computer Society, 1997. URL: https://doi.org/10.1109/LICS.1997.614931.
  29. Jim Laird, Giulio Manzonetto, Guy McCusker, and Michele Pagani. Weighted relational models of typed lambda-calculi. In 28th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2013, New Orleans, LA, USA, June 25-28, 2013, pages 301-310. IEEE Computer Society, 2013. URL: https://doi.org/10.1109/LICS.2013.36.
  30. Paul-André Melliès. Asynchronous games 4: A fully complete model of propositional linear logic. In 20th IEEE Symposium on Logic in Computer Science (LICS 2005), 26-29 June 2005, Chicago, IL, USA, Proceedings, pages 386-395. IEEE Computer Society, 2005. URL: https://doi.org/10.1109/LICS.2005.6.
  31. Paul-André Melliès. Asynchronous games 2: The true concurrency of innocence. Theor. Comput. Sci., 358(2-3):200-228, 2006. URL: https://doi.org/10.1016/J.TCS.2006.01.016.
  32. Paul-André Melliès. Template games and differential linear logic. In 34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2019, Vancouver, BC, Canada, June 24-27, 2019, pages 1-13. IEEE, 2019. URL: https://doi.org/10.1109/LICS.2019.8785830.
  33. C.-H. Luke Ong. Quantitative semantics of the lambda calculus: Some generalisations of the relational model. In 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017, Reykjavik, Iceland, June 20-23, 2017, pages 1-12. IEEE Computer Society, 2017. URL: https://doi.org/10.1109/LICS.2017.8005064.
  34. Silvain Rideau and Glynn Winskel. Concurrent strategies. In Proceedings of the 26th Annual IEEE Symposium on Logic in Computer Science, LICS 2011, June 21-24, 2011, Toronto, Ontario, Canada, pages 409-418. IEEE Computer Society, 2011. URL: https://doi.org/10.1109/LICS.2011.13.
  35. Takeshi Tsukada and C.-H. Luke Ong. Plays as resource terms via non-idempotent intersection types. 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 237-246. ACM, 2016. URL: https://doi.org/10.1145/2933575.2934553.
  36. Glynn Winskel. Event structures. In Wilfried Brauer, Wolfgang Reisig, and Grzegorz Rozenberg, editors, Petri Nets: Central Models and Their Properties, Advances in Petri Nets 1986, Part II, Proceedings of an Advanced Course, Bad Honnef, Germany, 8-19 September 1986, volume 255 of Lecture Notes in Computer Science, pages 325-392. Springer, 1986. URL: https://doi.org/10.1007/3-540-17906-2_31.
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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact