preprints about continuations

Types readers may be interested in these two papers about types and
continuations, which will appear in Higher-Order and Symbolic Computation.




Josh Berdine, Peter O'Hearn, Uday Reddy and Hayo Thielecke:
"Linear Continuation-Passing"

Abstract.  Continuations can be used to explain a wide variety of control
be-haviours, including calling/returning (procedures), raising/handling
(exceptions), labelled jumping (goto statements), process switching
(coroutines), and backtrack-ing.  However, continuations are often
manipulated in a highly stylised way, and we show that all of these, bar
backtracking, in fact use their continuations linearly; this is formalised
by taking a target language for CPS transforms that has both
intuitionistic and linear function types.



Hayo Thielecke:
"Comparing Control Constructs by Double-barrelled CPS"

Abstract. We investigate call-by-value 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 Landins
J-operator. In each case there is an associated simple typing. For those
constructs that allow upward continuations, the typing is classical, for
the others it remains intuitionistic, giving a clean distinction
independent of syntactic details. Moreover, those constructs that make the
typing classical in the source of the CPS transform break the linearity of
continuation use in the target.