Strong normalization in type systems: A model theoretical approach Original Research Article

Taitʹs proof of strong normalization for the simply typed λ-calculus is interpreted in a general model theoretical framework by means of the specification of a certain theory T and a certain model /oU 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 /oU, which is carried out in stages. The uniform and standardized character of the argumentation contributes to its perspicuity.