Template games: a homotopy model of differential linear logic
In this introductory talk, I will describe the basic building blocks leading to the recent construction of a template game model of differential linear logic. The construction relies on the observation that the scheduling mechanisms of game semantics are regulated by a simple and independent combinatorial structure, called synchronisation template. One benefit of the approach is that template games come in different flavours (sequential, concurrent, relational) depending on the chosen synchronisation template. After illustrating in all flavours how the template game model works for multiplicative additive linear logic (MALL), I will explain how to extend it with an exponential modality, in order to obtain a model of differential linear logic (DiLL). The construction is guided by the model of generalised species designed ten years ago by Fiore, Gambino, Hyland and Winskel. One significant novelty of the model is the emergence of an unexpected homotopy structure on games and strategies, whose purpose (as we will see) is to accommodate and adjust the action of the various symmetric groups on the address space of the formula. More on template games will be found on this web page: https://www.irif.fr/~mellies/template-games.html
Sun 7 AprDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
09:00 - 10:30 | |||
09:00 60mTalk | Template games: a homotopy model of differential linear logic GaLoP | ||
10:00 30mTalk | Simple game semantics and Day convolution GaLoP Clovis Eberhart National Institute of Informatics, Japan, Tom Hirschowitz Univ. Grenoble Alpes, Univ. Savoie Mont Blanc, CNRS, LAMA, 73000 Chambéry, Alexis Laouar Univ. Grenoble Alpes, Univ. Savoie Mont Blanc, CNRS |