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.
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.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 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.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>
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).cont2 <C2 o C1, v> → cont1 <C1, v, C2>
cont2 <, v> → v