Blogs (1) >>
POPL 2019
Sun 13 - Sat 19 January 2019 Cascais, Portugal
Wed 16 Jan 2019 14:29 - 14:51 at Sala II - Categories Chair(s): Nicolas Tabareau

Game semantics is the art of interpreting types as \emph{games} and programs as strategies interacting in space and time with their environment. In order to reflect the interactive behavior of programs, strategies are required to follow specific scheduling policies. Typically, in the case of a purely sequential programming language, the program (Player) and its environment (Opponent) will play one after the other, in a strictly alternating way. On the other hand, in the case of a concurrent language, Player and Opponent will be allowed to play several moves in a row, in a non-alternating way. In both cases, the scheduling policy is designed very carefully in order to ensure that the strategies synchronize properly and compose well when plugged together. A longstanding conceptual problem has been to understand when and why a given scheduling policy works and is compositional in that sense. In this paper, we exhibit a number of simple and fundamental combinatorial structures which ensure that a given scheduling policy encoded as \emph{synchronization template} defines a symmetric monoidal closed (and in fact $\ast$-autonomous) bicategory of games, strategies and simulations. To that purpose, we choose to work at a very general level, and illustrate our method by constructing two template game models of linear logic with different flavors (alternating and non-alternating) using the same categorical combinatorics, performed in the category of small categories. As a whole, the paper may be seen as a hymn in praise of synchronization, building on the notion of synchronization algebra in process calculi and adapting it smoothly to programming language semantics, using a combination of ideas at the converging point of game semantics and categorical algebra.

Categorical Combinatorics of Scheduling and Synchronization in Game Semantics (popl-january-2019.pdf)1.88MiB

Wed 16 Jan

Displayed time zone: Belfast change

13:45 - 14:51
CategoriesResearch Papers at Sala II
Chair(s): Nicolas Tabareau Inria
13:45
22m
Talk
Familial Monads and Structural Operational Semantics
Research Papers
Tom Hirschowitz Univ. Grenoble Alpes, Univ. Savoie Mont Blanc, CNRS, LAMA, 73000 Chambéry
Link to publication DOI Media Attached File Attached
14:07
22m
Talk
Bindings as Bounded Natural Functors
Research Papers
Jasmin Blanchette Vrije Universiteit Amsterdam, Lorenzo Gheri Middlesex University London, Andrei Popescu Middlesex University, London, Dmitriy Traytel ETH Zurich
Link to publication DOI Media Attached File Attached
14:29
22m
Talk
Categorical Combinatorics of Scheduling and Synchronization in Game Semantics
Research Papers
Paul-André Melliès CNRS and University Paris Diderot
Link to publication DOI Media Attached File Attached