Un type est-il composé de termes ou un terme composé de types?


Flavien Breuvart, Paris 13. 6 avril 2017 10:00 limd 2:00:00
Abstract:

S'il est commun, dans la communauté de réalisabilité, de considérer un type comme l'ensemble de ses preuves, et donc un ensemble de termes, il est aussi commun, dans la communauté des types intersections, de considérer un terme comme l'ensemble de ses comportements possibles, et donc un ensemble de types. Dans cet exposé, je présenterai en détail les types intersections, qui sont moins connus au sein du LAMA. Puis j'essaierai d'expliciter les liens avec la réalisabilité: en quoi il est intéressant de composer les deux, et si l'on peut voir les deux opérations comme duales dans un certain sens. Il ne s'agira pas (ou peu) de travaux personnels, mais d'une présentation générale et transversale du domaine.