Explicit Pure Type Systems for the Lambda-Cube - Archive ouverte HAL Accéder directement au contenu
Rapport (Rapport De Recherche) Année : 2004

Explicit Pure Type Systems for the Lambda-Cube

(1) , (1)
1

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
Fichier principal
Vignette du fichier
RR2004-08.pdf (282.23 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-02101921 , version 1 (17-04-2019)

Identifiants

  • HAL Id : hal-02101921 , version 1

Citer

Romain Kervarc, Pierre Lescanne. Explicit Pure Type Systems for the Lambda-Cube. [Research Report] LIP RR-2004-08, Laboratoire de l'informatique du parallélisme. 2004, 2+45p. ⟨hal-02101921⟩
18 Consultations
31 Téléchargements

Partager

Gmail Facebook Twitter LinkedIn More