Document Open Access Logo

Categorical Continuation Semantics for Concurrency

Authors Flavien Breuvart , Hugo Paquet

PDF

File

Thumbnail PDF
PDF
LIPIcs.FSCD.2025.10.pdf
  • Filesize: 1.42 MB
  • 21 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Categorical semantics
  • Theory of computation → Denotational semantics
  • Theory of computation → Concurrency
  • Theory of computation → Linear logic
Keywords
  • denotational semantics
  • 2-categories
  • concurrency
  • continuations
  • game semantics

Metrics

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

Abstract

Continuation semantics for simple programming languages can be axiomatized as a dialogue category: a symmetric monoidal category equipped with a negation operation. This axiomatization makes clear the relationship between game semantics, CPS transformations, and continuation monads. 

In this paper we extend dialogue categories with 2-categorical structure and concurrent primitives. This is inspired by a recent analysis of concurrency based on 2-categorical monads. We show that the fine-grained structure of dialogue categories, not generally available in other semantic models, can be exploited to give a type to concurrent primitives join and fork. Our main theorem is that this simple axiomatization induces a concurrent continuation 2-monad. We also show that this framework is expressive beyond call-by-value monadic programming.

The definitions in this paper are illustrated by concrete constructions in concurrent game semantics, and our results give a formal categorical basis for concurrent strategies. From a more practical perspective, our approach suggests a candidate target language for linear CPS transformations of concurrent programming languages.

Cite As Get BibTex

Flavien Breuvart and Hugo Paquet. Categorical Continuation Semantics for Concurrency. In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 10:1-10:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.FSCD.2025.10

Author Details

Flavien Breuvart
  • Université Sorbonne Paris Nord, CNRS, Laboratoire d'Informatique de Paris Nord, LIPN, F-93430 Villetaneuse, France
Hugo Paquet
  • Inria, École Normale Supérieure - PSL, CNRS, Paris, France

Acknowledgements

We have benefited from discussing this work with many people including Morgan Rogers, Philip Saville, Tarmo Uustalu and Guannan Wei. Thanks to two anonymous referees for helpful feedback.

