Luc Pellissier
LIPN, Université Paris 13
https://lacl.fr/~lpellissier/
Date(s) : 15/06/2017 iCal
11 h 00 min - 12 h 00 min
We investigate intersection types from the “type systems as functors” viewpoint, as recently given by Melliès and Zeilberger. After recasting type-theoretic notions such as subject reduction and subject expansion in functorial terms, we will give an intersection type system for linear logic (deriving from the fact that propositional linear logic is aproximated by its multiplicative fragment). Pulling back this intersection type system along translations of embeddings of a term language into linear logic gives a corresponding intersection type system. We discuss several instances of this general construction, recovering known systems and their usual properties.
Joint work with Damiano Mazza and Pierre Vial.
https://lipn.univ-paris13.fr/~pellissier/
Catégories