Paul-André Melliès (CNRS - Univ. Paris Diderot), Template games: a homotopy model of differential linear logic

Programme

Résumé

In this introductory tutorial talk, I will explain how the notion of template game slowly emerged from the desire to develop a simple and purely combinatorial description of game semantics, living in harmony with the relational semantics of linear logic. My talk will be in three parts. First, I will recall the traditional game semantics of intuitionistic linear logic (ILL) based on sequential alternating games and strategies. Then, I will explain how to reformulate that model (or a slight variant of it) in the functorial language of template games. Finally, I will show that template games provide the first game semantics of differential linear logic (DiLL). The construction of the model will be driven by a healthy comparison with the model of generalised species formulated ten years ago by Marcelo Fiore, Nicola Gambino, Martin Hyland and Glynn Winskel. I will in particular indicate why homotopy theory plays a fundamental role in the construction of the template game model, while it remains hidden in the model based on generalised species. In that way, besides the resolution of an old open problem of game semantics, the template game model reveals an unexpected and promising convergence between linear logic and homotopy theory. If time permits, I will also describe the concurrent template game model of differential linear logic, and its connection to the semantics of the pi-calculus through the translation by Thomas Ehrhard and Olivier Laurent.

See also this page about template games!