Higher-Order and Symbolic Computation, 15(2/3)141-160
Comparing Control Constructs by Double-Barrelled CPSHayo Thielecke, School of Computer Science, University of Birmingham, Birmingham B15 2TT, United Kingdom
|
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 Landin's 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.
Keywords: continuations, control operators, J-operator, intuitionistic and classical logic |
This article can be downloaded [here].
![[picture of journal cover]](../LISP.JPG)