[Prev][Next][Index][Thread]
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
http://www.comlab.ox.ac.uk/oucl/users/guy.mccusker/
or from the Hypatia electronic archive
http://hypatia.dcs.qmw.ac.uk/
(search for "McCusker").
They can also be obtained by anonymous ftp from the Imperial College archive
theory.doc.ic.ac.uk
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.