A BRICS Mini-Course
March 14, 19 and 21, 2002
Lectures by
Olivier Danvy, danvy@brics.dk
BRICS
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.
Yet continuations are remarkably elusive. They can be explained in five minutes, but grasping them seems to require a lifetime. Consequently one often reacts to them to an extreme, either loving them (``to a man with a hammer, the world looks like a nail'') or hating them (``too many lambdas'').
The mini-course addresses continuations both conceptually, theoretically, and practically. While continuations are not an end in themselves, it is the consistent experience of the lecturer that any new understanding of continuations is accompanied by a new understanding in other areas in computer science.