Categorifying Intersection Types

Federico Olimpieri (University of Leeds)

18-Nov-2021, 14:30-15:30 (2 years ago)

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 wo examples of our construction.

category theory

Audience: researchers in the topic


ItaCa Fest 2021

Series comments: ItaCa Fest is an online webinar aimed to gather the community of ItaCa.

Organizer: Progetto ItaCa*
*contact for this listing

Export talk to