Speaker:  Giulio Guerrieri


Quando:  19/02/2021  15:00


Dove:  Online su teams: http://bit.ly/36W271a


Abstract
Nonidempotent intersection types can be seen as a syntactic presentation of a wellknown denotational semantics for the lambdacalculus, 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 callbypushvalue. 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. 