Lambda the Ultimate

Continuation calculus ("CC") is an alternative to lambda calculus, where the order of evaluation is determined by programs themselves. CC is a constrained term rewriting system, designed such that continuations are no unusual terms. This makes it natural to model programs with nonlocal control flow, as is the case with exceptions and call-by-name functions. The resulting system has very simple operational semantics.

Because no real pattern matching is possible in CC, we can only examine data through its reduction behavior. This in turn allows us to define values that are compatible to natural numbers or lists, but whose deconstruction requires computation. Such values are similar to call-by-name function applications.

For an introduction, look at the presentation. Details can be found in the paper. You may also experiment with the online evaluator, which has some example programs.

In future work, I will describe a scheme to translate functional programs to continuation calculus. I also plan to describe an applicable type system, but the details have yet to be worked out.