Paper: Games and Definability for System F (at LICS 1997)
Authors: Dominic J. D. HughesAbstract
We develop a game-theoretic model of the polymorphic lambda-calculus, system F, as a fibred category \mathbb{F}. Our main result is that every morphism \sigma of the model defines a normal form s_\sigma of system F, whose interpretation is \sigma. Thus the model give a precise, non-syntactic account of the calculus.
BibTeX
@InProceedings{Hughes-GamesandDefinabilit, author = {Dominic J. D. Hughes}, title = {Games and Definability for System F}, booktitle = {Proceedings of the Twelfth Annual IEEE Symp. on Logic in Computer Science, {LICS} 1997}, year = 1997, editor = {Glynn Winskel}, month = {June}, pages = {76--86}, location = {Warsaw, Poland}, publisher = {IEEE Computer Society Press} }