Pierre Clairambault (Cambridge, UK)

Concurrent games with symmetry

Abstract: Recently, Rideau and Winskel introduced a new framework of concurrent games, to serve as a new foundation for games semantics. It is based on "true concurrency" ideas, and extends the concurrent games of Abramsky and Melliès and the asynchronous games of Melliès and Mimram, allowing nondeterminism. In this new framework, we introduce a behavioural symmetry, expressing when plays are essentially the same. The addition of symmetry has profound effects on the mathematical structure of games and strategies: strategies have to respect symmetry, and this affects the definition of copycat and composition. We characterize the strategies for which copycat acts like an identity, building a -bicategory of games with symmetry and concurrent strategies. Thanks to the addition of symmetry, we can use concurrent games to model languages that are not resource-sensitive. We give two applications: firstly, a concurrent generalization of a variant of AJM games used by Baillot, Danos, Ehrhard and Regnier to model Classical Linear Logic. Secondly, a notion of "concurrent games with pointers", leading to a concurrent and nondeterministic generalization of the HO framework of arenas and innocent strategies. This is joint work with Simon Castellan and Glynn Winskel.