This thesis introduces hypergame semantics, a second-order extension of game semantics in which games themselves can be played as moves. The mathematical structure on hypergames is a lambda-X-hyperdoctrine (split cloven fibration), providing a model of the polymorphic lambda calculus, system F.
It is the first fully complete model of the polymorphic lambda calculus: every element of the model is the interpretation of a term. Thus from a computer science perspective we obtain a precise characterisation of parametric polymorphism; from a foundational mathematics perspective we obtain a precise characterisation of the proof theory of propositional second-order inituitionistic logic.