Explicit pure type systems, subject reduction and preservation of strong normalisation
Résumé
Pure type systems are an elegant formalism allowing to specify in a very easy way a large number of type systems. The possibility of their extension to calculi with explicit substitution was the object of numerous studies, which ran into various problems. In particular, the intuitive systems obtained by the mere addition of a cut rule to type substitutions have a major flaw : they do not satisfy subject reduction. In this report, we introduce pure type systems based upon the explicit substitution calculus with names Lambda x, and we show that our systems satisfy among others subject reduction, and that they preserve the strong normalisation of their implicit counterparts.
Les systèmes de types purs sont un formalisme élégant permettant de représenter de nombreux systèmes de types. La possible extension de ces systèmes à des calculs à substitutions explicites a fait l'objet de diverses études, qui se heurtent à différents problèmes. En particulier, les systèmes intuitifs obtenus par la simple adjonction d'une règle de coupure pour typer les substitutions présentent le défaut majeur de na pas satisfaire la réduction du sujet. Dans ce rapport, nous exposons des systèmes de types purs basés sur le calcul de substitutions explicites à noms Lambda x, et nous montrons que nos systèmes satisfont entre autres propriétés la réduction du sujet, et qu'ils préservent la normalisation forte de leur équivalent implicite.
Origine : Fichiers produits par l'(les) auteur(s)