Shift and reset via two-continuations

I did a little pleasure-reading while I was out of town this weekend. Biernacki, Danvy, and Shan have a paper on delimited continuations with a nice formulation of shift and reset based on Filinski's specification. Filinski's approach is to evaluate every expression in two continuations. The first is the local continuation, representing the dynamic context up to the nearest delimiter. The second is the global continuation (which he calls the "meta-continuation"), representing everything above the delimiter. The nice thing about separating these two is that control effects are only able to affect the local continuation; the global continuation is completely off-limits to the user program.

Filinski uses a two-continuation version of CPS for his specification, but Biernacki et al give a nice CEK machine semantics (which I have a certain fondness for). The two continuations are represented as evaluation contexts, which themselves are represented as composable sequences of context frames.

The first rules specify the evaluation of a term. The interesting rules are the last two: installing a prompt promotes the current local continuation to "inviolable" status by placing it in the global continuation; and capturing the current local continuation removes it and stores it in the environment.

eval <x, e, C1, C2>     → cont1 <C1, e(x), C2>
eval <λx.t, e, C1, C2>  → cont1 <C1, [x,t,e], C2>
eval <t0 t1, e, C1, C2> → eval <t0, e, C1 o (t1 [])^e, C2>
eval <#t, e, C1, C2>    → eval <t, e, [], C2 o C1>
eval <Sk.t, e, C1, C2>  → eval <t, e[k := C1], [], C2>

The second set of rules represent returning a value to the local continuation. The most interesting rules is the last one, which represents applying a captured continuation: it simulates "returning" the operand to the captured continuation and saves the current local continuation in the global continuation, so as to preserve the current state of the computation.

cont1 <[], v, C2>                → cont2 <C2, v>
cont1 <C1 o (t [])^e, v, C2>     → eval <t, e, C1 o (v []), C2>
cont1 <C1 o ([x,t,e] []), v, C2> → eval <t, e[x := v], C1, C2>
cont1 <C1 o (C1' []), v, C2>     → cont1 <C1', v, C1 o C2>

The last rules represent returning values to the global continuation. If it has some local computing to do, that gets placed back into the local continuation, and otherwise it returns the final value.

cont2 <C2 o C1, v> → cont1 <C1, v, C2>
cont2 <[], v>      → v

This is a lovely presentation of delimited continuations. I'd also never thought of the connection between delimited continuations and two-continuation backtracking (having still never read Filinski's work).