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 :
Reports
Complete list of metadatas

Cited literature [19 references]  Display  Hide  Download

https://hal-lara.archives-ouvertes.fr/hal-02101921
Contributor : Colette Orange <>
Submitted on : Wednesday, April 17, 2019 - 9:09:49 AM
Last modification on : Friday, May 17, 2019 - 1:39:22 AM

File

RR2004-08.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-02101921, version 1

Collections

Citation

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⟩

Share

Metrics

Record views

2

Files downloads

6