D.Phil. (=Ph.D.) Mathematical Sciences, Oxford University, 2000.

Supervisor: Luke Ong. External Examiner: Samson Abramsky (then at Edinburgh). Internal Examiner: Bill Roscoe.

Game semantics models a program or proof interactively as a strategy in a game, a stimulus-response behaviour for Program/Prover against Environment/Refuter. The objective is to capture the meaning of programs and proofs in an abstract, syntax-free form.

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.