Games and Full Abstraction for FPC

I would like to announce the availability of my PhD thesis

        Games and Full Abstraction 
       for a Functional Metalanguage
           with Recursive Types

and of the paper

        Games and Full Abstraction for FPC (full version).

(The abstracts are below.) 
Both documents are available from my web page


or from the Hypatia electronic archive


(search for "McCusker"). 

They can also be obtained by anonymous ftp from the Imperial College archive


 in directory papers/McCusker/

        Games and Full Abstraction 
       for a Functional Metalanguage
           with Recursive Types
             Guy McCusker

This thesis 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. 

o 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, Jagadeesan aand Malacaria 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. 

o 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.   

o 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. 

o 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. 


  Games and Full Abstraction for FPC (full version)

       Guy McCusker

We present a new category of games, G, and build from it a cartesian
closed category I and its extensional quotient E. E represents an
improvement over existing categories of games in that it has sums as
well as products, function spaces and recursive types. A model of the
language FPC, a sequential functional language with just this type
structure, in E is described and shown to be fully abstract. 

An extended abstract of this work appeared in the proceedings of 
LICS '96.