[Prev][Next][Index][Thread]
Game semantics as continuation passing
-
To: types@cs.indiana.edu
-
Subject: Game semantics as continuation passing
-
From: Paul Levy <pbl@dcs.qmw.ac.uk>
-
Date: Fri, 24 Apr 1998 13:49:45 +0100 (BST)
-
Delivery-Date: Fri, 24 Apr 1998 07:50:24 -0500
The following is available by anonymous ftp on the site
ftp://ftp.dcs.qmw.ac.uk/pub/lfp/pbl/mfcs.ps
-------------------------------------------------------------------------------
Game Semantics as Continuation Passing (extended abstract)
We show that the game semantics of Hyland, Ong and Nickau and related
game semantics factorize via continuation-passing style (CPS)
transforms. We provide a comparatively simple game semantics for a
typed language $\Sigma \neg$-calculus that can be seen as the target
of these transforms. This elucidates some key concepts of game
semantics. We see that the role of \emph{pointers between moves} is to
indicate the time of receipt of the continuation being thrown
to. \emph{Arenas} are seen to be type normal forms in
$\Sigma\neg$-calculus.
--
===========================================================================
Paul Blain Levy, Department of Computer Science,
Queen Mary and Westfield College, LONDON E1 4NS
http://www.dcs.qmw.ac.uk/~pbl/
===========================================================================