Dominic Hughes - Selected Papers

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.