@inbook{b10d441300b14aaab981dcb59ef3cf8d,
title = "A normalisation result for higher-order calculi with explicit substitutions",
abstract = "Explicit substitutions (ES) were introduced as a bridge between the theory of rewrite systems with binders and substitution, such as the λ-calculus, and their implementation. In a seminal paper P.-A. Melli{\`e}s observed that the dynamical properties of a rewrite system and its ES-based implementation may not coincide: he showed that a strongly normalising term (i.e. one which does not admit infinite derivations) in the λ-calculus may lose this status in its ES-based implementation. This paper studies normalisation for the latter systems in the general setting of higher-order rewriting: Based on recent work extending the theory of needed strategies to non-orthogonal rewrite systems we show that needed strategies normalise in the ES-based implementation of any orthogonal pattern higher-order rewrite system.",
author = "Eduardo Bonelli",
year = "2003",
doi = "10.1007/3-540-36576-1_10",
language = "English",
isbn = "3540008977",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
pages = "153--168",
editor = "Gordon, {Andrew D.}",
booktitle = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
}