Causal Investigations in Interactive Semantics
Pierre Clairambault · HAL (Le Centre pour la Communication Scientifique Directe) · 2024
Game Semantics is a powerful mathematical framework to reason compositionally on programs. In contrast to other more classical methods in denotational semantics, game semantics sees programs not merely as mathematical functions taking inputs (which may be functions themselves) and producing outputs, but rather, sees them as dynamic and interactive processes. It captures compositionally the control flow even for programs with complex computational primitives such as higher-order, mutable state, control operators, etc. However, gamesemanticsisnotamathematicaltheory: rather, it is a loose collection of separated technical settings, sometimes only loosely connected by the folklore of a handful of experts. One of those technical setting is concurrent games, inheriting from the concurrent games of Abramsky and Melliès and from Melliès’ asynchronous games. In its recent technical set-up proposed by Rideau and Winskel, this model is based on event structures, a true concurrency model that avoids assuming the existence of a global clock, representing instead programs via their causal structure. Of course, concurrent games can handle the semantics of concurrent programs. But in this monograph, I show that more than yet another new model, their expressivity reveals structures implicitly present in several other models from the literature, for concurrent languages, or not. In doing so, walking in the footsteps of Abramsky and Melliès’ vision, they give us the means for a synthesis between various games or other denotational models, bringing game semantics one step closer to a mathematical theory. Concretely, this monograph starts in Part I with a detailed introduction to several traditional pointer game semantics: first for the paradigmatic purely functional language , its extension with mutable state, and the non-alternating variant for its concurrent extension . In Part II, I give a complete presentation of concurrent games and their extension with symmetry. In Part III, I link concurrent games to the different gamesmodelsintroducedinPartI–butalsoothermodels, suchastherelationalmodelvia interpretation-preserving functors. Finally, in Part IV, I survey other developments in concurrent games, and I conclude with some open problems and perspectives.