Equality is typable in Semi-Full Pure Type Systems

International audienceThere are two usual ways to describe equality in a dependent typing system, one that uses an external notion of computation like beta-reduction, and one that introduces a typed judgement of beta-equality directly in the typing system. After being an open problem for some time, the general equivalence between both approaches has been solved by Adams for a class of pure type systems (PTSs) called functional. In this paper, we relax the functionality constraint and prove the equivalence for all semi-full PTSs by combining the ideas of Adams with a study of the general shape of types in PTSs. As one application, an extension of this result to systems with sub-typing would be a first step toward bringing closer the theory behind a proof assistant such as Coq to its implementation.Il existe deux manières habituelles de présenter un système de types dépendants, une qui utilise une notion de calcul indépendante du typage, tel que la beta-reduction, et une autre qui introduit une notion de jugements d'égalité typée directement dans les règles de typage du système. La question de savoir si ces deux présentations décrivaient la même théorie est restée un problème pendant plusieurs années. Adams a fait un premier vers une réponse à cette question en la prouvant correcte pour une classe de Systèmes de Types Pures (PTS) dit "fonctionnels". Dans ce papier, nous étendons encore un peu plus la preuve d'Adams en prouvant que cette équivalence est vraie pour tout les Systèmes de Types Pures "semi-complet", en combinant les idées présentées par Adams avec une étude de la forme générale des types dans les PTS. Ce résultat est un premier pas vers une extension à des systèmes de types contenant du sous-typage, ce qui permettrait de rapprocher encore plus la méta-théorie de certains assistants à la preuve , tel que Coq, de leur implémentation