Dominic Hughes - Selected Papers

Hypergame Semantics: Full Completeness for System F [pdf - pdf.gz - ps - ps.gz]
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.