Relating Models of Polymorphism

Abstract

A new general notion of model for the polymorphic lambda calculus based on the simple idea of a universe, is proposed. Although impossible in nonconstructive set theory, the notion is unproblematic for constructive sets, yields completeness and initiality theorems, and can be used to unify and relate many different notions of model that have been proposed in the literature, including those that extend the basic calculus with additional features such as fixpoints or a type of all types. Moreover, the polymorphic lambda calculus and Martin-Lof type theory are related by a map of logics. A categorical and initial model semantics is given for the basic calculus and for richer calculi that extend the basic one with fixpoints or with a type of all types.