Games and Full Abstraction for a Functional Metalanguage
                   with Recursive Types 

                    Guy McCusker

ISBN 3-540-76255-9
Springer-Verlag London Limited, 1998

This book develops a theory of game semantics suitable for modelling
programming languages with rich type structure. Game semantics is a
recently discovered setting for the interpretation of sequential
languages which is extremely accurate; in particular, it gave rise to
the first syntax-independent construction of a fully abstract model of
PCF, a simple higher-order functional language, solving a problem
that had been open for 15 years. The work presented here improves and
extends these results to handle both sum types and recursive types. 

  A new category of games is defined and shown to have the
  structure required to model product, function space and sum
  types. This category can be seen as a descendent of those of
  Abramsky et al. and Hyland and Ong which have been used to
  model PCF so successfully, but is richer than those categories
  because of the existence of sums. 

  A theory of recursive types is developed which applies to the
  category of games. Pitts' theory of
  invariant relations is generalized to this setting, providing
  elegant principles for reasoning about recursive types.   

  The structure needed to model Plotkin's FPC, a rich functional
  language with product, function space, sum and recursive types, is
  investigated, and the category of games is shown to be suitable. The
  theory of recursive types developed earlier is used to show that any
  such model, and in particular the games model, is computationally
  adequate and hence sound. 

  The games model of FPC is shown to be fully abstract. The
  model is used to prove some strong properties of FPC which in turn
  yield simple proofs of full abstraction for games models of both a
  call-by-name and a call-by-value untyped lambda-calculus.