A new model construction for the polymorphic lambda calculus

Abstract

Various models for the Girard-Reynolds second-order lambda calculus have been presented in the literature. Except for the term model they are either realizability or domain models. In this paper a further model construction is introduced. Types are interpreted as inverse limits of ω-cochains of finite sets. The corresponding morphisms are sequences of maps acting locally on the finite sets in the ω-cochains. The model can easily be turned into an effectively given one. Moreover, it can be arranged in such a way that the universally quantified type ∀t.t representing absurdity in the higher-order logic defined by the type structure is interpreted by the empty set, which means that it is also a model of this logic.