Equality is typable in Semi-Full Pure Type Systems

Vincent Siles 1, 2, 3 Hugo Herbelin 1, 2
2 PI.R2 - Design, study and implementation of languages for proofs and programs
PPS - Preuves, Programmes et Systèmes, Inria Paris-Rocquencourt, UPD7 - Université Paris Diderot - Paris 7, CNRS - Centre National de la Recherche Scientifique : UMR7126
Résumé : 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.
Type de document :
Communication dans un congrès
Logic In Computer Science - LICS 2010, Jul 2010, Edinburgh, United Kingdom. 10 p., 2010
Liste complète des métadonnées

Littérature citée [15 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00496988
Contributeur : Vincent Siles <>
Soumis le : vendredi 2 juillet 2010 - 10:36:24
Dernière modification le : vendredi 25 mai 2018 - 12:02:06
Document(s) archivé(s) le : mardi 23 octobre 2012 - 09:36:18

Fichier

herbelin.siles.LICS2010.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00496988, version 1

Collections

Citation

Vincent Siles, Hugo Herbelin. Equality is typable in Semi-Full Pure Type Systems. Logic In Computer Science - LICS 2010, Jul 2010, Edinburgh, United Kingdom. 10 p., 2010. 〈inria-00496988〉

Partager

Métriques

Consultations de la notice

220

Téléchargements de fichiers

110