appeared in the Archive for Mathematical Logic 42, 59-87 (2003)
Erratum to the published version and hence also to this version and the 1999 version: PDF (2 pages, November 2004). Every statement is correct but two lemmas concerning permutative conversions need a change in the organization of their proofs.
Slides for a talk on the parts without permutative conversions on May 30, 2002 are available here.
Those who know the 1998 version might want to read the following:
Short Proofs of Normalization for the simply-typed lambda-calculus, permutative conversions and Gödel's T by Ralph Matthes and Felix Joachimski Version as of Nov 11, 1999 The major changes relative to the 1998 version: A new section (6) with a new lambda calculus with generalized application: Strong normalization is our new result (solving a problem raised by Jan von Plato). Even Kappa (=immediate simplification) included. Shows our ability to efficiently handle permutative conversions which we see as a major achievement of the paper. Treatment of Eta clearer for -> and new for + (not covered by de Groote) Treatment of T much smoother: We only have to prove more closure properties of SN (via value expansion). Further Comments: The normalization algorithms are not seen as the outcome of the respective sections but as some summary which comes for free. The SN method may be seen as a way of reducing the cut rank to zero in one pass. Hence, it is not designed with the aim to conduct fine-grained analysis of reduction lengths. The issue of formalizability in theorem proving systems on computers is important, and the proofs are indeed well-suited for that purpose as shown by Tobias Nipkow for the Isabelle system. We also could have included a forward (w.r.t. our original submission date) reference to Goguen's TLCA 99 paper which shows how to extend our method to dependent types (i. e., to Martin-Löf's Logical Framework).