Olivier Danvy5 
| (5) |
BRICS Department of Computer Science, University of Aarhus, Ny Munkegade, Building 540, DK-8000 Aarhus C, Denmark |
Abstract
Continuations occur in many areas of computer science: logic, proof theory, formal semantics, programming-language design
and implementation, and programming. Like the wheel, continuations have been discovered and rediscovered many times, independently.
In programming languages, they represent of “the rest of a computation” as a function, and proved particularly convenient
to formalize control structures (sequence, gotos, exceptions, coroutines, backtracking, resumptions, etc.) and to reason about
them. In the lambda-calculus, terms can be transformed into “continuation-passing style” (CPS), and the corresponding transformation
over types can be interpreted as a double-negation translation via the Curry-Howard isomorphism. In the computational lambda-calculus,
they can simulate monads. In programming, they provide functional accumulators.
Basic Research in Computer Science (www.brics.dk), funded by the Danish National Research Foundation.