Introduction

The aim of these notes is to explain how games can provide an intensional semantics for functional programming languages, and for a theory of proofs. From the point of view of program semantics, the rough idea is that we can move from modelling computable functions (which give the ‘extensional’ behaviour of programs) to modelling ‘intensional’ aspects of the algorithms themselves. In proof theory, the tradition has been to consider syntactic representations of (what are presumably intended to be ‘intensional’) proofs; so the idea is to give a more intrinsic account of a notion of proof.

Three main sections follow this Introduction. Section 2 deals with games and partial strategies; it includes a discussion of the application of these ideas to the modelling of algorithms. Section 3 is about games and total strategies; it runs parallel to the treatment in Section 2, and is quite compressed. Section 4 gives no more than an outline of more sophisticated notions of game, and discusses them as models for proofs. Exercises are scattered through the text.

I very much hope that the broad outline of these notes will be comprehensible on the basis of little beyond an understanding of sequences (lists) and trees. However the statements of some results and some of the exercises presuppose a little knowledge of category theory, of domain theory and of linear logic.