Rencontre, 24 janvier 2019
Programme
- 10:30 – 12:00
-
Paul-André Melliès (CNRS - Univ. Paris Diderot)
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!
- 14:00 – 15:00
-
Aurore Alcolei (ENS de Lyon)Invited talk: Resource-tracking concurrent games
In the study of programming languages, denotational semantics is used to abstract away from (some) intermediate steps of computation by providing invariants of reduction. Although these abstractions are very useful to help reasoning about qualitative program behaviours such as program termination, they usually do not reflect quantitative informations such as permissions or time consumption.
In this talk, I will present a framework of annotated concurrent games and strategies on event structures that generally allows for keeping track of side-information, that is, data whose value may vary with the execution flow but cannot modify it. In particular, I will use this new framework to give a sound denotational semantics to R-IPA, an affine concurrent higher-order programming language with shared state and a primitive for resource consumption, parametrized by an algebraic structure R expressing resources. Although this model is not adequate in general – its analysis being finer than that offered by the general operational semantics on resource R – I will show that adequacy holds for an operational semantics specialized to time consumption.
- 15:30 – 16:30
-
Andreas Nuyts (KU Leuven (Be))Invited talk: Degrees of Relatedness
Dependent type theory allows us to write programs and to prove properties about those programs in the same language. However, some properties do not require much proof, as they are evident from a program's implementation, e.g. if a polymorphic program is not ad hoc but relationally parametric, then we get parametricity theorems for free. If we want to safely shortcut proofs by relying on the evident good behaviour of a program, then we need a type-level guarantee that the program is indeed well-behaved. This can be achieved by annotating function types with a modality describing the behaviour of functions. We consider a dependent type system with modalities for relational parametricity, irrelevance (i.e. type-checking time erasability of an argument) and ad hoc polymorphism. The interplay of three modalities and dependent types raises a number of questions. For example: If a term depends on a variable with a given modality, then how should its type depend on it? Are all modalities always applicable, e.g. should we consider parametric functions from the booleans to the naturals? Do we need any further modalities in order to properly reason about these three?
We develop a type system, based on a denotational presheaf model, that answers these questions. The core idea is to equip every type with a number of relations --- just equality for small types, but more for larger types --- and to describe function behaviour by saying how functions act on those relations. The system has modality-aware equality judgements (ignoring irrelevant parts) and modality-aware proving operators (for proving free theorems) which are even self-applicable. It also supports sized types, some form of intersection and union types, and parametric quantification over algebraic structures. We prove soundness in a denotational presheaf model.
In this presentation I will give a relatively technical overview of how relational parametricity works in System F, Fω and dependent type theory. I will explain how and why a parametric modality is needed in dependent type theory to assert free theorems for all types. Next, I will explain how the framework in which we formulate this modality, is already powerful enough to accommodate the other modalities mentioned above. Finally, I will briefly discuss the novel structural modality which is of interest when working with algebraic structures, as well as union and intersection types and the presheaf model.
While prior knowledge about dependent type theory and relational parametricity is useful, the presentation is intended to be accessible without.
