Games and definability for system F

Abstract

We develop a game-theoretic model of the polymorphic /spl lambda/-calculus, system F, as a fibred category F. Our main result is that every morphism /spl sigma/ of the model defines a normal form s/sub /spl sigma// of system F, whose interpretation is /spl sigma/. Thus the model gives a precise, non-syntactic account of the calculus.