Pure Type System conversion is always typable - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Article Dans Une Revue Journal of Functional Programming Année : 2012

Pure Type System conversion is always typable

Résumé

Pure Type Systems are usually described in two different ways, one that uses an external notion of computation like beta-reduction, and one that relies on a typed judgment of equality, directly in the typing system. For a long time, the question was open to know whether both presentations described the same theory. A first step toward this equivalence has been made by Adams for a particular class of \emph{Pure Type Systems} (PTS) called functional. Then, his result has been relaxed to all semi-full PTS in previous work. In this paper, we finally give a positive answer to the general issue, and prove that equivalence holds for any Pure Type System.
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.
Fichier principal
Vignette du fichier
PTSATR.pdf (208.37 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

inria-00497177 , version 1 (02-07-2010)
inria-00497177 , version 2 (18-12-2011)

Identifiants

Citer

Vincent Siles, Hugo Herbelin. Pure Type System conversion is always typable. Journal of Functional Programming, 2012, 22 (2), pp.153 - 180. ⟨10.1017/S0956796812000044⟩. ⟨inria-00497177v2⟩
197 Consultations
363 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More