The Partout team welcomes Federico Olimpieri for a seminar of the proofs and algorithms pole of LIX. He will be speaking about his work on intersection type systems and (bi)categorical models of lambda-calculus, see abstract below.

Abstract: We study a family of distributors-induced bicategorical models of lambda-calculus, proving that they can be syntactically presented via intersection type systems. We first introduce a class of 2-monads whose algebras are monoidal categories modelling resource management. We lift these monads to distributors and define a parametric Kleisli bicategory, giving a sufficient condition for its cartesian closure. 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 prove that our model characterize solvability, adapting reducibility techniques to our setting. We conclude by describing two examples of our construction.

Link to the online conference

The list of next seminars can be found at: https://smimram.gitlabpages.inria.fr/proofs-algorithms/seminar/

The calendar of seminars can be found at: https://smimram.gitlabpages.inria.fr/proofs-algorithms/seminar/calendar.ics