Vendredi 13 Mars
Heure: 
11:00  12:30 
Lieu: 
Salle B107, bâtiment B, Université de Villetaneuse 
Résumé: 
Functors are Type Refinement Systems 
Description: 
Noam Zeilberger The standard reading of type theory through the lens of category theory is based on the idea of viewing a type system as a category of welltyped terms. In this joint work with PaulAndré Melliès we propose a basic revision of this reading: rather than interpreting type systems as categories, we describe them as functors from a category of typing derivations to a category of underlying terms. Then, turning this around, we explain how in fact *any* functor gives rise to a generalized type system, with an abstract notion of typing judgment, typing derivations and typing rules. This leads to a purely categorical reformulation of various natural classes of type systems as natural classes of functors.
In the talk I want to motivate and introduce this general framework (which can also be seen as providing a categorical analysis of _refinement types_), and as a larger example give a sketch of how the framework can be used to formalize an elegant proof of a coherence theorem by John Reynolds. If time permits, I will also describe some of the natural questions raised by this perspective that are the subject of ongoing research. 

