Abstract References

Towards A Rosetta Stone of Interactive and Quantitative Semantics

Pierre Clairambault ORCID CNRS, Aix Marseille Univ, LIS, France
Abstract

Quantitative semantics are those denotational semantics that inherit from linear logic [24] a sensitivity to the multiplicity of resources involved in computation. Those include the relational model [24] and its numerous variations (such as finiteness spaces [18], weighted relational models [29] and their extensions [20, 17], generalized species of structure [22], span models [32, 12], etc), as well as related syntactic methods such as non-idempotent intersection types [15] and Taylor expansion of lambda-terms [21]. 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 [27, 2]), and other frameworks such as Geometry of Interaction [25] or ludics [26]. 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 [1]. 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 [3], control operators [28], and concurrent primitives [23]. Early on, researchers have explored the relationship between the two [16, 4], and investigations on this question have spanned decades [5, 6, 35, 33]. In particular, Melliès’ work on asynchronous games [31, 30] 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” [8, 9], an extension with symmetry of Rideau and Winskel’s concurrent games on event structures [34]. Event structures being one of the main “truly concurrent” models of concurrency [36], 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 [7, 9]. 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 [7, 9], the weighted relational model [14], the quantum relational model [11], generalized species of structure [13], and – going beyond quantitative semantics – the linear Scott model [10], a linear decomposition of standard Scott domain semantics [19]. 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.

Keywords and phrases:
Denotational semantics, Game semantics
Category:
Invited Talk
Copyright and License:
[Uncaptioned image] © Pierre Clairambault; licensed under Creative Commons License CC-BY 4.0
2012 ACM Subject Classification:
Theory of computation → Denotational semantics
DOI:
10.4230/LIPIcs.CSL.2026.4
Event:
34th EACSL Annual Conference on Computer Science Logic (CSL 2026)
Editors:
Stefano Guerrini and Barbara König
Series and Publisher:
LIPIcs Logo Leibniz International Proceedings in Informatics, Schloss Dagstuhl – Leibniz-Zentrum für Informatik

References

  • [1] Samson Abramsky. Semantics of interaction: an introduction to game semantics. In Semantics and Logics of Computation. Cambridge University Press, 1997.
  • [2] Samson Abramsky, Radha Jagadeesan, and Pasquale Malacaria. Full abstraction for PCF. Inf. Comput., 163(2):409–470, 2000. doi: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. doi: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. doi: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. doi: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. doi: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. doi: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. doi: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. doi: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. doi: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. doi: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. doi:10.1109/LICS56636.2023.10175681.
  • [14] Pierre Clairambault and Hugo Paquet. The quantitative collapse of concurrent games with symmetry. CoRR, abs/2107.03155, 2021. arXiv: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. doi:10.1017/S0960129516000396.
  • [16] Thomas Ehrhard. Projecting sequential algorithms on strongly stable functions. Ann. Pure Appl. Log., 77(3):201–244, 1996. doi: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. doi:10.1017/S0960129502003729.
  • [18] Thomas Ehrhard. Finiteness spaces. Math. Struct. Comput. Sci., 15(4):615–646, 2005. doi: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. doi: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. doi:10.1109/LICS.2011.29.
  • [21] Thomas Ehrhard and Laurent Regnier. The differential lambda-calculus. Theor. Comput. Sci., 309(1-3):1–41, 2003. doi: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.
  • [23] Dan R. Ghica and Andrzej S. Murawski. Angelic semantics of fine-grained concurrency. Ann. Pure Appl. Log., 151(2-3):89–114, 2008. doi:10.1016/J.APAL.2007.10.005.
  • [24] Jean-Yves Girard. Linear logic. Theor. Comput. Sci., 50:1–102, 1987. doi: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.
  • [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. doi: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. doi: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. doi: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. doi: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. doi: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. doi: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. doi: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. doi: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. doi: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. doi: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. doi:10.1007/3-540-17906-2_31.