10/01/2002: Paul Levy (PPS)
Jump-With-Argument and its Pointer Game Model.

Résumé

Jump-With-Argument (JWA) is a typed language of continuations (in fact, it is an extension of Thielecke's CPS calculus). We present the language and show how to execute a program by jumping around a tree (essentially the environment) which grows during execution. The idea that a continuation is a point we jump to is decades-old, and is how Steele understood CPS code, so this will all be rather familiar to people who have worked with continuation based compilers.
We explain how to build a pointer game model for JWA. (A "pointer game" is a game in the style of Hyland-Ong, where (almost) every move includes a pointer back to a previous move of the other player.) What is original is not the model itself---which is essentially the same as Laird's, and therefore does not use a bracketing condition---but the operational way in which we motivate it.
First, we see how every JWA type is isomorphic to a canonical form, and that it is convenient to represent this canonical form as a family of forests or "arenas" (as in Abramsky-McCusker's call-by-value games).
We see how in each jump in and out of a subterm of type canonical form, we take a tag (something like a boolean or number)---this is represented in the game by a token in the arena---and a continuation, which does not need to be represented at all. We also have to indicate the time of receipt of the continuation being jumped to; this is the job of the pointer.
We see the role of the present branch of the tree (the "Player-view" in Hyland-Ong's terminology). We see how, if Player can store ground data, he can exploit information outside the present branch (i.e. behave non-innocently) but still cannot jump to a continuation received outside the present branch. If Player can furthermore store continuations, he can jump to a continuation received at *any* time in the past (i.e. break the P-visibility condition). Thus we provide some operational motivation for the relaxing of constraints in the storage models of Abramsky-McCusker-Honda.
Several languages can be compiled into Jump-With-Argument (call-by-value,call-by-name,call-by-push-value,control operators). So what we do here sheds some light on the pointer game models for those languages. We take a look at the case of call-by-value, because its CPS transform is the easiest.