Games for Logic and Programming Languages XIV

6-7 April 2019, Prague, Czech Republic.

An ETAPS 2019 workshop

GaLoP is an annual international workshop on game-semantic models for logics and programming languages and their applications. This is an informal workshop that welcomes work in progress, overviews of more extensive work, programmatic or position papers and tutorials.

Areas of interest include:

* Games and other interaction-based denotational and operational models;

* Game-based program analysis and verification;

* Logics for games and games for logics;

* Algorithmic aspects of game semantics;

* Categorical aspects of game semantics;

* Programming languages and full abstraction;

* Higher-order automata and Petri nets;

* Geometry of interaction;

* Ludics;

* Epistemic game theory;

* Logics of dependence and independence;

* Computational linguistics;

* Games and multi-valued logics.

There will be no formal proceedings but the possibility of a special issue in a journal will be considered. (The 2005, 2008, 2011 and 2014 workshops led to special issues in Annals of Pure and Applied Logic.)

Submission Instructions

Please submit an abstract (up to one page, excluding bibliography) of your proposed talk on the EasyChair submission page below. Supplementary material may be submitted, and will be considered at the discretion of the PC.

Important Dates

Submission: 8 February 2019 (extended deadline)

Notification: 22 February 2019

Workshop: 6-7 April 2019


Follow this link.

Invited Talks

Nathanaël Fijalkow (CNRS & LaBRI, Bordeaux)

Jules Hedges (University of Oxford)

Paul-André Melliès (CNRS & IRIF, Paris)


Saturday, April 6

08.45 – 09.00: Welcome

09.00 – 10.30: Session I

Jules Hedges (Invited Talk). Intertwining game theory and game semantics.

Open games are fragments of games in the sense of game theory, that can be used to build games compositionally. They can also be thought of as games in the sense of game semantics between a System and Environment, in which the moves are states and payoffs. The System is jointly controlled by n noncooperative utility-maximising players, and the goal of the System is to be in game-theoretic equilibrium. This game-semantic viewpoint is a useful way of thinking about compositional game theory, with its often-mysterious composition operators becoming quite transparent when viewed in terms of game-semantic strategies.

Paul Blain Levy, Sergey Goncharov and Lutz Schröder. Universal property of the monad for infinite trace strategies (work in progress).

10.30 – 11.00: Coffee Break

11.00 – 12.00: Session II

Pietro Galliani. Characterizing Downwards Closed Strongly First Order Dependencies.

Juha Kontinen and Fan Yang. Logics for first-order definable team properties.

12.00 – 13.00: Lunch

13.30 – 15.30: Session III

Nathanaël Fijalkow (Invited Talk). Model checking games: the recent advances on parity games.

I will talk about parity games. The first objective is to show where they appear in verification and synthesis, in particular as algorithmic back end for model checking different logical formalisms.

The second objective is to present the latest results on this model, which are neatly explained using the newly introduced notion of universal graphs.

Yu-Yang Lin and Nikos Tzevelekos. A Framework for Compositional Model Checking.

Timo Lang, Chris Fermüller, Elaine Pimentel and Carlos Olarte. Modalities as prices: a game model of intuitionistic linear logic with subexponentials.

15.30 – 16.00: Coffee Break

16.00 – 17.10: Session IV

Pierre-Louis Curien. Sequential algorithms and innocent strategies share the same execution mechanism.

Colin Riba and Pierre Pradic. A Dialectica-Like Interpretation of a Linear MSO on Infinite Words.

Sunday, April 15

09.00 – 10.30: Session V

Paul-André Melliès. 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:

Clovis Eberhart, Tom Hirschowitz and Alexis Laouar. Simple game semantics and Day convolution.

10.30 – 11.00: Coffee Break

11.00 – 12.00: Session VI

Simon Castellan, Alceste Scalas and Nobuko Yoshida. A game semantics understanding of asynchronous multiparty session types subtyping.

Simon Castellan and Hugo Paquet. Probabilistic Programming Inference via Intensional Semantics.

12.00 – 13.00: Lunch

13.30 – 15.30: Session VII

Pierre Clairambault and Marc de Visme. Full Abstraction for the Quantum Lambda-Calculus.

Lê Thành Dũng Nguyễn. Some ideas for a finite geometry of interaction model of second-order MLL.

David Baelde, Amina Doumane, Denis Kuperberg and Alexis Saurin. Bouncing Threads for Infinitary and Circular Proofs.

Abhishek De and Alexis Saurin. Towards Circular Proof Nets.

Program Committee