@inbook{fb1ac4545749424886e0f6142cfa2a47,
title = "A Direct Proof of Strong Normalization for an Extended Herbelin's Calculus",
abstract = "Herbelin presented (at CSL'94) an explicit substitution calculus with a sequent calculus as a type system, in which reduction steps correspond to cut-elimination steps. The calculus, extended with some rules for substitution propagation, simulates β-reduction of ordinary λcalculus. In this paper we present a proof of strong normalization for the typable terms of the calculus. The proof is a direct one in the sense that it does not depend on the result of strong normalization for the simply typed A-calculus, unlike an earlier proof by Dyckhoff and Urban.",
author = "Kentaro Kikuchi",
year = "2004",
doi = "10.1007/978-3-540-24754-8_18",
language = "English",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "244--259",
editor = "Yukiyoshi Kameyama and Stuckey, {Peter J.}",
booktitle = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
address = "Germany",
}