THE SEMANTICS OF 2ND-ORDER LAMBDA CALCULUS

In the second-order (polymorphic) typed lambda calculus, lambda abstraction over type variables leads to terms denoting polymorphic functions. Straightforward cardinality considerations show that a naive set-theoretic interpretation of the calculus is impossible. We give two definitions of semantic models for this language and prove them equivalent. Our syntactical "environment model" definition and a more algebraic "combinatory model" definition for the polymorphic calculus correspond to analogous model definitions for untyped lambda calculus. Soundness and completeness theorems are proved using the environment model definition. We verify that some specific interpretations of the calculus proposed in the literature indeed yield models in our sense. © 1990.