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.
Continuation calculus was discovered when building a toy programming language with continuations. I found no formalism with clean operational semantics, so I sat down and thought about a compilation target for high-level languages with simple operational semantics. My supervisor Herman Geuvers helped me develop the calculus for my master thesis, which has recently led to a paper accepted for publication.
My presentation at a local seminar features a case study where we translate to CC a list multiplication program, that uses continuations/exceptions to optimize some inputs. The CC program is proven correct in our paper, and the reduction length in CC clearly shows where the optimized special case applies.
I’m currently working on a systematic translation from a subset of ML to CC.