Strong normalization in type systems: A model theoretical approach

Tait's proof of strong normalization for the simply typed lambda-calculus is interpreted in a general model theoretical framework by means of the specification of a certain theory T and a certain model U of T. The argumentation is partly reduced to formal predicate logic by the application of certain derivability properties of T. The resulting version of Tait's proof is, within the same framework, systematically generalized to the Calculus of Constructions and other advanced type systems. The generalization proceeds along the formal level in the sense that T is modified first and that the new theory partly dictates the subsequent transformation of U, which is carried out in stages. The uniform and standardized character of the argumentation contributes to its perspicuity.