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.