Rencontre, 31 mars 2022

Programme

10:30 – 12:00
Cristina Matache (Oxford University, UK)
Invited talk: A unified treatment of concrete sheaf models for higher-order recursion

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)
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 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.