References

  1. John C Baez and Kenny Courser. Structured cospans. Theory & Applications of Categories, 35, 2020. Google Scholar
  2. H P Barendregt. The lambda calculus, its syntax and semantics. Studies in Logic and the Foundations of Mathematics, 103, 1984. Google Scholar
  3. Josh Berdine, Peter W. O'Hearn, Uday S. Reddy, and Hayo Thielecke. Linear continuation-passing. High. Order Symb. Comput., 15(2-3):181-208, 2002. URL: https://doi.org/10.1023/A:1020891112409.
  4. Simon Castellan, Pierre Clairambault, Silvain Rideau, and Glynn Winskel. Games and strategies as event structures. Logical Methods in Computer Science, 13, 2017. URL: https://doi.org/10.23638/LMCS-13(3:35)2017.
  5. Simon Castellan, Pierre Clairambault, and Glynn Winskel. The parallel intensionally fully abstract games model of PCF. In 30th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2015, Kyoto, Japan, July 6-10, 2015, pages 232-243. IEEE Computer Society, 2015. URL: https://doi.org/10.1109/LICS.2015.31.
  6. Simon Castellan, Pierre Clairambault, and Glynn Winskel. Observably deterministic concurrent strategies and intensional full abstraction for parallel-or. In Dale Miller, editor, 2nd International Conference on Formal Structures for Computation and Deduction, FSCD 2017, September 3-9, 2017, Oxford, UK, volume 84 of LIPIcs, pages 12:1-12:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. URL: https://doi.org/10.4230/LIPIcs.FSCD.2017.12.
  7. 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.
  8. Pierre-Louis Curien, Marcelo P. Fiore, and Guillaume Munch-Maccagnoni. A theory of effects and resources: adjunction models and polarised calculi. In Rastislav Bodík and Rupak Majumdar, editors, Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20 - 22, 2016, pages 44-56. ACM, 2016. URL: https://doi.org/10.1145/2837614.2837652.
  9. Claudia Faggian and Mauro Piccolo. Partial orders, event structures and linear strategies. In International Conference on Typed Lambda Calculi and Applications, pages 95-111. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-02273-9_9.
  10. 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
  11. Marcelo Fiore and Philip Saville. A type theory for cartesian closed bicategories. In 2019 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 1-13. IEEE, 2019. URL: https://doi.org/10.1109/LICS.2019.8785708.
  12. Dan R Ghica and Andrzej S Murawski. Angelic semantics of fine-grained concurrency. Annals of Pure and Applied Logic, 151(2-3):89-114, 2008. URL: https://doi.org/10.1016/j.apal.2007.10.005.
  13. Timothy G Griffin. A formulae-as-type notion of control. In Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 47-58, 1989. URL: https://doi.org/10.1145/96709.96714.
  14. Masahito Hasegawa. Semantics of linear continuation-passing in call-by-name. In Yukiyoshi Kameyama and Peter J. Stuckey, editors, Functional and Logic Programming, 7th International Symposium, FLOPS 2004, Nara, Japan, April 7-9, 2004, Proceedings, volume 2998 of Lecture Notes in Computer Science, pages 229-243. Springer, 2004. URL: https://doi.org/10.1007/978-3-540-24754-8_17.
  15. Tony Hoare. Unifying semantics for concurrent programming. In Bob Coecke, Luke Ong, and Prakash Panangaden, editors, Computation, Logic, Games, and Quantum Foundations. The Many Facets of Samson Abramsky - Essays Dedicated to Samson Abramsky on the Occasion of His 60th Birthday, volume 7860 of Lecture Notes in Computer Science, pages 139-149. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-38164-5_10.
  16. Tony Hoare, Bernhard Möller, Georg Struth, and Ian Wehrman. Concurrent kleene algebra and its foundations. J. Log. Algebraic Methods Program., 80(6):266-296, 2011. URL: https://doi.org/10.1016/j.jlap.2011.04.005.
  17. Martin Hofmann and Thomas Streicher. Completeness of continuation models for lambda-mu-calculus. Inf. Comput., 179(2):332-355, 2002. URL: https://doi.org/10.1006/inco.2001.2947.
  18. Niles Johnson and Donald Ying Yau. 2-Dimensional Categories. Oxford university press, Oxford, 2021. Google Scholar
  19. Axel Kerinec, Giulio Manzonetto, and Federico Olimpieri. Why are proofs relevant in proof-relevant models? Proc. ACM Program. Lang., 7(POPL):218-248, 2023. URL: https://doi.org/10.1145/3571201.
  20. Anders Kock. Strong functors and monoidal monads. Archiv der Mathematik, 23:113-120, 1972. Google Scholar
  21. Stephen Lack. A 2-categories companion. In Towards higher categories, pages 105-191. Springer, 2009. Google Scholar
  22. Paul Blain Levy. Adjunction models for call-by-push-value with stacks. In Richard Blute and Peter Selinger, editors, Category Theory and Computer Science, CTCS 2002, Ottawa, Canada, August 15-17, 2002, volume 69 of Electronic Notes in Theoretical Computer Science, pages 248-271. Elsevier, 2002. URL: https://doi.org/10.1016/S1571-0661(04)80568-1.
  23. Paul Blain Levy. Pointer games. Call-By-Push-Value: A Functional/Imperative Synthesis, pages 169-203, 2003. Google Scholar
  24. Paul-André Melliès. Asynchronous games 3 an innocent model of linear logic. In Lars Birkedal, editor, Proceedings of the 10th Conference on Category Theory in Computer Science, CTCS 2004, Copenhagen, Denmark, August 12-14, 2004, volume 122 of Electronic Notes in Theoretical Computer Science, pages 171-192. Elsevier, 2004. URL: https://doi.org/10.1016/j.entcs.2004.06.057.
  25. Paul-André Mellies. Categorical semantics of linear logic. Panoramas et syntheses, 27:15-215, 2009. Google Scholar
  26. Paul-André Melliès. Game semantics in string diagrams. In Proceedings of the 27th Annual IEEE Symposium on Logic in Computer Science, LICS 2012, Dubrovnik, Croatia, June 25-28, 2012, pages 481-490. IEEE Computer Society, 2012. URL: https://doi.org/10.1109/LICS.2012.58.
  27. Paul-André Melliès. Une étude micrologique de la négation. Habilitation à diriger des recherches. Université Paris VII, page 19, 2017. Google Scholar
  28. Paul-André Melliès. Categorical combinatorics of scheduling and synchronization in game semantics. Proceedings of the ACM on Programming Languages, 3(POPL):1-30, 2019. URL: https://doi.org/10.1145/3290336.
  29. Paul-André Melliès and Léo Stefanesco. Concurrent separation logic meets template games. CoRR, abs/2005.04453, 2020. URL: https://doi.org/10.48550/arXiv.2005.04453.
  30. Paul-André Melliès and Nicolas Tabareau. Resource modalities in tensor logic. Ann. Pure Appl. Log., 161(5):632-653, 2010. URL: https://doi.org/10.1016/j.apal.2009.07.018.
  31. Eugenio Moggi. Notions of computation and monads. Information and computation, 93(1):55-92, 1991. URL: https://doi.org/10.1016/0890-5401(91)90052-4.
  32. Hugo Paquet. Probabilistic concurrent game semantics. PhD thesis, University of Cambridge, Computer Laboratory, 2020. URL: https://doi.org/10.17863/CAM.61919.
  33. Hugo Paquet and Philip Saville. Effectful semantics in bicategories: strong, commutative, and concurrent pseudomonads. In Pawel Sobocinski, Ugo Dal Lago, and Javier Esparza, editors, Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2024, Tallinn, Estonia, July 8-11, 2024, pages 61:1-61:15. ACM, 2024. URL: https://doi.org/10.1145/3661814.3662130.
  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. Exequiel Rivas and Mauro Jaskelioff. Monads with merging, 2019. URL: https://inria.hal.science/hal-02150199/document.
  36. Peter Selinger. Control categories and duality: on the categorical semantics of the lambda-mu calculus. Mathematical structures in computer science, 11(2):207-260, 2001. URL: http://journals.cambridge.org/action/displayAbstract?aid=68983.
  37. Hayo Thielecke. Categorical structure of continuation passing style. PhD thesis, University of Edinburgh. College of Science and Engineering, 1997. Google Scholar
  38. Philip Wadler. Call-by-value is dual to call-by-name. In Colin Runciman and Olin Shivers, editors, Proceedings of the Eighth ACM SIGPLAN International Conference on Functional Programming, ICFP 2003, Uppsala, Sweden, August 25-29, 2003, pages 189-201. ACM, 2003. URL: https://doi.org/10.1145/944705.944723.
  39. Glynn Winskel and Mogens Nielsen. Models for concurrency. In Handbook of logic in computer science (vol. 4) semantic modelling, pages 1-148. 1995. Google Scholar
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