Linear approximations, fibrations, intersection types

Carte non disponible

Date(s) - 15/06/2017
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.

Posts created 14

Articles similaires

Commencez à saisir votre recherche ci-dessus et pressez Entrée pour rechercher. ESC pour annuler.

Retour en haut
Secured By miniOrange