Explicit Pure Type Systems for the Lambda-Cube
Résumé
Pure type systems are a general formalism allowing to represent many type systems -- in particular, Barendregt's lambda-cube, including Girard's system F, dependent types, and the calculus of constructions. We built a variant of pure type systems by adding a cut rule associated to an explicit substitution in the syntax, according to the Curry-Howard-de Bruijn correspondence. The addition of the cut requires the addition of a new rule for substitutions, with which we are able to show type correctness and subject reduction for all explicit systems. Moreover, we proved that the explicit lambda-cube obtained this way is strongly normalizing.
Les systèmes de types purs sont un formalisme général permettant de représenter de nombreux systèmes – en particulier, le λ-cube de Barendregt, incluant le système F de Girard, les types dépendants et le calcul es constructions. Nous avons construit une variante des systèmes de types purs en ajoutant une règle de coupure associée à une substitution explicite dans la syntaxe, selon la correspondance de Curry-Howard-de Bruijn. L’adjonction de la règle de coupure impose d’ajouter une nouvelle règle pour les substitutions, avec laquelle nous pouvons montrer la correction des types et la réduction du sujet pour tous les systèmes explicites. En outre, nous avons montré que le λ-cube explicite obtenu de cette manière est fortement normalisant
Origine : Fichiers produits par l'(les) auteur(s)
Loading...