Typing and computational properties of lambda expressions

AbstractWe use a perception of second-order typing in the λ-Calculus, as conveying semantic properties of expressions in models over λ-expressions, to exhibit natural and uniform proofs of theorems of Girard (1971/1972) and of Coppo, Dezani and Veneri (1981) about the relations between typing properties and computational properties of λ-expressions (solvability, normalizability, strong normalizability), and of some generalizations of these theorems