Title:A New Model Construction for the Polymorphic Lambda Calculus
Author: Dieter Spreen

Abstract:

Various models for the Girard-Reynolds second-order lambda calculus
have been presented in the literature. Except 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
$\omega$-cochains of finite sets. The corresponding morphisms are sequences of
maps acting locally on the finte sets in the $\omega$-cochains. The model can
easily be turned into an effectively given one. Moreover, it can be
arranged in such a way that the universal type $\forall 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.