2026-08-15T12:16:37Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:23625 2025-07-07T17:36:47Z ddc:004 open_access

Categorical Continuation Semantics for Concurrency Breuvart, Flavien Paquet, Hugo denotational semantics 2-categories concurrency continuations game semantics 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Flavien Breuvart and Hugo Paquet 2025 Is Part Of LIPIcs, Volume 337, 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSCD.2025.10 urn:nbn:de:0030-drops-236251 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2025.10 eng https://creativecommons.org/licenses/by/4.0/legalcode