|
|
 |
|
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. |
|
|
