08/04/2003
Hayo Thielecke (University of Birmingham)
Comparing Control Constructs by Typing Double-barrelled CPS Transforms

We investigate continuation-passing style transforms that pass two continuations. Altering a single variable in the translation of lambda-abstraction gives rise to different control operators: first-class continuations; dynamic control; and (depending on a further choice of a variable) either the return statement of C; or Landin's J-operator. In each case there is an associated simple typing. For those constructs that allow upward continuation, the typing is classical; for the others it remains intuitionistic, giving a clean distinction independent of syntactic details.