A general method to prove the normalization theorem for first and second order typed lambda-calculi

In this paper we describe a method to prove the normalization property for a large variety of typed lambda calculi of first and second order, based on a proof of equivalence of two deduction systems. We first illustrate the method on the elementary example of simply typed lambda calculus and then we show how to extend it to a more expressive dependent type system. Finally we use it to prove the normalization theorem for Girard's system F