Higher-Order and Symbolic Computation, 15(2/3)181-208
Linear Continuation-PassingJosh Berdine, Department of Computer Science, Queen Mary, University of London, London E1 4NS, United Kingdom
Peter O'Hearn, Department of Computer Science, Queen Mary, University of London, London E1 4NS, United Kingdom
Uday Reddy, School of Computer Science, The University of Birmingham, Birmingham B15 2TT, United Kingdom
Hayo Thielecke, School of Computer Science, The University of Birmingham, Birmingham B15 2TT, United Kingdom
|
Abstract: Continuations can be used to explain a wide variety
of control behaviours, including calling/returning (procedures),
raising/handling (exceptions), labelled jumping (goto statements),
process switching (coroutines), and backtracking. 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.
Keywords: continuations, continuation-passing style, linear typing, call/cc, exceptions, goto, coroutines |
This article can be downloaded [here].
![[picture of journal cover]](../LISP.JPG)