IEEE Symposium on Logic in Computer Science

LICS Home - LICS Awards - LICS Newsletters - LICS Archive - LICS Organization - Logic-Related Conferences - Links

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