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èsmidi 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 : https://entservices.enslyon.fr/entVisio/ 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 popups pour pouvoir vous connecter.
Programme
 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 wellknown 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)Invited talk: Provability of linear logic with fixed points
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)Invited talk: Categorifying graph models of lambda calculus
We study a family of distributorinduced bicategorical models of lambdacalculus, proving that they can be syntactically presented via intersection type systems. In this framework we define a proofrelevant 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 proofrelevance of our model, which allows a finegrained analysis of programs evaluation. We then obtain the characterization of the theory induced by the bicategorical model: two lambdaterms share the same interpretation exactly when their Bohm trees coincide.