Typing and computational properties of lambda expressions (Q1819575)

This paper integrates and generalizes known techniques and results (in particular, by the works of Girard and Coppo, Dezani \& Veneri) relating typing to convergence properties (such as normalizability) in the lambda calculus. It does so by considering types as semantical properties of \(\lambda\)-expressions in second-order models over \(\lambda\)-expressions. Working in the semantic discipline permits a richer notion of type and, therefore, more general results.