Title: New Notions of Reduction and Non-Semantic Proofs of Beta-Strong
       Normalization in Typed Lambda-Calculi 
Author: A. J. Kfoury and J. B. Wells
Date: December 19, 1994

Abstract:

Two new notions of reduction for terms of the lambda-calculus are
introduced and the question of whether a lambda-term is beta-strongly
normalizing is reduced to the question of whether a lambda-term is merely
normalizing under one of the new notions of reduction.  This leads to a
new way to prove beta-strong normalization for typed lambda-calculi.
Instead of the usual semantic proof style based on Girard's ``candidats de
r\'eductibilit\'e'', termination can be proved using a decreasing metric
over a well-founded ordering in a style more common in the field of term
rewriting.  This new proof method is applied to the simply-typed
lambda-calculus and the system of intersection types.