Skip to Main content Skip to Navigation

Explicit Pure Type Systems for the Lambda-Cube

Abstract : 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.
Document type :
Complete list of metadata

Cited literature [19 references]  Display  Hide  Download
Contributor : Colette Orange Connect in order to contact the contributor
Submitted on : Wednesday, April 17, 2019 - 9:09:49 AM
Last modification on : Saturday, September 11, 2021 - 3:19:17 AM


Files produced by the author(s)


  • HAL Id : hal-02101921, version 1



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⟩



Les métriques sont temporairement indisponibles