Service interruption on Monday 11 July from 12:30 to 13:00: all the sites of the CCSD (HAL, Epiciences, SciencesConf, AureHAL) will be inaccessible (network hardware connection).
Skip to Main content Skip to Navigation
Reports

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 metadata

Cited literature [19 references]  Display  Hide  Download

https://hal-lara.archives-ouvertes.fr/hal-02101921
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

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

15

Files downloads

13