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 Symposium on Logic in Computer Science (LICS 1997)},
    year =	 {1997},
    month =	 {June}, 
    pages =      {76--86},
    location =   {Warsaw, Poland}, 
    publisher =	 {IEEE Computer Society Press}
  }