Rencontre, March 31, 2022

La rencontre se tiendra à l'ENS de Lyon, sur le site Monod.

Le déjeûner est fourni, à partir du moment où vous êtes inscrit(e).

Nous serons le matin en salle 435 (4ème étage), l'après-midi dans en amphi B (3ème et 4ème étages).

Pour suivre la journée à distance, choisissez "chocola" dans le menu déroulant que vous trouverez ici : Le mot de passe est en minuscules, c'est la capitale de la Belgique, le titre d'une chanson de Jacques Brel, et une race de chou.

Pensez à autoriser les pop-ups pour pouvoir vous connecter.


10:30 – 12:00
Cristina Matache (Oxford University, UK)

In this talk I will discuss how to build models of programming languages using monads on categories of sheaves. The goal of the talk is to explain how several well-known models from different application domains, such as probability, differentiability and full abstraction, are instances of the same general framework.

I will explain what sheaves are and how in all these models partiality and recursion are treated uniformly using ideas from synthetic domain theory.

The talk is based on joint work with Sean Moss and Sam Staton.

14:00 – 15:00
Abhishek De (IRIF)

Fixed point logics are logics enriched with one or more fixed point operators. There are several motivations for investigating fixed point logics from the study of algebraic structures (like Kleene lattices) to the study of (co)inductive type systems. In this talk, I will give a brief overview of fixed point logics and concentrate specifically on linear logic with fixed points discussing various proof systems, their expressivity, and truth semantics.

15:30 – 16:30
Federico Olimpieri (University of Leeds, UK)

We study a family of distributor-induced bicategorical models of lambda-calculus, proving that they can be syntactically presented via intersection type systems. In this framework we define a proof-relevant semantics: the interpretation of a term associates to it the set of its typing derivations in appropriate systems. We then restrict to a particular case of our construction and show that the interpretation of a program corresponds to the interpretation of its Böhm tree. We prove this result exploiting the proof-relevance of our model, which allows a fine-grained analysis of programs evaluation. We then obtain the characterization of the theory induced by the bicategorical model: two lambda-terms share the same interpretation exactly when their Bohm trees coincide.