Explicit pure type systems, subject reduction and preservation of strong normalisation

Abstract : Pure type systems are an elegant formalism allowing to specify in a very easy way a large number of type systems. The possibility of their extension to calculi with explicit substitution was the object of numerous studies, which ran into various problems. In particular, the intuitive systems obtained by the mere addition of a cut rule to type substitutions have a major flaw : they do not satisfy subject reduction. In this report, we introduce pure type systems based upon the explicit substitution calculus with names Lambda x, and we show that our systems satisfy among others subject reduction, and that they preserve the strong normalisation of their implicit counterparts.
Document type :
Reports
Complete list of metadatas

https://hal-lara.archives-ouvertes.fr/hal-02102423
Contributor : Colette Orange <>
Submitted on : Wednesday, April 17, 2019 - 11:51:38 AM
Last modification on : Friday, April 19, 2019 - 1:38:13 AM

File

RR2006-35.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-02102423, version 1

Collections

Citation

Romain Kervac. Explicit pure type systems, subject reduction and preservation of strong normalisation. [Research Report] Laboratoire de l'informatique du parallélisme. 2006, 2+69p. ⟨hal-02102423⟩

Share

Metrics

Record views

5

Files downloads

23