Systèmes de types purs et séquents classique. - LARA - Libre accès aux rapports scientifiques et techniques
Rapport (Rapport De Recherche) Année : 2006

Pure type systems and classical sequents

Systèmes de types purs et séquents classique.

Résumé

The bar lambda mu tilde mu-calculus was designed by P.-L. Curien and H.Herbelin. One of its interest is that its terms can be interpreted asderivations in the classical sequent calculus. One of the its lacks isthe fact that it has only simple types. Our purpose here is to extendthe calculus to higher-order types, and especially those of thecalculus of constructions, a calculus designed by T. Coquand and G.Huet in order to provide a very general typed language for proofassistants based on \lambda-calculus. In order to do this, we placeourselves in the framework of pure type systems, which are a verygeneral formalism allowing to represent many interesting type systems,among which those of Barendregt's lambda-cube, which is a hierarchicalpresentation of the calculus of constructions. We show that our systemssatisfy some fundamental properties, such as subject reduction, andstrong normalisation on the lambda-cube.
Fichier principal
Vignette du fichier
RR2006-36.pdf (379 Ko) Télécharger le fichier
Origine Fichiers produits par l'(les) auteur(s)

Dates et versions

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

Identifiants

  • HAL Id : hal-02102422 , version 1

Citer

Romain Kervac. Systèmes de types purs et séquents classique.. [Rapport de recherche] LIP RR-2006-36, Laboratoire de l'informatique du parallélisme. 2006, 2+27p. ⟨hal-02102422⟩
23 Consultations
24 Téléchargements

Partager

More