[Prev][Next][Index][Thread]
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.
Regards,
Hayo
-------------------------------------------------
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.
http://www.cs.bham.ac.uk/~hxt/research/LinCP.pdf
---------------------------------------------
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.
http://www.cs.bham.ac.uk/~hxt/research/HOSC-double-barrel.pdf
-----------------------------------------------