Skip to Main content Skip to Navigation
New interface
Reports (Research report)

Direct proofs of strong normalisation in calculi of explicit substitutions

Abstract : This paper is part of a general programme of treating explicit substitutions as the primary $\lambda$-calculi from the point of view of foundations as well as applications. Here we investigate the property of strong normalization. To date all the proofs of strong normalization of typed calculi of explicit substitutions use a reduction to the strong normalization of classical $\lambda$-calculus via the so-called ``preservation of strong normalization'' property. This paper develops a new approach, namely a direct proof that the strongly normalizing terms are precisely those typable under the intersection-types discipline. We also define an effective perpetual strategy for the general calculus, give an inductive definition of the strongly normalizing terms, and furthermore show that normalization properties are essentially unaffected by the inclusion of a rule for garbage collection. A key role is played by a certain general combinatorial lemma relating the reduction properties of two interacting abstract reductions, which we feel is of interest in its own right.
Document type :
Reports (Research report)
Complete list of metadata
Contributor : Colette ORANGE Connect in order to contact the contributor
Submitted on : Wednesday, April 17, 2019 - 9:08:57 AM
Last modification on : Wednesday, October 26, 2022 - 8:14:34 AM


Files produced by the author(s)


  • HAL Id : hal-02101884, version 1



Daniel Dougherty, Pierre Lescanne. Direct proofs of strong normalisation in calculi of explicit substitutions. [Research Report] LIP RR-2000-05, Laboratoire de l'informatique du parallélisme. 2000, 2+20p. ⟨hal-02101884⟩



Record views


Files downloads