Vendredi 13 Mars

Retour à la vue des calendrier
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
well-typed terms. In this joint work with Paul-André 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.