Il a été montré par Adams [1], avec généralisation par Siles et Herbelin [2,3], qu’il était équivalent de définir les Systèmes de Types Purs (PTS) avec une conversion non typée (ce qui fournit une définition des PTS facile à implémenter) ou avec une conversion typée (« à la Martin-Löf », ce qui facile la construction de modèles). L’extension du résultat à des PTS avec sous-typage de sorte continue cependant de poser problème, et pourtant, une telle extension permettrait de connecter Coq, dont le cœur est le Calcul des Constructions avec univers cumulatifs, à son modèle ensembliste.

L’objectif du stage est ainsi d’établir si oui ou non le Calcul des Constructions avec univers cumulatifs (c’est-à-dire avec la règle Prop ⊂ Type(i) ⊂ Type(i+1)) est équivalent à sa version avec conversion typée.

On pourra se baser pour démarrer sur des idées récentes développées par Siles et Herbelin.

Références

[1] Adams, Pure Type Systems with judgemental equality. Journal of Functional Programming 16(2), 2006.

[2] Siles et Herbelin, Equality Is Typable in Semi-full Pure Type Systems. LICS 2010.

[3] Siles et Herbelin, Pure Type System conversion is always typable, manuscrit, 2010.

Ce document a été traduit de L^AT_EX par H^EV^EA