On Normalisation

F. van Raamsdonk and P. Severi
CWI technical report CS-R9545

Abstract: Using a characterisation of strongly normalising $\lambda$-terms, we give new and simple proofs of the following: all developments and superdevelopments are finite, a certain rewrite strategy is perpetual, a certain rewrite strategy is maximal and thus perpetual, simply typed $\lambda$-calculus is strongly normalising.