Pure Type System conversion is always typable

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é : Les Systèmes de Types Purs (PTS) sont habituellement présentés de deux manières différentes, une qui utilise une notion de calcul indépendante du typage, comme la béta-reduction, et une qui défini un jugement d'égalité typée au sein du système de types. La question de savoir si ces deux présentations représentaient la même théorie est restée ouverte pendant de nombreuses années. Une première réponse partielle à cette question a été apportée par Adams pour une classe particulière de PTS dit "fonctionnels". Nous avons récement étendu ce résultat à tous les PTS "semi-complets" . Dans cet article, nous pouvons finalement donner une réponse positive à la question dans toute sa généralité: l'équivalence entre les deux présentations est prouvée correcte pour n'importe quel Système de Types Purs.
Type de document :
Article dans une revue
Journal of Functional Programming, Cambridge University Press (CUP), 2012, 22 (2), pp.153 - 180. 〈10.1017/S0956796812000044〉
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00497177
Contributeur : Vincent Siles <>
Soumis le : dimanche 18 décembre 2011 - 10:10:40
Dernière modification le : mercredi 25 avril 2018 - 10:45:20
Document(s) archivé(s) le : lundi 5 décembre 2016 - 08:42:47

Fichier

PTSATR.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

INRIA | LIX | X | PARISTECH | X-LIX | PPS | USPC

Citation

Vincent Siles, Hugo Herbelin. Pure Type System conversion is always typable. Journal of Functional Programming, Cambridge University Press (CUP), 2012, 22 (2), pp.153 - 180. 〈10.1017/S0956796812000044〉. 〈inria-00497177v2〉

Partager

Métriques

Consultations de la notice

269

Téléchargements de fichiers

203