**Games and Definability for System F**
[pdf -
ps -
ps.gz -
dvi -
bibtex]

*
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*.