Speaker:  Federico Olimpieri


Quando:  15/01/2021  15:00


Dove:  Videoconferenza su teams al link https://bit.ly/3bbdIMz


Abstract
Building on previous works, we present a general method to define proof relevant intersection type semantics for pure lambda calculus. We argue that the bicategory of distributors is an appropriate categorical framework for this kind of semantics. We first introduce a class of 2monads whose algebras are monoidal categories modelling resource management, following MarsdenZwardt's approach. We show how these monadic constructions determine Kleisli bicategories over the bicategory of distributors and we give a sufficient condition for cartesian closedness. We define a family of nonextensional models for pure lambda calculus. We then prove that the interpretation of lambda terms induced by these models can be concretely described via intersection type systems. The intersection constructor corresponds to the particular tensor product given by the considered free monadic construction. 