Games and Definability for System F
Logic in Computer Science, 1997.
This paper develops a game-theoretic model of the polymorphic
lambda calculus, System F, as a fibred category. The model
provides a precise account of the calculus that is both synthetic and
syntax-free. The main result is that every strategy s defines a
normal form n(s) of System F, whose interpretation is s.