# Logic in Computer Science (LICS 1997)

## Paper: Games and Definability for System F (at LICS 1997)

Authors: Dominic J. D. Hughes

### Abstract

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}
}