Categorifying Non-Idempotent Intersection Types

Venerdì 19 febbraio 2021, ore 15:00 si terrà il seminario del dr. Giulio Guerrieri (Università di Bath) di Logica e Informatica Teorica dal titolo: "Categorifying Non-Idempotent Intersection Types".

Abstract

Non-idempotent intersection types can be seen as a syntactic presentation of a well-known denotational semantics for the lambda-calculus, the category of sets and relations. Building on previous work, we present a categorification of this line of thought in the framework of the bang calculus, an untyped version of Levy’s call-by-push-value. We define a bicategorical model for the bang calculus, whose syntactic counterpart is a suitable category of types. In the framework of distributors, we introduce intersection type distributors, a bicategorical proof relevant refinement of relational semantics. Finally, we prove that intersection type distributors characterize normalization at depth 0.

This is joint work with Federico Olimpieri, accepted at CSL 2021.

Per partecipare al Seminario cliccare sul seguente Link