Games and Definability for System F

We present a game-theoretic model of the polymorphic -calculus, system F, as a fibred category. Every morphism of the model defines an -expanded, -normal form ^ of system F whose interpretation is . Thus the model gives a precise, non-syntactic account of the calculus.

• Type: Conference
• Year: 1997
• Where: LICS
• Authors: Dominic J. D. Hughes
• Keywords: Automated Reasoning, Fibred Category, Game-theoretic Model, LICS 1997, Model