@inbook{f77d2f30b97a4378aa91a1ec2b3573e6,

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",

month = jan,

day = "1",

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)",

}