Update: Find the recording of this talk here.
This year I’m the faculty chair of the School of Computer and Cyber Sciences’ Colloquium Series. As many of you, I’ve had to transition this course online. Thus, when choosing the final speaker of the semester I did not take distance into consideration, because the requirement to physically come to Augusta University and present is no longer required. In addition, since there is no need for financial support, I’m also more free in who I ask to present.
So I am happy to announce that Paul-André Melliès will be our final presenter of the semester, but that’s not all! I have 100 seats available on my Zoom account, and only 30 of them will be needed for AU students and faculty. That leaves open 70 seats! So I am taking RSVPs from anyone who would like to attend the talk online.
The presentation information is as follows:
When: April 24th at 2pm EDT / 8pm CEST
RSVP: April 20th by email ()
Who: Paul-André Melliès (CNRS, University of Paris)
Title: “A gentle introduction to template games”
Abstract:
Game semantics is the art of interpreting formulas (or types) as games and proofs (or programs) as strategies. In order to reflect the interactive behaviour of programs, strategies are required to follow specific scheduling policies. Typically, in the case of a sequential programming language, the program (Player) and its environment (Opponent) play one after the other, in a strictly alternating way. On the other hand, in the case of a concurrent language, Player and Opponent are allowed to play several moves in a row, in a non alternating way. In the two cases, the scheduling policy is designed very carefully in order to ensure that the strategies synchronise 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 talk, I will introduce the notion of template game and exhibit a number of simple and fundamental combinatorial properties which ensure that a given scheduling policy defines (indeed) a monoidal closed bicategory of games, strategies and simulations. The notion of template game will be illustrated by constructing two game models of linear logic with different flavours (alternating and non alternating) using the same categorical combinatorics, performed in the category of small 2-categories.
The interested reader will find more material here
https://www.irif.fr/~mellies/template-games.html
https://www.youtube.com/watch?v=ZC2jtq2R3cw
and in the companion papers [1,2,3].
Bio:
Paul-André Melliès is a CNRS Researcher in France, and works in the Computer Science Department of the University of Paris. He also teaches at Ecole Normale Supérieure in Paris a graduate course on the connection between lambda-calculus, functional languages and category theory.
Paul-André Melliès has worked on a number of areas of logic, computer science and mathematics, including lambda-calculus, rewriting theory, algebraic and monadic effects in functional languages, semantics of low level languages, formal certification of machine code, game semantics, linear logic, concurrent separation logic, higher-order automata, higher categories, axiomatic homotopy theory. Behind this apparent diversity, he is looking for common unifying patterns, and for a simple description of the linguistic, geometric and interactive structures at work in logic and mathematics.
References:
[1] PAM. Categorical combinatorics of scheduling and synchronization in game semantics. Proceedings of POPL 2019.
https://www.irif.fr/~mellies/papers/Mellies19popl.pdf
https://www.irif.fr/~mellies/slides/popl-slides-january-2019.pdf
[2] PAM. Template games and differential linear logic. Proceedings of LICS 2019.
- https://www.irif.fr/~mellies/template-games/2-template-games-and-differential-linear-logic.pdf
[3] PAM. Une étude micrologique de la négation (in French)
- https://www.irif.fr/~mellies/hdr-mellies.pdf