Control Operators and Classical Proofs

Prerequisites. Direct starred prerequisites: none. No later core chapter depends on this route.

An exception discards the rest of a computation. It cannot save that rest, pass it to a function, and invoke it twice. A continuation is a value representing that remaining computation; it can be saved, passed to a function, and invoked more than once. A control operator captures or invokes continuations, enabling early return, backtracking, and coroutines; under propositions as types it also validates classical principles which have no intuitionistic proof.

The mechanism reifies the current call-by-value evaluation context as a value. Under propositions as types this value implements double-negation elimination, and hence excluded middle.

A stack that can become a value

The complete control-machine and proof-term rule sheets are collected in subappendix A.32; the main text derives the rules needed by each worked trace.

We write $e{⇝}_0{e}^{\prime }$ for one root contraction. We extend the call-by-value simply typed calculus of chapter 2. Products, sums, the empty type, unit, and arrows retain their earlier rules. We add the base type $\mathsf{Nat}$, its numerals, and, for the calculations below, ${\mathsf{add}}_m:\mathsf{Nat}\to \mathsf{Nat}$, a primitive value with ${\mathsf{add}}_{m}n{⇝}_{0}m+n$. This harmless constant avoids hiding control behind an arithmetic encoding.

We write ${\pi }_1,{\pi }_2$ for the earlier $\mathsf{fst},\mathsf{snd}$, and write a case with named $\mathsf{inl}$ and $\mathsf{inr}$ branches. Only the typography changes; the retained typing and reduction rules do not. We retain $\mathbf{0}$ and $\mathbf{1}$ for the inherited empty and unit types, and write $()$ for the earlier unit value $\star$.

If $\mathsf{Cont}A$ is read operationally as an object-language representation of a refutation of $A$, T-Letcc is the classical step known as consequentia mirabilis: from a derivation of $A$ under a temporary refutation of $A$, conclude $A$. Removing T-Letcc, T-Throw, and $\mathsf{Cont}$ leaves the inherited intuitionistic simply typed calculus.

The pure transitions are written out because the stack captured by $\mathsf{letcc}$ includes precisely these frames. Values change the direction of the machine: $$K▹v\stackrel{M-Return}{⟶}K◃v.$$ Application and pairs use Injections first evaluate their payload. A case first evaluates its scrutinee, then selects and substitutes: and, writing $\mathcal{B}$ for the displayed pair of case branches, Empty elimination evaluates its impossible premise: $$K▹{\mathsf{abort}}_A(e)\stackrel{M-Abort}{⟶}K;{\mathsf{abort}}_A([])▹e.$$ There is no return transition for this frame, because no well-typed value has type $\mathbf{0}$. Unit, numerals, lambda abstractions, and primitive functions are values. The primitive arithmetic return is $$K;{\mathsf{add}}_m[]◃n\stackrel{M-Add}{⟶}K◃(m+n).$$

Only the following transitions mention control: The last line visibly discards $K$, including the two throw frames, and restores $K^{\prime }$. A continuation is persistent: throwing to it does not consume the stored stack.

This is the typed core of the familiar $\mathsf{call}\mathsf{/}\mathsf{cc}$ idiom. The term $\mathsf{letcc}k\mathsf{in}e$ captures the current continuation, binds it to $k$, and evaluates $e$. In particular, the usual typed shape, Peirce’s law, is definable: The inner throw is assigned result type $B$. The hypothetical dependent ${\mathsf{callcc}}_k$ of the final section is a different, explicitly call-by-name construct.

A nonlocal trace

Put $$K_0:=\bullet ;{\mathsf{add}}_1[],K_1:=K_0;{\mathsf{add}}_2[].$$ Call by value evaluates $$p:={\mathsf{add}}_1(\mathsf{letcc}k:\mathsf{Cont}\mathsf{Nat}\mathsf{in}{\mathsf{add}}_2(\mathsf{throw}40\mathsf{to}k))$$ as follows. The initial application first reaches where $e_2=\mathsf{letcc}k\mathsf{in}{\mathsf{add}}_2(\mathsf{throw}40\mathsf{to}k)$. Rule M-Capture substitutes the whole outer addition stack: where $e_3=\mathsf{throw}40\mathsf{to}\mathsf{cont}(K_0)$. The result is $41$, not $43$. Reinstating $K_0$ erases the pending ${\mathsf{add}}_2$ frame. An exception can produce the same early return; the difference appears when $\mathsf{cont}(K_0)$ is stored and invoked again.

Typing frames and states

Fix an ambient answer type $R$ for one run. The runtime judgment $\mathrm{\Gamma }{⊢}_{R}e:A$ has all the surface rules and the internal continuation rule displayed below. On source terms it agrees with $\mathrm{\Gamma }⊢e:A$. The frame judgment $F:A\Rightarrow B$ is defined so that plugging a value $v:A$ into $F$ produces the next computation of type $B$. Its term premises use the fixed ambient $R$: The bracketed notation in the case row means the branch has the displayed single free variable and becomes closed when that variable is replaced. The result $B$ in the two throw rows is arbitrary, exactly as in T-Throw.

Stacks compose by

$\bullet :R\Rightarrow R$

$K:B\Rightarrow R$$F:A\Rightarrow B$

$K;F:A\Rightarrow R$

The internal value rule and state judgments are

$K:A\Rightarrow R$

${⊢}_R\mathsf{cont}(K):\mathsf{Cont}A$

$K:A\Rightarrow R$${⊢}_{R}e:A$

${⊢}_{R}K▹e$

$K:A\Rightarrow R$${⊢}_{R}v:A$

${⊢}_{R}K◃v$

The subscript is essential: it prevents a continuation captured in a run returning $R$ from being installed in a run returning an unrelated type. Only closed runs are needed here. An open machine can instead thread one term context through every frame while retaining the same ambient answer.

Proof of Lemma 35.2 — Closed value substitution and canonical continuations

Proof. Substitution is induction on typing. In the T-Letcc case, rename its bound continuation away from $x$ and the free variables of $v$; apply the induction hypothesis to the body and rebuild T-Letcc. In T-Throw, apply the two induction hypotheses to the value and continuation premises; the arbitrary result type is unchanged. The pure binder case is the same alpha-renaming argument for lambda abstraction, and products, sums, and elimination rules follow premise by premise.

For canonical forms, inspect the value grammar and invert the introduction rule for each form. Lambdas and the primitive ${\mathsf{add}}_m$ are the only arrow values; pairs and the two injections are the only product and sum values; no introduction rule concludes $\mathbf{0}$; and the only continuation form is $\mathsf{cont}(K)$, whose T-Cont premise gives the required stack typing. The ground forms have base types and cannot enter the other cases. ◻

Proof of Theorem 35.3 — Machine preservation

Proof. The proof is by cases on the transition. Pushing a frame factors a stack typing through K-Push; returning to it composes the type promised by the frame with the rest of the stack. Application beta uses substitution. Pair, projection, injection, case, empty elimination, and arithmetic transitions use the corresponding frame row and, for case, substitution into the selected branch. Empty elimination has only its push case. These cases account for every pure transition displayed above.

For capture, inversion gives $K:A\Rightarrow R$ and $k:\mathsf{Cont}A⊢e:A$. Rule T-Cont types $\mathsf{cont}(K):\mathsf{Cont}A$; substitution gives the reduct type $A$, so S-Eval restores state type $R$.

For the first throw transition, inversion of T-Throw gives $e_1:A$, $e_2:\mathsf{Cont}A$, and the arbitrary source result $B$. The frame $\mathsf{throw}[]\mathsf{to}{e}_2:A\Rightarrow B$ extends the stack. Returning the first value changes to the second throw frame, whose typing is $\mathsf{Cont}A\Rightarrow B$. In the final control transition, canonical forms gives $v_2=\mathsf{cont}(K^{\prime })$ with $K^{\prime }:A\Rightarrow R$; the stored value has type $A$. Hence $K^{\prime }◃v$ has the original state type $R$, even though the current stack was discarded. ◻

Proof of Theorem 35.4 — Machine progress

Proof. An evaluation state containing a value takes the direction-change rule. Every nonvalue has a unique outer constructor and therefore takes its unique displayed push, capture, or throw transition.

For a return state, an empty stack is final. Otherwise inspect its unique top frame. The first application, pair, injection, case, and throw frames advance to their second phase. The second application frame contains a function value, hence a lambda or the appropriate primitive by canonical forms. Projection receives a pair; case receives an injection; the second throw frame receives $\mathsf{cont}(K^{\prime })$ by lemma 35.2. Thus each has exactly one transition. An abort frame would have to receive a value of type $\mathbf{0}$, which canonical forms excludes. The frame grammar has no remaining case. ◻

Proof of Corollary 35.5 — Safety

Proof. Induct on the run using preservation. Progress classifies the endpoint. ◻

Compiling control into pure functions

The stack judgment $K:A\Rightarrow R$ is represented in the target by a function $A^{\star }\to R$. This is continuation-passing style (CPS): each computation receives an extra function describing what to do with its result, and calls that function instead of returning directly. The target is the pure simply typed calculus with the same base types, products, sums, and empty type $\mathbf{0}$, but without $\mathsf{Cont}$, $\mathsf{letcc}$, or $\mathsf{throw}$. Its compatible $\beta \delta$-reduction is strongly normalizing.

Proof of Proposition 35.6 — Normalization of the CPS target

Proof. The reducibility proof of theorem 2.43 applies unchanged to products, sums, unit, empty type, and arrows. Interpret the new base type $\mathsf{Nat}$ by the strongly normalizing terms of that type. Numerals belong to this candidate. To add ${\mathsf{add}}_m$, the only new candidate obligation says that ${\mathsf{add}}_{m}t$ is strongly normalizing whenever $t$ is. Compatible reduction of a finite term is finitely branching, with successors canonically enumerated by the finitely many redex positions and the finite rule list. Thus no choice function is used. The elementary finitely-branching form of König’s lemma says that an unbounded-height reduction tree would have an infinite branch; strong normalization excludes that branch, so the tree from $t$ has a maximum branch length. Induction on that height handles steps inside $t$; when $t$ is the numeral $n$, the sole new root step is ${\mathsf{add}}_{m}n{⟶}_{\beta \delta }m+n$, whose reduct is a numeral. Thus the fundamental reducibility lemma, and hence strong normalization, extends to the target used here. ◻

With $\mathbf{0}$ read as falsehood, the computation type is the explicit double-negation translation $A^{\mathsf{c}}=\mathrm{\neg }\mathrm{\neg }{A}^{\mathsf{v}}$. This is a call-by-value CPS translation rather than Kolmogorov’s formula translation: sums, products, and arrows are translated first as value types and the outer double negation is added to a computation. The theorem proved here is typed source-to-target simulation. No converse translation, reflection of provability, or completeness theorem for a separately presented classical proof system is claimed.

The translation separates source values from computations. On values it is homomorphic except at functions and reified stacks: In chapter 22, a superscript $\mathsf{v}$ named the call-by-value translation into CBPV. Here $\mathsf{v}$ and $\mathsf{c}$ name the value and computation parts of this CPS translation. For every source value, the computation clause is uniformly $v^{\mathsf{c}}=\lambda k.k{v}^{\mathsf{v}}$. The composite clauses below apply only when their whole subject is not a value. This disjointness matches the value-first side conditions of M-PairL, M-Inl, and M-Inr, so the translation is a function on syntax rather than two overlapping equations. The arithmetic function has the exact value translation $${\mathsf{add}}_m^{\mathsf{v}}=\lambda n:\mathsf{Nat}.\lambda k:\mathsf{Nat}\to \mathbf{0}.k({\mathsf{add}}_{m}n).$$ A stack value is translated below, because its function depends on the final answer continuation of the whole run.

The machine example has a short CPS image. For fresh $h:\mathsf{Nat}\to \mathbf{0}$, set $q:=\lambda a.{\mathsf{add}}_1^{\mathsf{v}}ah$. Unfolding the application and capture clauses, then contracting administrative beta redexes, gives The continuation supplied while translating ${\mathsf{add}}_2$ is ignored by the translated throw, exactly as the machine discarded the pending ${\mathsf{add}}_2$ frame. Thus the target calculation displays the same $41$, rather than $43$, as the source trace.

Proof of Lemma 35.10 — CPS substitution

Proof. Induct on $e$, alpha-renaming lambda and $\mathsf{letcc}$ binders before descending. Every structural clause distributes substitution to its subterms. In the control clauses, a continuation variable is an ordinary target variable of function type $A^{\mathsf{v}}\to \mathbf{0}$. The internal continuation case is the same target substitution after replacing the stack by its function. ◻

The fresh $h$ is necessary. There is no closed target function $R^{\mathsf{v}}\to \mathbf{0}$ in general, so an empty source stack cannot be represented by a closed target continuation. Strong normalization holds for well-typed open target terms as well, so keeping $h$ free costs nothing.

Proof of Theorem 35.11 — CPS type preservation

Proof. The three claims are simultaneous induction on runtime value, term, frame, and stack typing. A variable or base value is passed to a continuation of its value type. The internal T-Cont case uses the stack induction hypothesis to type $K_h^{\mathsf{k}}:A^{\mathsf{v}}\to \mathbf{0}$. For a lambda, the induction hypothesis gives $e_h^{\mathsf{c}}:B^{\mathsf{c}}$ under $x:A^{\mathsf{v}}$; hence the value inside the outer continuation has type $A^{\mathsf{v}}\to B^{\mathsf{c}}=(A\to B{)}^{\mathsf{v}}$. For application, the successive binders in $$\lambda k.e_1^{\mathsf{c}}(\lambda f.e_2^{\mathsf{c}}(\lambda a.fak))$$ have types $B^{\mathsf{v}}\to \mathbf{0}$, $A^{\mathsf{v}}\to \mathbf{0}$, and $(A^{\mathsf{v}}\to B^{\mathsf{c}})\to \mathbf{0}$, in that order from the inside out. Thus the whole term has type $B^{\mathsf{c}}$.

Pairing sequences values of types $A^{\mathsf{v}}$ and $B^{\mathsf{v}}$ before passing their pair. Projection passes an $A^{\mathsf{v}}\times B^{\mathsf{v}}$ value to a target projection. Injection and case use the corresponding target sum rules; in the two case branches the corresponding induction hypothesis is applied under the same assumption $k:C^{\mathsf{v}}\to \mathbf{0}$. For empty elimination, apply the premise translation to $\lambda z:\mathbf{0}.z$; its result is $\mathbf{0}$, so abstracting the unused continuation gives $A^{\mathsf{c}}$. Variables, abstractions, applications, pairs, projections, injections, case, and empty elimination exhaust the pure source constructors.

For T-Letcc, the target variable $\kappa :A^{\mathsf{v}}\to \mathbf{0}=(\mathsf{Cont}A{)}^{\mathsf{v}}$ has exactly the type assigned to the translated source variable. The body induction hypothesis types $e^{\mathsf{c}}[\kappa /k]:(A^{\mathsf{v}}\to \mathbf{0})\to \mathbf{0}$; applying it to $\kappa$ gives $\mathbf{0}$, and abstracting over $\kappa$ gives $A^{\mathsf{c}}$. For T-Throw, write the two source premises as $e_1:A$ and $e_2:\mathsf{Cont}A$. The innermost target application has $$c:A^{\mathsf{v}}\to \mathbf{0},a:A^{\mathsf{v}},ca:\mathbf{0}.$$ It is a continuation accepted by $e_2^{\mathsf{c}}$; that result is a continuation accepted by $e_1^{\mathsf{c}}$. The unused outer binder may have type $B^{\mathsf{v}}\to \mathbf{0}$, so the result is $B^{\mathsf{c}}$ for the arbitrary source type $B$.

For the stack cases, each clause of definition 35.9 has as domain the translated input of its top frame and calls $K_h^{\mathsf{k}}$ only with the frame’s translated output. The abort frame and two throw clauses have result $\mathbf{0}$ without calling $K_h^{\mathsf{k}}$, exactly as their arbitrary frame result requires. Applying the term or value translation to the resulting function proves the state claim. ◻

Proof of Theorem 35.12 — Positive-step machine simulation

Proof. Expand the term and top-frame translations. The direction change for a value is $$(\lambda k.k{v}_h^{\mathsf{v}})K_h^{\mathsf{k}}{⟶}_{\beta }{K}_h^{\mathsf{k}}{v}_h^{\mathsf{v}}.$$ The application push is $$(e_1{e}_2{)}_h^{\mathsf{c}}{K}_h^{\mathsf{k}}{⟶}_{\beta }(e_1{)}_h^{\mathsf{c}}(\lambda f.(e_2{)}_h^{\mathsf{c}}(\lambda a.fa{K}_h^{\mathsf{k}})),$$ which is exactly the translation of $K;[]e_2▹e_1$. Returning a function contracts the outer binder of this displayed continuation; returning its argument contracts the next binder and then target beta. By lemma 35.10, the endpoint is $(e[v/x]{)}_h^{\mathsf{c}}{K}_h^{\mathsf{k}}$, the translation of the source beta state.

The remaining pure pushes are not implicit. Expanding their outer CPS binders gives Returning the first pair component contracts the $a$-binder and produces the second pair frame; returning the second contracts the $b$-binder and produces $K_h^{\mathsf{k}}⟨v_1^{\mathsf{v}},v_2^{\mathsf{v}}⟩$. Projection return contracts the frame binder and the target projection. Injection return contracts its payload binder. Either case return contracts the scrutinee binder, takes the matching target sum contraction, and uses CPS substitution in the selected branch. No abort return is typable.

For the primitive, put $$s_{\mathsf{add}}:=K;{\mathsf{add}}_m[]◃n.$$ Also abbreviate the translated frame by $$L_h:=\lambda a.{\mathsf{add}}_m^{\mathsf{v}}a{K}_h^{\mathsf{k}}.$$ The generic application-frame clause and the displayed translation of ${\mathsf{add}}_m$ give Thus the primitive source step is represented by beta steps followed by the target primitive’s $\delta$-step. Every pure transition family is now covered.

Capture gives the characteristic equation where the equality is the internal case of CPS substitution. The initial throw push is $$(\mathsf{throw}{e}_1\mathsf{to}{e}_2{)}_h^{\mathsf{c}}{K}_h^{\mathsf{k}}{⟶}_{\beta }(e_1{)}_h^{\mathsf{c}}(\lambda a.(e_2{)}_h^{\mathsf{c}}(\lambda w.wa)),$$ which is precisely the first throw-frame translation. The next return contracts $a$, giving the second evaluation state. If its continuation value is $\mathsf{cont}(K^{\prime })$, the last return reduces as $$(\lambda w.w{v}_h^{\mathsf{v}})K_h^{\prime }{}^{\mathsf{k}}{⟶}_{\beta }{K}_h^{\prime }{}^{\mathsf{k}}{v}_h^{\mathsf{v}},$$ the translation of $K^{\prime }◃v$. This enumerates every rule of the machine. ◻

The requirement ${⟶}_{\beta \delta }^{+}$, rather than ${⟶}_{\beta \delta }^{\ast }$, is load bearing. A translation which represented some source steps by no target step would not by itself transfer termination of the deterministic machine.

Proof of Theorem 35.13 — Termination of the λ _ K machine

Proof. Suppose $s_0⟶s_1⟶\cdots$ were an infinite well-typed run. Preservation keeps one result type $R$. Choose fresh $h:R^{\mathsf{v}}\to \mathbf{0}$. Positive-step simulation concatenates to an infinite $\beta \delta$-reduction $$\Vert s_0{\Vert }_h{⟶}_{\beta \delta }^{+}\Vert s_1{\Vert }_h{⟶}_{\beta \delta }^{+}\cdots .$$ CPS typing gives a well-typed pure target term. This contradicts proposition 35.6. ◻

Proof of Corollary 35.14 — Relative consistency of the continuation calculus

Proof. If $⊢e:\mathbf{0}$, strong normalization and progress take $\bullet ▹e$ to a final state $\bullet ◃v$ with $v:\mathbf{0}$. The value grammar has no value of empty type, a contradiction. ◻

Classical proofs execute by changing the future

Under propositions as types, read $\mathbf{0}$ as falsehood $\mathrm{\perp }$, $A+B$ as disjunction $A\vee B$, and define $\mathrm{\neg }A:=A\to \mathrm{\perp }$. The relevant intuitionistic natural-deduction rules are

$\mathrm{\Gamma },A⊢\mathrm{\perp }$

$\mathrm{\Gamma }⊢\mathrm{\neg }A$

$\mathrm{\Gamma }⊢\mathrm{\neg }A$$\mathrm{\Gamma }⊢A$

$\mathrm{\Gamma }⊢\mathrm{\perp }$

$\mathrm{\Gamma }⊢A$

$\mathrm{\Gamma }⊢A\vee B$

$\mathrm{\Gamma }⊢B$

$\mathrm{\Gamma }⊢A\vee B$

Disjunction elimination is $$\frac{\mathrm{\Gamma }⊢A\vee B\mathrm{\Gamma },A⊢C\mathrm{\Gamma },B⊢C}{\mathrm{\Gamma }⊢C}(\vee E).$$ Empty elimination is $$\frac{\mathrm{\Gamma }⊢\mathrm{\perp }}{\mathrm{\Gamma }⊢C}(\mathrm{\perp }E),$$ and implication introduction and elimination are the inherited lambda and application rules. These rules do not include $$\frac{\mathrm{\Gamma }⊢\mathrm{\neg }\mathrm{\neg }A}{\mathrm{\Gamma }⊢A}(\mathsf{DNE}),\text{nor do they derive}\mathrm{\Gamma }⊢A\vee \mathrm{\neg }A$$ in general. A two-world Kripke frame $w_0\le w_1$, with $P$ forced only at $w_1$ and $\mathrm{\perp }$ forced nowhere, refutes $P\vee \mathrm{\neg }P$ at $w_0$: neither $P$ nor $P\to \mathrm{\perp }$ is forced there. Kripke soundness for exactly the displayed propositional rules is a rule induction (one case per rule): assumptions are monotone, implication introduction quantifies over extensions, implication elimination and the disjunction rules preserve forcing, and the empty-elimination case is vacuous. Soundness therefore rules out an intuitionistic derivation.

With the displayed $\mathrm{\perp }E$, the two classical extensions are equivalent. From $n:\mathrm{\neg }\mathrm{\neg }A$, case-analyze $A\vee \mathrm{\neg }A$; the left branch returns $A$, and the right branch derives $\mathrm{\perp }$ as $nq$ and eliminates it. Conversely, from $n:\mathrm{\neg }(A\vee \mathrm{\neg }A)$, the function $\lambda a.n(\mathsf{inl}a)$ proves $\mathrm{\neg }A$, so $n(\mathsf{inr}(\lambda a.n(\mathsf{inl}a)))$ proves $\mathrm{\perp }$; DNE at $A\vee \mathrm{\neg }A$ completes the other direction.

Now read $\mathsf{Cont}A$ as an operational program representation of $\mathrm{\neg }A$, not as its definitional equal. It is represented in CPS by $A^{\mathsf{v}}\to \mathbf{0}$, and throwing an $A$-value to such a continuation produces no local result. The control typing rules then give double-negation elimination directly.

Proof of Proposition 35.15 — Continuation-form double negation

Proof. The body has the complete derivation $$\frac{{\displaystyle \frac{\begin{array}{c}n:\mathsf{Cont}(\mathsf{Cont}A),k:\mathsf{Cont}A⊢k:\mathsf{Cont}A\\ n:\mathsf{Cont}(\mathsf{Cont}A),k:\mathsf{Cont}A⊢n:\mathsf{Cont}(\mathsf{Cont}A)\\ A\mathsf{type}\end{array}}{n:\mathsf{Cont}(\mathsf{Cont}A),k:\mathsf{Cont}A⊢\mathsf{throw}k\mathsf{to}n:A}}\mathrm{T}-\mathrm{Throw}}{n:\mathsf{Cont}(\mathsf{Cont}A)⊢\mathsf{letcc}k:\mathsf{Cont}A\mathsf{in}\mathsf{throw}k\mathsf{to}n:A}\mathrm{T}-\mathrm{Letcc}.$$ Lambda introduction derives $\mathsf{Cont}(\mathsf{Cont}A)\to A$. For the trace, capture substitutes $\mathsf{cont}(K)$; the two throw frames evaluate that value and $\mathsf{cont}(N)$, after which the last rule of (35.1) discards $K$ and restores $N$. ◻

Excluded middle uses the same mechanism twice. It first returns a continuation as evidence for the right summand. The only way to refute that evidence is to supply an $A$-value; doing so re-enters the original caller with the value in the left summand.

Proof of Proposition 35.16 — Continuation-form excluded middle with a change-of-mind trace

Proof. Put $B:=A+\mathsf{Cont}A$ and ${\mathrm{\Gamma }}_0:=k:\mathsf{Cont}B,q:\mathsf{Cont}A$. The complete derivation of the body is $$\frac{{\displaystyle \frac{{\displaystyle \frac{{\displaystyle \frac{\begin{array}{c}{\displaystyle \frac{{\mathrm{\Gamma }}_0⊢q:\mathsf{Cont}A}{{\mathrm{\Gamma }}_0⊢\mathsf{inr}q:B}}\mathrm{Inr}\\ {\mathrm{\Gamma }}_0⊢k:\mathsf{Cont}B\\ A\mathsf{type}\end{array}}{{\mathrm{\Gamma }}_0⊢\mathsf{throw}(\mathsf{inr}q)\mathsf{to}k:A}}\mathrm{T}-\mathrm{Throw}}{k:\mathsf{Cont}B⊢\mathsf{letcc}q:\mathsf{Cont}A\mathsf{in}\mathsf{throw}(\mathsf{inr}q)\mathsf{to}k:A}}\mathrm{T}-\mathrm{Letcc}}{k:\mathsf{Cont}B⊢\mathsf{inl}(\mathsf{letcc}q:\mathsf{Cont}A\mathsf{in}\mathsf{throw}(\mathsf{inr}q)\mathsf{to}k):B}}\mathrm{Inl}}{⊢{\mathsf{lem}}_A:B}\mathrm{T}-\mathrm{Letcc}.$$ The two variable premises are instances of Var; the last premise of T-Throw records its arbitrary result type $A$.

Operationally, the outer capture substitutes $\mathsf{cont}(K)$. The injection frame is pushed before the inner capture, so that capture yields $q=\mathsf{cont}(K^{\prime })$. Throwing its right injection to $\mathsf{cont}(K)$ discards $K^{\prime }$ and gives the first displayed return. The second calculation is the throw rule followed by the injection-frame return. Both traces include the same caller stack $K$; this is why the caller repeats its case analysis and can take the other branch. ◻

Proof of Corollary 35.17 — Double-negation elimination and excluded middle

Proof. For double-negation elimination use $$\lambda n:(A\to \mathbf{0})\to \mathbf{0}.\mathsf{letcc}k:\mathsf{Cont}A\mathsf{in}{\mathsf{abort}}_A(n(\lambda a:A.\mathsf{throw}a\mathsf{to}k)).$$ The inner lambda has type $A\to \mathbf{0}$ because its throw is assigned result type $\mathbf{0}$; hence $n$ produces $\mathbf{0}$, which ${\mathsf{abort}}_A$ eliminates. For excluded middle, case-analyze ${\mathsf{lem}}_A$. Map $\mathsf{inl}a$ to $\mathsf{inl}a$, and map $\mathsf{inr}q$, where $q:\mathsf{Cont}A$, to $\mathsf{inr}(\lambda a:A.\mathsf{throw}a\mathsf{to}q)$. The latter lambda again has type $A\to \mathbf{0}$. ◻

These propositions prove classical formulas by typed programs. They do not make double-negation elimination or excluded middle a definitional equality of the pure calculus. Their machine reductions capture and reinstate stacks; their CPS images are pure functions with additional beta reductions. Consistency follows from that translation, not from erasing the operational difference between classical and intuitionistic proof terms.

Delimiters, dependent projection, and let-polymorphism

The preceding continuations contain the whole stack. A reset instead marks a boundary, and ${\mathsf{shift}}_0$ or ${\mathsf{control}}_0$ captures only the evaluation context inside the nearest boundary. The four translations below are typable only under a specific polymorphic type-and-effect signature, and that signature is the content of this section. No theorem below identifies these calculi with ${\lambda }_{\mathsf{K}}$.

The section revisits deep resumption, handler clauses, and effect annotations in a deliberately different, unlabeled ordered-row signature. No theorem identifies its $\mathsf{do}$ form with the labeled operations of chapter 22, chapter 25. In the first of those chapters, an operation is ${\mathsf{op}}_{\ell }V(x.M)$, a handler is $\mathsf{handle}M\mathsf{with}H$, and the annotation $E_{\mathrm{out}}$ is a finite set. In chapter 25, the corresponding forms are $\mathsf{perform}\ell v$, $\mathsf{handle}e\mathsf{with}H$, and the unordered row $ϵ$. Here they are $\mathsf{do}v$, $\mathsf{handle}e\{x,r.e_h;y.e_r\}$, and the ordered row $\rho$. This last vocabulary is not inherited from either earlier chapter; it is the common core in which the four correspondences below are stated.

A delimited correspondence must record two facts that the whole-stack machine does not: which row entry marks the nearest delimiter, and whether invoking a captured continuation reinstalls that delimiter. The common core makes the row explicit before either control operator is introduced.

The common ordered-row core

The notation changes at this boundary. In chapter 4, rows are unique-label and unordered. In chapter 25, $\epsilon$ is a duplicate-label unordered row and $\mu$ a row variable. Here $\epsilon$ is one effect, $\rho$ is a duplicate-permitting ordered row, and $\mu$ below binds a recursive effect. The kind context $\mathrm{\Delta }$ and term context $\mathrm{\Gamma }$ are not the store typing $\mathrm{\Sigma }$ used in the state fragments of earlier chapters. These distinctions, rather than a shared row notation, are used by the translations. The arrow $\Rightarrow$ in ${\mathrm{\Delta }}_0.{\tau }_1\Rightarrow {\tau }_2$ is the single-effect signature separator, corresponding to the earlier $P⇝R$. It is unrelated to the stack/frame typing judgment $F:A\Rightarrow B$ used in the first two sections.

Deep handlers and ${\mathsf{shift}}_0$

For a concrete root calculation, temporarily add the pure arithmetic constants used in the stack machine and put $$E={\mathsf{add}}_2[],e=k40,e_r=x.$$ The S0-Shift contraction gives The substituted continuation reinstalls the reset around precisely the inner ${\mathsf{add}}_2[]$ context; the outer ${\mathsf{add}}_1[]$ frame is not captured.

Proof of Lemma 35.22 — Deep-bridge type substitution

Proof. Induct on types and rows. At a quantified effect, alpha-rename every binder away from $\alpha$ and $\mathrm{ftv}(\sigma )$ before applying the induction hypothesis beneath the binder. ◻

Proof of Lemma 35.23 — Deep-bridge value substitution

Proof. Induct on terms. Alpha-rename lambda, shift, handler, and return-clause binders away from $x$ and $\mathsf{FV}(v)$ before descent. For example, choose $k,h,y\notin \mathsf{FV}(\mathsf{DD}(v))\cup \{x\}$. The reverse operation clause gives $$\mathsf{DD}((\mathsf{do}w)[v/x])={\mathsf{shift}}_{0}k.\lambda h.h\mathsf{DD}(w[v/x])(\lambda y.kyh),$$ which is the induction hypothesis substituted into $\mathsf{DD}(\mathsf{do}w)$. The remaining nonhomomorphic clauses commute with capture-avoiding substitution in the same way. ◻

Proof of Lemma 35.24 — Deep-bridge context compatibility

Proof. Use simultaneous induction on the evaluation-context and freeness derivations. Application and lift use the common context constructors. A source delimiter becomes exactly one target delimiter, so its premise raises freeness from $n$ to $n+1$ in both calculi. ◻

Proof of Lemma 35.25 — Deep-bridge translation algebra

Proof. Combine lemma 35.22, lemma 35.23, lemma 35.24. ◻

The tempting reverse operation clause $${\mathsf{DD}}_{\mathrm{bad}}(\mathsf{do}v)={\mathsf{shift}}_{0}k.\lambda h.h\mathsf{DD}(v)k$$ does not type-check. The captured $k$ returns the handler-code function still expected outside the capture, whereas $h$ requires a resumption that returns the handler result after receiving that code. Closing over $h$ in $\lambda x.kxh$ rethreads the deep handler on every resumption.

Proof of Lemma 35.26 — Deep-bridge formation

Proof. Translate kinding and subtyping simultaneously; this fixes the scope of $\mathrm{\forall }{\mathrm{\Delta }}_0$ in the handler-code type. Use lemma 35.25 at every type-substitution boundary.

Formation. Induct simultaneously on kinding and subtyping. Variable, arrow, universal, empty-row, and row-cons formation are homomorphic, as are reflexive, arrow, universal, empty-row, and row-cons subtyping. The homomorphic cases follow their corresponding source constructors. For the translated-effect instance of Sub-Cons, the induction hypothesis on gives ; one target Sub-Cons step then derives . The $\mathsf{DD}$ direction is identical after replacing each translation symbol.

The two nonhomomorphic effect-formation cases do not follow from those homomorphic clauses. For the forward K-S0-to-K-DH case put $$T=\mathsf{DH}(\tau ),R=\mathsf{DH}(\rho ),C_a=a\stackrel{R}{\to }T,$$ $$Q_a=\mathrm{\forall }{\mathrm{\Delta }}_0.(C_a\stackrel{R}{\to }T),\eta =a::\mathsf{T}.Q_a\Rightarrow a.$$ The source premises translate to $\mathrm{\Delta },{\mathrm{\Delta }}_0⊢T::\mathsf{T}$ and $\mathrm{\Delta },{\mathrm{\Delta }}_0⊢R::\mathsf{R}$. Under fresh $a::\mathsf{T}$, write $\mathrm{\Xi }=\mathrm{\Delta },a::\mathsf{T},{\mathrm{\Delta }}_0$. Weakening derives $\mathrm{\Xi }⊢T::\mathsf{T}$ and $\mathrm{\Xi }⊢R::\mathsf{R}$. The complete target derivation is $$\frac{\mathrm{\Xi }⊢a::\mathsf{T}\mathrm{\Xi }⊢R::\mathsf{R}\mathrm{\Xi }⊢T::\mathsf{T}}{\mathrm{\Xi }⊢C_a::\mathsf{T}}K-Arr.$$ $$\frac{\mathrm{\Xi }⊢C_a::\mathsf{T}\mathrm{\Xi }⊢R::\mathsf{R}\mathrm{\Xi }⊢T::\mathsf{T}}{\mathrm{\Xi }⊢C_a\stackrel{R}{\to }T::\mathsf{T}}K-Arr.$$ $$\frac{\mathrm{\Delta },a::\mathsf{T},{\mathrm{\Delta }}_0⊢C_a\stackrel{R}{\to }T::\mathsf{T}}{\mathrm{\Delta },a::\mathsf{T}⊢Q_a::\mathsf{T}}K-Al{l}^{{\mathrm{\Delta }}_0},$$ $$\frac{\mathrm{\Delta },a::\mathsf{T}⊢Q_a::\mathsf{T}\mathrm{\Delta },a::\mathsf{T}⊢a::\mathsf{T}}{\mathrm{\Delta }⊢\eta ::\mathsf{E}}K-DH.$$ $$\frac{\mathrm{\Delta }⊢\eta ::\mathsf{E}\mathrm{\Delta }⊢\iota ::\mathsf{R}}{\mathrm{\Delta }⊢\eta \cdot \iota ::\mathsf{R}}K-Cons.$$ Here $K-Al{l}^{{\mathrm{\Delta }}_0}$ denotes one displayed K-All step for every binder of ${\mathrm{\Delta }}_0$, retaining each declared kind $\mathsf{T}$, $\mathsf{E}$, or $\mathsf{R}$. Thus the universal really scopes the entire function $C_a\stackrel{R}{\to }T$, and the result is both a deep effect and, after row cons, a row.

For K-DH-to-K-S0, put $$D_{a,b}={\tau }_2\stackrel{b}{\to }a,G_{a,b}=D_{a,b}\stackrel{b}{\to }a,$$ $$H_{a,b}=\mathrm{\forall }{\mathrm{\Delta }}_0.({\tau }_1\stackrel{\iota }{\to }{G}_{a,b}),\theta =a::\mathsf{T},b::\mathsf{R}.(H_{a,b}\stackrel{b}{\to }a)/b.$$ The translated K-DH premises give $\mathrm{\Delta },{\mathrm{\Delta }}_0⊢{\tau }_i::\mathsf{T}$ for $i=1,2$. Under fresh $a::\mathsf{T},b::\mathsf{R}$, write ${\mathrm{\Omega }}_0=\mathrm{\Delta },a::\mathsf{T},b::\mathsf{R}$ and $\mathrm{\Omega }={\mathrm{\Omega }}_0,{\mathrm{\Delta }}_0$. Weakening derives $\mathrm{\Omega }⊢{\tau }_i::\mathsf{T}$ for $i=1,2$. The three K-Arr derivations are $$\frac{\mathrm{\Omega }⊢{\tau }_2::\mathsf{T}\mathrm{\Omega }⊢b::\mathsf{R}\mathrm{\Omega }⊢a::\mathsf{T}}{\mathrm{\Omega }⊢D_{a,b}::\mathsf{T}}K-Arr.$$ $$\frac{\mathrm{\Omega }⊢D_{a,b}::\mathsf{T}\mathrm{\Omega }⊢b::\mathsf{R}\mathrm{\Omega }⊢a::\mathsf{T}}{\mathrm{\Omega }⊢G_{a,b}::\mathsf{T}}K-Arr.$$ $$\frac{\mathrm{\Omega }⊢{\tau }_1::\mathsf{T}\mathrm{\Omega }⊢\iota ::\mathsf{R}\mathrm{\Omega }⊢G_{a,b}::\mathsf{T}}{\mathrm{\Omega }⊢{\tau }_1\stackrel{\iota }{\to }{G}_{a,b}::\mathsf{T}}K-Arr.$$ The remaining formation tree is $$\frac{\mathrm{\Omega }⊢{\tau }_1\stackrel{\iota }{\to }{G}_{a,b}::\mathsf{T}}{{\mathrm{\Omega }}_0⊢H_{a,b}::\mathsf{T}}K-Al{l}^{{\mathrm{\Delta }}_0},$$ $$\frac{{\mathrm{\Omega }}_0⊢H_{a,b}::\mathsf{T}{\mathrm{\Omega }}_0⊢b::\mathsf{R}{\mathrm{\Omega }}_0⊢a::\mathsf{T}}{{\mathrm{\Omega }}_0⊢H_{a,b}\stackrel{b}{\to }a::\mathsf{T}}K-Arr,$$ $$\frac{{\mathrm{\Omega }}_0⊢H_{a,b}\stackrel{b}{\to }a::\mathsf{T}{\mathrm{\Omega }}_0⊢b::\mathsf{R}}{\mathrm{\Delta }⊢\theta ::\mathsf{E}}K-S0.$$ Consequently K-Cons also gives $\mathrm{\Delta }⊢\theta \cdot \iota ::\mathsf{R}$. This displays both the polymorphic handler-code kind and the effect/row result required by the reverse translation. ◻

Proof of Lemma 35.27 — shift_0-to-deep type preservation

Proof. Induct on the source typing derivation. Rule P-Gen retains the empty row; P-Inst uses type substitution from lemma 35.25; and P-Sub uses lemma 35.26. Variable, lambda, application, and lift rebuild their corresponding target rules. It remains to check the two nonhomomorphic cases.

For a source effect ${\mathrm{\Delta }}_0.\tau /\rho$, put $$T=\mathsf{DH}(\tau ),R=\mathsf{DH}(\rho ),C_X=X\stackrel{R}{\to }T,$$ $$Q_X=\mathrm{\forall }{\mathrm{\Delta }}_0.(C_X\stackrel{R}{\to }T),\eta =a::\mathsf{T}.Q_a\Rightarrow a.$$

For the control-to-handler implication, the two nonhomomorphic typing cases use $$U=\mathsf{DH}({\tau }^{\prime }),R_0=\mathsf{DH}({\rho }_0).$$ For S0-Shift, the induction hypothesis and the translated premise give Alpha-rename every binder of ${\mathrm{\Delta }}_0$ away from $\mathsf{FV}(\mathrm{\Gamma })$; hence each use of P-Gen satisfies its freshness side condition. Apply P-Sub to the evaluation row, then P-Lam, then P-Gen once for each binder in ${\mathrm{\Delta }}_0$: Rule DH-Do uses the explicit instantiation $a\mapsto U$ and derives $$\mathsf{do}(\lambda k.\mathsf{DH}(e)):U/\eta .$$ Finally, Sub-Cons lifts beneath $\eta$. Rule P-Sub then gives $U/\eta \cdot R_0$, the translated conclusion.

For S0-Reset, let $\delta ::{\mathrm{\Delta }}_0$ be its displayed instantiation. The induction hypotheses type the handled computation at $U/\eta \cdot \delta R$ and the return clause at $\delta T/\delta R$. In the operation clause of DH-Handle, $$f:Q_a,r:a\stackrel{\delta R}{\to }\delta T.$$ Rule P-Inst specializes every binder of $f$ by $\delta$, so $$f:(a\stackrel{\delta R}{\to }\delta T)\stackrel{\delta R}{\to }\delta T.$$ Lift the two pure variable judgments to $\delta R$ by P-Sub and apply P-App; this derives $fr:\delta T/\delta R$. Thus DH-Handle has all three premises and returns $\delta T/\delta R$.

These calculations establish the implication. ◻

Proof of Lemma 35.28 — Deep-to- shift_0 type preservation

Proof. Induct on the source typing derivation. Common rules are homomorphic, with substitution and subtyping supplied by lemma 35.25, lemma 35.26. It remains to check the operation and handler rules.

For a source effect ${\mathrm{\Delta }}_0.{\tau }_1\Rightarrow {\tau }_2$ with trailing row $\iota$, put $$D_{a,b}={\tau }_2\stackrel{b}{\to }a,G_{a,b}=D_{a,b}\stackrel{b}{\to }a,$$ $$H_{a,b}=\mathrm{\forall }{\mathrm{\Delta }}_0.({\tau }_1\stackrel{\iota }{\to }{G}_{a,b}),\theta =a::\mathsf{T},b::\mathsf{R}.(H_{a,b}\stackrel{b}{\to }a)/b.$$ The undecorated arrow in definition 35.21 is the $\iota$-arrow in this definition of $H_{a,b}$. In a translated DH-Do premise, let ${\delta }_0::{\mathrm{\Delta }}_0$ be the operation’s instantiation. Under fresh $a,b$, P-Inst gives $$h:{\delta }_0{\tau }_1\to ({\delta }_0{\tau }_2\stackrel{b}{\to }a)\stackrel{b}{\to }a,k:{\delta }_0{\tau }_2\stackrel{b}{\to }(H_{a,b}\stackrel{b}{\to }a).$$ After lifting pure variables to row $b$, repeated P-App and P-Lam derive, in order, $$kxh:a/b,\lambda x.kxh:{\delta }_0{\tau }_2\stackrel{b}{\to }a/\iota ,h\mathsf{DD}(v)(\lambda x.kxh):a/b,$$ and hence $$\lambda h.h\mathsf{DD}(v)(\lambda x.kxh):H_{a,b}\stackrel{b}{\to }a/\iota .$$ Rule S0-Shift, with its binders instantiated by the fresh $a,b$, uses and concludes ${\delta }_0{\tau }_2/\theta \cdot \iota$.

Finally suppose the source DH-Handle has result ${\tau }_r/\rho$, and put $$H_r=\mathrm{\forall }{\mathrm{\Delta }}_0.{\tau }_1\to ({\tau }_2\stackrel{\rho }{\to }{\tau }_r)\stackrel{\rho }{\to }{\tau }_r.$$ The translated reset uses the explicit substitution $[a\mapsto {\tau }_r,b\mapsto \rho ]$. Its computation premise has type $\tau /\theta \cdot \rho$, while $x.\lambda h.\mathsf{DD}(e_r)$ has type $H_r\stackrel{\rho }{\to }{\tau }_r/\rho$; hence S0-Reset yields $H_r\stackrel{\rho }{\to }{\tau }_r/\rho$. Generalizing the translated operation clause over ${\mathrm{\Delta }}_0$ gives $\lambda x.\lambda r.\mathsf{DD}(e_h):H_r/\iota$. One final P-App, after pure-row widening, gives ${\tau }_r/\rho$. This also explains why the captured resumption is $\lambda x.kxh$, not merely $k$. ◻

Proof of Lemma 35.29 — Deep-bridge root simulation

Proof. For semantic preservation, write $$D=\{f,r.fr;y.\mathsf{DH}(e_r)\},v_c=\lambda z.\mathsf{handle}\mathsf{DH}(E)[z]D.$$ The translated ${\mathsf{shift}}_0$ root is the complete calculation where the last equality is lemma 35.25. Every step is an ordinary evaluation step.

In the reverse direction put $$H=\lambda x.\lambda r.\mathsf{DD}(e_h),R_y=\lambda h.\mathsf{DD}(e_r),Q[z]=⟨\mathsf{DD}(E)[z]\mid y.R_y⟩.$$ Then the translated deep-operation root is The contraction of $(\lambda w.Q[w])z$ occurs beneath $\lambda z$, so ordinary evaluation-context reduction is insufficient; this is exactly the use of arbitrary-context ${⟶}_i$. Handler/reset return roots contract directly and then use substitution. The context and freeness parts of lemma 35.25 lift these root calculations, proving the two stated positive closures. ◻

Proof of Theorem 35.30 — Typed deep/ shift_0 correspondence

Proof. The two typing implications are lemma 35.27, lemma 35.28; the two positive simulations are lemma 35.29. ◻

A fully typed deep root.

Fix $A::\mathsf{T}$ and $a:A$, and put $${\epsilon }_s=\varnothing .A/\iota ,{\epsilon }_h=b::\mathsf{T}.((b\stackrel{\iota }{\to }A)\stackrel{\iota }{\to }A)\Rightarrow b.$$ The empty quantifier in ${\epsilon }_s$ disappears in ${\epsilon }_h$. The complete source derivation for $d_A=⟨{\mathsf{shift}}_{0}k.ka\mid x.x⟩$ is

$A::\mathsf{T}⊢\varnothing ::\varnothing$

$a:A,k:A\stackrel{\iota }{\to }A⊢k:(A\stackrel{\iota }{\to }A)/\iota$

$a:A,k:A\stackrel{\iota }{\to }A⊢a:A/\iota$

$a:A,k:A\stackrel{\iota }{\to }A⊢ka:A/\iota$

$A::\mathsf{T}$${\epsilon }_s\cdot \iota ::\mathsf{R}$

$a:A⊢{\mathsf{shift}}_{0}k.ka:A/{\epsilon }_s\cdot \iota$

$a:A,x:A⊢x:A/\iota$

$a:A⊢d_A:A/\iota$

Put $D_{\mathsf{h}}=\{f,r.fr;x.x\}$. Its translation is $$h_A=\mathsf{handle}\mathsf{do}(\lambda k.ka)D_{\mathsf{h}}.$$ No typing premise is implicit: P-App followed by P-Lam gives $$a:A⊢\lambda k.ka:(A\stackrel{\iota }{\to }A)\stackrel{\iota }{\to }A/\iota ,$$ and DH-Do, instantiated by $b\mapsto A$, gives $a:A⊢\mathsf{do}(\lambda k.ka):A/{\epsilon }_h$. For the handler’s operation premise, under fresh $b::\mathsf{T}$, $$f:(b\stackrel{\iota }{\to }A)\stackrel{\iota }{\to }A,r:b\stackrel{\iota }{\to }A⊢fr:A/\iota$$ by two P-Var leaves and P-App; its return premise is $x:A⊢x:A/\iota$ by P-Var. Rule DH-Handle therefore derives $a:A⊢h_A:A/\iota$. The typed source root and its target simulation are

Shallow handlers and ${\mathsf{control}}_0$

Deep resumption reinstalls its delimiter. Shallow resumption does not. The type of a resumed computation can therefore expose the same leading effect again, which forces recursion at the level of effect specifications.

Proof of Lemma 35.33 — Shallow-bridge type substitution

Proof. Induct on types and rows. The recursive-effect case uses capture-avoiding unfolding ${\delta }^{\epsilon }=\delta [\alpha \mapsto \epsilon ]$, after renaming every bound variable away from the substitution support. ◻

Proof of Lemma 35.34 — Shallow-bridge value substitution

Proof. Induct on terms, alpha-renaming each term binder away from $x$ and $\mathsf{FV}(v)$ before descent. Choose $k,h\notin \mathsf{FV}(\mathsf{SD}(v))\cup \{x\}$. Then $$\mathsf{SD}((\mathsf{do}w)[v/x])={\mathsf{control}}_{0}k.\lambda h.h\mathsf{SD}(w[v/x])k,$$ and the induction hypothesis makes this exactly $\mathsf{SD}(\mathsf{do}w)[\mathsf{SD}(v)/x]$. The shallow handler clause follows by the same capture-avoiding calculation. ◻

Proof of Lemma 35.35 — Shallow-bridge context compatibility

Proof. Use simultaneous induction on the evaluation-context and freeness derivations. A shallow handler and a ${\mathsf{control}}_0$ reset each add exactly one delimiter; their translated contexts therefore have the same freeness index. ◻

Proof of Lemma 35.36 — Shallow-bridge translation algebra

Proof. Combine lemma 35.33, lemma 35.34, lemma 35.35. ◻

For a shallow handler, the corresponding plain-$k$ clause is well typed: $$\mathsf{SD}(\mathsf{do}v)={\mathsf{control}}_{0}k.\lambda h.h\mathsf{SD}(v)k.$$ Unlike the failed deep attempt above, invoking $k$ must not reinstall the handler. This contrast determines the operation clause rather than merely confirming it after translation.

Proof of Lemma 35.37 — Forward shallow-bridge preservation

Proof. Induct simultaneously on forward formation, subtyping, and typing, using the substitution component of lemma 35.36 at each binding boundary.

Formation. Variable, arrow, universal, empty-row, and row-cons formation and all common-core typing cases are homomorphic. We derive the recursive effect-formation cases and the novel typing cases here, without appealing to another correspondence theorem. In the control-to-handler direction use $\mathsf{SH}(-)$. For the source types ${\tau }_1,{\tau }_2$ and answer row $\rho$, put $$T_1:=\mathsf{SH}({\tau }_1),T_2:=\mathsf{SH}({\tau }_2),R:=\mathsf{SH}(\rho ).$$ Then write $$\eta =\mu a.b::\mathsf{T}.Q_b\Rightarrow b,Q_b=\mathrm{\forall }{\mathrm{\Delta }}_0.((b\stackrel{a\cdot R}{\to }{T}_1)\stackrel{R}{\to }{T}_2).$$ For the K-C0-to-K-SH formation case, write $\mathrm{\Xi }=\mathrm{\Delta },a::\mathsf{E},b::\mathsf{T},{\mathrm{\Delta }}_0$. The translated source premises provide $\mathrm{\Xi }⊢T_i::\mathsf{T}$ and $\mathrm{\Xi }⊢R::\mathsf{R}$. The target derivation begins $$\frac{\mathrm{\Xi }⊢a::\mathsf{E}\mathrm{\Xi }⊢R::\mathsf{R}}{\mathrm{\Xi }⊢a\cdot R::\mathsf{R}}K-Cons,$$ $$\frac{\mathrm{\Xi }⊢b::\mathsf{T}\mathrm{\Xi }⊢a\cdot R::\mathsf{R}\mathrm{\Xi }⊢T_1::\mathsf{T}}{\mathrm{\Xi }⊢b\stackrel{a\cdot R}{\to }{T}_1::\mathsf{T}}K-Arr,$$ $$\frac{\mathrm{\Xi }⊢b\stackrel{a\cdot R}{\to }{T}_1::\mathsf{T}\mathrm{\Xi }⊢R::\mathsf{R}\mathrm{\Xi }⊢T_2::\mathsf{T}}{\mathrm{\Xi }⊢(b\stackrel{a\cdot R}{\to }{T}_1)\stackrel{R}{\to }{T}_2::\mathsf{T}}K-Arr.$$ Iterated universal formation and recursive shallow-effect formation are $$\frac{\mathrm{\Xi }⊢(b\stackrel{a\cdot R}{\to }{T}_1)\stackrel{R}{\to }{T}_2::\mathsf{T}}{\mathrm{\Delta },a::\mathsf{E},b::\mathsf{T}⊢Q_b::\mathsf{T}}K-Al{l}^{{\mathrm{\Delta }}_0},$$ $$\frac{\mathrm{\Delta },a::\mathsf{E},b::\mathsf{T}⊢Q_b::\mathsf{T}\mathrm{\Delta },a::\mathsf{E},b::\mathsf{T}⊢b::\mathsf{T}}{\mathrm{\Delta }⊢\eta ::\mathsf{E}}K-SH.$$ Thus K-Cons gives $\mathrm{\Delta }⊢\eta \cdot \iota ::\mathsf{R}$.

Control-to-handler typing.

Unfolding the recursive effect is kind-preserving substitution. Put $${\bar{T}}_i=T_i[\eta /a],\bar{R}=R[\eta /a],{\bar{Q}}_b=Q_b[\eta /a].$$ The preceding derivation therefore gives $$\mathrm{\Delta },b::\mathsf{T}⊢{\bar{Q}}_b::\mathsf{T},\mathrm{\Delta },{\mathrm{\Delta }}_0⊢\eta \cdot \bar{R}::\mathsf{R},$$ where, in full, $${\bar{Q}}_b=\mathrm{\forall }{\mathrm{\Delta }}_0.((b\stackrel{\eta \cdot \bar{R}}{\to }{\bar{T}}_1)\stackrel{\bar{R}}{\to }{\bar{T}}_2).$$ In the typing derivation below we drop overlines on $T_i,R$, but retain $\bar{Q}$. Thus a translated C0-Control premise, for result type $U$, is Rule P-Sub widens the body’s row to $R$; P-Lam and one P-Gen for each member of ${\mathrm{\Delta }}_0$ then give the following judgment. Alpha-rename the binders of ${\mathrm{\Delta }}_0$ away from $\mathsf{FV}(\mathrm{\Gamma })$ first, so every generalization satisfies the freshness premise: $$\mathrm{\Gamma }⊢\lambda k.\mathsf{SH}(e):{\bar{Q}}_U/\iota .$$ Rule SH-Do unfolds $\eta$, instantiates $b\mapsto U$, and gives result $U/\eta$. The final P-Sub uses under Sub-Cons, yielding $U/\eta \cdot R_0$.

At a translated C0-Reset, let $\delta ::{\mathrm{\Delta }}_0$ be the source instantiation. The operation arm of SH-Handle has $$f:{\bar{Q}}_b,r:b\stackrel{\eta \cdot \delta R}{\to }\delta T_1.$$ Instantiating $f$ by $\delta$ gives $$f:(b\stackrel{\eta \cdot \delta R}{\to }\delta T_1)\stackrel{\delta R}{\to }\delta T_2.$$ After pure-row widening, P-App derives $fr:\delta T_2/\delta R$. Together with the two induction hypotheses this is exactly SH-Handle; no deep handler is silently used. ◻

Proof of Lemma 35.38 — Reverse shallow-bridge preservation

Proof. Induct simultaneously on reverse formation, subtyping, and typing. Common constructors are homomorphic, and substitution uses lemma 35.36. The recursive effect, operation, and handler cases are the following explicit derivations.

For K-SH-to-K-C0, first keep the recursive variable abstract: $$F_{b_1,g}^a=\mathsf{SD}({\tau }_2)\stackrel{a\cdot g}{\to }{b}_1,G_{b_1,b_2,g}^a=F_{b_1,g}^a\stackrel{g}{\to }{b}_2,$$ $$H(a,b_1,b_2,g)=\mathrm{\forall }{\mathrm{\Delta }}_0.(\mathsf{SD}({\tau }_1)\stackrel{\iota }{\to }{G}_{b_1,b_2,g}^a),$$ $$\theta =\mu a.b_1::\mathsf{T},b_2::\mathsf{T},g::\mathsf{R}.b_1\Rightarrow (H(a,b_1,b_2,g)\stackrel{g}{\to }{b}_2)/g.$$ Put $\mathrm{\Omega }=\mathrm{\Delta },a::\mathsf{E},b_1::\mathsf{T},b_2::\mathsf{T},g::\mathsf{R},{\mathrm{\Delta }}_0$. The translated K-SH premises and the fresh-variable rules yield the following derivation: $$\frac{\mathrm{\Omega }⊢a::\mathsf{E}\mathrm{\Omega }⊢g::\mathsf{R}}{\mathrm{\Omega }⊢a\cdot g::\mathsf{R}}K-Cons.$$ $$\frac{\mathrm{\Omega }⊢{\tau }_2::\mathsf{T}\mathrm{\Omega }⊢a\cdot g::\mathsf{R}\mathrm{\Omega }⊢b_1::\mathsf{T}}{\mathrm{\Omega }⊢F_{b_1,g}^a::\mathsf{T}}K-Arr.$$ $$\frac{\mathrm{\Omega }⊢F_{b_1,g}^a::\mathsf{T}\mathrm{\Omega }⊢g::\mathsf{R}\mathrm{\Omega }⊢b_2::\mathsf{T}}{\mathrm{\Omega }⊢G_{b_1,b_2,g}^a::\mathsf{T}}K-Arr,$$ $$\frac{\mathrm{\Omega }⊢{\tau }_1::\mathsf{T}\mathrm{\Omega }⊢\iota ::\mathsf{R}\mathrm{\Omega }⊢G_{b_1,b_2,g}^a::\mathsf{T}}{\mathrm{\Omega }⊢{\tau }_1\stackrel{\iota }{\to }{G}_{b_1,b_2,g}^a::\mathsf{T}}K-Arr.$$ Writing ${\mathrm{\Omega }}_0=\mathrm{\Delta },a::\mathsf{E},b_1::\mathsf{T},b_2::\mathsf{T},g::\mathsf{R}$, the final formation steps are $$\frac{\mathrm{\Omega }⊢{\tau }_1\stackrel{\iota }{\to }{G}_{b_1,b_2,g}^a::\mathsf{T}}{{\mathrm{\Omega }}_0⊢H(a,b_1,b_2,g)::\mathsf{T}}K-Al{l}^{{\mathrm{\Delta }}_0},$$ $$\frac{{\mathrm{\Omega }}_0⊢H(a,b_1,b_2,g)::\mathsf{T}{\mathrm{\Omega }}_0⊢g::\mathsf{R}{\mathrm{\Omega }}_0⊢b_2::\mathsf{T}}{{\mathrm{\Omega }}_0⊢H(a,b_1,b_2,g)\stackrel{g}{\to }{b}_2::\mathsf{T}}K-Arr,$$ $$\frac{{\mathrm{\Omega }}_0⊢b_1::\mathsf{T}{\mathrm{\Omega }}_0⊢H(a,b_1,b_2,g)\stackrel{g}{\to }{b}_2::\mathsf{T}{\mathrm{\Omega }}_0⊢g::\mathsf{R}}{\mathrm{\Delta }⊢\theta ::\mathsf{E}}K-C0.$$ In particular, K-Cons gives $\mathrm{\Delta }⊢\theta \cdot \iota ::\mathsf{R}$. Unfolding is again kind-preserving substitution. With $${\bar{\tau }}_i={\tau }_i[\theta /a],{\bar{H}}_{b_1,b_2,g}=H(a,b_1,b_2,g)[\theta /a],$$ we have $${\bar{H}}_{b_1,b_2,g}=\mathrm{\forall }{\mathrm{\Delta }}_0.({\bar{\tau }}_1\stackrel{\iota }{\to }(({\bar{\tau }}_2\stackrel{\theta \cdot g}{\to }{b}_1)\stackrel{g}{\to }{b}_2)),$$ $$\mathrm{\Delta },b_1::\mathsf{T},b_2::\mathsf{T},g::\mathsf{R}⊢{\bar{H}}_{b_1,b_2,g}::\mathsf{T}.$$ $$\mathrm{\Delta },b_1::\mathsf{T},b_2::\mathsf{T},g::\mathsf{R}⊢\theta \cdot g::\mathsf{R}.$$ Below we omit overlines on ${\tau }_i$, but retain $\bar{H}$. For a translated SH-Do, specialize $h:{\bar{H}}_{b_1,b_2,g}$ by the source substitution ${\delta }_0::{\mathrm{\Delta }}_0$. With $$k:{\delta }_0{\tau }_2\stackrel{\theta \cdot g}{\to }{b}_1$$ the two applications derive $$h\mathsf{SD}(v)k:b_2/g,\lambda h.h\mathsf{SD}(v)k:{\bar{H}}_{b_1,b_2,g}\stackrel{g}{\to }{b}_2/\iota .$$ Rule C0-Control now instantiates its recursive effect by fresh $b_1,b_2,g$, uses , and concludes ${\delta }_0{\tau }_2/\theta \cdot \iota$.

For a source shallow handler with result ${\tau }_r/\rho$, set $$H_r=\mathrm{\forall }{\mathrm{\Delta }}_0.{\tau }_1\to ({\tau }_2\stackrel{\theta \cdot \rho }{\to }\tau )\stackrel{\rho }{\to }{\tau }_r.$$ The translated reset explicitly instantiates $[b_1\mapsto \tau ,b_2\mapsto {\tau }_r,g\mapsto \rho ]$. Its body has type $\tau /\theta \cdot \rho$, and its return clause $x.\lambda h.\mathsf{SD}(e_r)$ has type $H_r\stackrel{\rho }{\to }{\tau }_r/\rho$. Rule C0-Reset therefore returns a function of that type. Generalizing $\lambda x.\lambda r.\mathsf{SD}(e_h)$ over ${\mathrm{\Delta }}_0$ gives $H_r/\iota$; one row-widened P-App gives ${\tau }_r/\rho$. Thus $b_1$ is the type expected by the captured continuation, $b_2$ is the handler result, and $g$ is the residual row, with every instantiation exposed. ◻

Proof of Lemma 35.39 — Shallow-bridge root simulation

Proof. For the control-to-handler root, put $$D=\{f,r.fr;y.\mathsf{SH}(e_r)\},v_c=\lambda z.\mathsf{SH}(E)[z].$$ Then The shallow resumption contains neither handler nor reset.

For the reverse root, put $$H=\lambda x.\lambda r.\mathsf{SD}(e_h),R_y=\lambda h.\mathsf{SD}(e_r).$$ The whole calculation is Every administrative contraction is in evaluation position. Return roots translate to return roots, while common beta and lift roots are homomorphic. The substitution, context, and freeness parts of lemma 35.36 lift the calculations and complete both positive simulations. For a source context step $E[e]⟶E[e^{\prime }]$, the plugging equation rewrites $X(E[e])$ to $X(E)[X(e)]$; target compatible closure lifts the root calculation, and plugging rewrites its endpoint to $X(E[e^{\prime }])$. ◻

Proof of Theorem 35.40 — Typed shallow/ control_0 correspondence

Proof. The two typing implications are lemma 35.37, lemma 35.38; the two positive simulations are lemma 35.39. ◻

A fully typed shallow root.

Again fix $A::\mathsf{T}$ and $a:A$, and define $${\epsilon }_c=\mu q.\varnothing .A\Rightarrow A/\iota ,{\epsilon }_h=\mu q.b::\mathsf{T}.((b\stackrel{q\cdot \iota }{\to }A)\stackrel{\iota }{\to }A)\Rightarrow b.$$ For $c_A=⟨{\mathsf{control}}_{0}k.a\mid x.x⟩$, the capture premise and conclusion are

${\epsilon }_c=\mu q.\varnothing .A\Rightarrow A/\iota$

$a:A,k:A\stackrel{{\epsilon }_c\cdot \iota }{\to }A⊢a:A/\iota$

$A::\mathsf{T}$${\epsilon }_c\cdot \iota ::\mathsf{R}$

$a:A⊢{\mathsf{control}}_{0}k.a:A/{\epsilon }_c\cdot \iota$

Together with $A::\mathsf{T}⊢\varnothing ::\varnothing$ and $a:A,x:A⊢x:A/\iota$, rule C0-Reset gives $a:A⊢c_A:A/\iota$. This lists every premise of the two novel source rules.

The translated operation is $\mathsf{do}(\lambda k.a)$. Rule P-Var types the body $a$, and P-Lam abstracts $k$, giving $$a:A⊢\lambda k.a:(A\stackrel{{\epsilon }_h\cdot \iota }{\to }A)\stackrel{\iota }{\to }A/\iota .$$ Rule SH-Do unfolds ${\epsilon }_h$ and instantiates $b\mapsto A$, deriving $a:A⊢\mathsf{do}(\lambda k.a):A/{\epsilon }_h$. In the operation arm, under fresh $b::\mathsf{T}$, $$f:(b\stackrel{{\epsilon }_h\cdot \iota }{\to }A)\stackrel{\iota }{\to }A,r:b\stackrel{{\epsilon }_h\cdot \iota }{\to }A⊢fr:A/\iota$$ by two P-Var leaves and P-App; the return arm is $x:A⊢x:A/\iota$. Hence SH-Handle completely derives $$a:A⊢\mathsf{handle}\mathsf{do}(\lambda k.a)\{f,r.fr;x.x\}:A/\iota .$$ The source and target roots expose the shallow resumption: The target resumption is $\lambda z.z$, with no reinstalled handler.

The difference becomes observable when resumption itself reaches another operation. For this calculation only, conservatively extend the shared PPS core with the pure unit type $\mathsf{Unit}$, its value $()$, and typed lambda annotations; none of the correspondence theorems depends on this example. At the respective deep and shallow signatures for the unit operation $\mathsf{Unit}\Rightarrow \mathsf{Unit}$, let $$P:=\mathsf{handle}((\lambda u:\mathsf{Unit}.\mathsf{do}())(\mathsf{do}()))\{x,r.r();y.y\}.$$ For a deep handler, handling the first operation passes the reinstalled continuation $$\lambda z.\mathsf{handle}((\lambda u:\mathsf{Unit}.\mathsf{do}())z)\{x,r.r();y.y\}$$ to the clause. Invoking it puts the second $\mathsf{do}$ beneath the same handler, so the second operation is handled and the computation returns $()$. For a shallow handler, the corresponding resumption is only $\lambda z.(\lambda u:\mathsf{Unit}.\mathsf{do}())z$. Invoking it reduces to the unhandled operation $\mathsf{do}()$. Thus reinstalling the delimiter is not administrative syntax: it determines whether a later operation is caught.

The result is signature-specific. It requires four things at once: ordered rows; quantification over all three kinds; polymorphic deep effects; and recursive shallow effects. The four proved translations are Each arrow states type preservation and the simulation relation printed in the corresponding theorem. No inverse, retraction, reflection, or full- abstraction theorem is proved. Swapping either pairing, or erasing the quantifiers, changes the resumption type and invalidates the typing proof.

Dependent elimination: a separate failure boundary

This boundary calculation uses a strong existential, which packages a witness together with a certificate whose type may mention that very witness: from $p:\mathrm{\exists }x:\mathsf{Nat}.A$, its projections have types $\mathsf{wit}p:\mathsf{Nat}$ and $\mathsf{prf}p:A[\mathsf{wit}p/x]$.

Simple types do not let a result type inspect the particular value returned by a computation. A dependent pair does. Control can make the same proof return different witnesses in different continuations, so unrestricted dependent elimination can confuse a witness with its certificate.

The counterexample in this section is not a run of the call-by-value machine ${\lambda }_{\mathsf{K}}$. It belongs to a separate hypothetical call-by-name calculus with a commuting rule for first projection. Its purpose is to isolate exactly which extra dependent rule is dangerous.

Consider $$p_0:={\mathsf{callcc}}_k(0,{\mathsf{throw}}_k(1,\mathsf{refl})):\mathrm{\exists }x:\mathsf{Nat}.x=1.$$ Every node of its typing is visible in the following chain. Under $k:\mathrm{\neg }(\mathrm{\exists }x:\mathsf{Nat}.x=1)$, $$1:\mathsf{Nat},\mathsf{refl}:1=1,(1,\mathsf{refl}):\mathrm{\exists }x:\mathsf{Nat}.x=1.$$ Rule Dep-Throw-P assigns ${\mathsf{throw}}_k(1,\mathsf{refl})$ the arbitrary local result type $0=1$. With $0:\mathsf{Nat}$, rule Dep-Pair therefore gives $$(0,{\mathsf{throw}}_k(1,\mathsf{refl})):\mathrm{\exists }x:\mathsf{Nat}.x=1,$$ and Dep-Callcc-P discharges $k$, yielding the type in (35.2). The commuting rule and the explicit compatibility clause under $\mathsf{callcc}$ give the call-by-name reduction The projection typing and this conversion yield $$\mathsf{prf}{p}_0:\mathsf{wit}{p}_0=1,\mathsf{refl}:\mathsf{wit}{p}_0=0.$$ Substitution of equals produces a proof of $1=0$. The same occurrence $p_0$ supplied the witness in one continuation and the certificate in another. This collapses two distinct closed numerals. The fragment has no rule from $1=0$ to $\mathrm{\perp }$, so the precise conclusion is failure of numerical canonicity, not a separately derived proof of falsehood.

Proof of Proposition 35.42 — The dependent-elimination boundary

Proof. Let $B(x):=x=0$. The first displayed proof has type $\mathsf{wit}{p}_0=1$, while conversion along $\mathsf{wit}{p}_0{⟼}^{\ast }0$ types $\mathsf{refl}:\mathsf{wit}{p}_0=0=B(\mathsf{wit}{p}_0)$. Rule Dep-Subst therefore derives $$\mathsf{subst}(\mathsf{prf}{p}_0)\mathsf{refl}:B(1),\text{that is,}1=0.$$ The simple CPS theorem cannot be applied: its source has neither dependent projection nor the commuting call-by-name rule. A value restriction blocks both $\mathsf{wit}{p}_0$ and $\mathsf{prf}{p}_0$, because $p_0$ is not a proof value. Soundness of any broader purity class requires a separate preservation argument. ◻

ML polymorphism: a third, disjoint boundary

The ML comparison concerns neither the stack machine nor dependent elimination. It asks whether Damas–Milner let-generalization remains sound after continuations become first-class ML values. The answer depends on the operational treatment of $\mathsf{let}$, so the syntax, type assignment, and evaluator are fixed together.

Write $e_1;e_2:=(\lambda z.e_2)e_1$, where $z\notin \mathrm{fv}(e_2)$. The unsoundness result and this closed ML expression are due jointly to Lillibridge and Harper [HDM93]: $$\mathsf{let}f\mathsf{be}\mathsf{callcc}(\lambda k.\lambda x.\mathsf{throw}k(\lambda y.x))\mathsf{in}f1;f\mathsf{true}.$$ Unrestricted assignment gives this expression type $\mathsf{bool}$, while the continuation evaluator returns $1$. The local rules and the complete derivations make both statements precise.

The local expressions, monotypes, and polytypes are Here $b$ ranges over base types, including $\mathsf{int}$ and $\mathsf{bool}$, while $t$ ranges over type variables. Apart from $\mathsf{callcc}$ and $\mathsf{throw}$, constants have base monotypes. Write $\sigma \succcurlyeq \tau$ when $\tau$ is a monotype instance of $\sigma$, and write ${\sigma }_1⊒{\sigma }_2$ when every monotype instance of ${\sigma }_2$ is an instance of ${\sigma }_1$. This relation is reflexive and transitive by inclusion of instance sets. Define $${\mathsf{Close}}_{\mathrm{\Gamma }}(\tau ):=\mathrm{\forall }{t}_1\dots \mathrm{\forall }{t}_n.\tau ,\{t_1,\dots ,t_n\}=\mathrm{ftv}(\tau )\setminus \mathrm{ftv}(\mathrm{\Gamma }).$$ Let $\mathrm{\Sigma }$ be the fixed constant signature. The complete type-assignment card is

$\mathrm{\Gamma }(x)\succcurlyeq \tau$

$\mathrm{\Gamma }⊢x:\tau$

$\mathrm{\Sigma }(c)\succcurlyeq \tau$

$\mathrm{\Gamma }⊢c:\tau$

$\mathrm{\Gamma },x:{\tau }_1⊢e:{\tau }_2$$x\notin \mathrm{dom}(\mathrm{\Gamma })$

$\mathrm{\Gamma }⊢\lambda x.e:{\tau }_1\to {\tau }_2$

$\mathrm{\Gamma }⊢e_1:{\tau }_2\to \tau$$\mathrm{\Gamma }⊢e_2:{\tau }_2$

$\mathrm{\Gamma }⊢e_1{e}_2:\tau$

$\mathrm{\Gamma }⊢e_1:{\tau }_1$$\mathrm{\Gamma },x:{\mathsf{Close}}_{\mathrm{\Gamma }}({\tau }_1)⊢e_2:{\tau }_2$$x\notin \mathrm{dom}(\mathrm{\Gamma })$

$\mathrm{\Gamma }⊢\mathsf{let}x\mathsf{be}{e}_1\mathsf{in}{e}_2:{\tau }_2$

The continuation primitives have exactly the polytypes $$\mathsf{callcc}:\mathrm{\forall }t.(t\mathsf{cont}\to t)\to t,\mathsf{throw}:\mathrm{\forall }s.\mathrm{\forall }t.s\mathsf{cont}\to s\to t.$$ Thus the result type of a throw is arbitrary, but the value sent to the saved continuation has the saved continuation’s argument type.

The operational judgment is $K⊢e\Downarrow a$. Its closed values, evaluation continuations, and answers are The partial application $\mathsf{throw}v$ is a value because $\mathsf{throw}$ is curried; an evaluator continuation $K$ is a reified run-time value, not a surface expression. Fix one answer monotype $\alpha$. Its free type variables are rigid parameters of the operational metatheory: admissible type substitutions fix them. Quantified prefixes are alpha-renamed away from those parameters. For that theorem instance, $\mathsf{Close}$ quantifies only flexible variables, while $\succcurlyeq$ and $⊒$ range over admissible substitutions fixing the rigid answer parameters. Outside the fixed-answer operational argument, the surface assignment rules retain their ordinary meaning. Reified-continuation typing is defined only at that boundary: $$K:\tau \mathsf{cont}⟺x:\tau ⊢K[x]:\alpha .$$ The surface type $\tau \mathsf{cont}$ does not quantify over $\alpha$. If $K$ has one hole, write $K[e]$ for plugging $e$ into that hole and $K[K^{\prime }]$ for continuation composition. The complete evaluator card is

$[]⊢v\Downarrow v$

$[]⊢K[v]\Downarrow a$$K\ne []$

$K⊢v\Downarrow a$

$K[[]e_2]⊢e_1\Downarrow a$$e_1\text{ is not a value}$

$K⊢e_1{e}_2\Downarrow a$

$K[v_1[]]⊢e_2\Downarrow a$$e_2\text{ is not a value}$

$K⊢v_1{e}_2\Downarrow a$

$K⊢e_1[v_2/x]\Downarrow a$

$K⊢(\lambda x.e_1)v_2\Downarrow a$

$v_1\text{ is headed by neither }\lambda \text{ nor }\mathsf{callcc}\text{ nor }\mathsf{throw}$

$K⊢v_1{v}_2\Downarrow \mathsf{wrong}$

$K[\mathsf{let}x\mathsf{be}[]\mathsf{in}{e}_2]⊢e_1\Downarrow a$$e_1\text{ is not a value}$

$K⊢\mathsf{let}x\mathsf{be}{e}_1\mathsf{in}{e}_2\Downarrow a$

$K⊢e_2[v_1/x]\Downarrow a$

$K⊢\mathsf{let}x\mathsf{be}{v}_1\mathsf{in}{e}_2\Downarrow a$

$K⊢vK\Downarrow a$

$K⊢\mathsf{callcc}v\Downarrow a$

$K^{\prime }⊢v\Downarrow a$

$K⊢\mathsf{throw}{K}^{\prime }v\Downarrow a$

Rule seize passes the current $K$ to its operand. Rule jump discards the current $K$ and resumes $K^{\prime }$. In wrong, “headed by $\mathsf{throw}$” includes the partial application $\mathsf{throw}{K}^{\prime }$, whose next argument is governed by jump. These clauses are the continuation semantics at the fixed answer boundary, not a reduction semantics for ${\lambda }_{\mathsf{K}}$.

For the counterexample, $\mathrm{\Sigma }(1)=\mathsf{int}$ and $\mathrm{\Sigma }(\mathsf{true})=\mathsf{bool}$. Unrestricted ML-Let is unsound with this evaluator. Let where the sequencing abbreviation uses application, not let. Thus $P$ is the expression in (35.3). Every type in the critical derivation can be read off from one type variable $u$. Under $k:(u\to u)\mathsf{cont}$ and $x:u$, choose $y:u$. Then $$\lambda y.x:u\to u,\mathsf{throw}k(\lambda y.x):u,\lambda x.\mathsf{throw}k(\lambda y.x):u\to u.$$ The throw uses (35.4) at $s=u\to u$ and local result $t=u$. Instantiating $\mathsf{callcc}$ at $t=u\to u$ gives $$q:(u\to u)\mathsf{cont}\to (u\to u),E:u\to u.$$ Because the outer context is empty, ML-Let assigns $f:\mathrm{\forall }u.u\to u$. Its first occurrence is instantiated at $\mathsf{int}$, its second at $\mathsf{bool}$; hence

The evaluator nevertheless returns $1$. Put $$K_0:=\mathsf{let}f\mathsf{be}[]\mathsf{in}C[f],g:=\lambda x.\mathsf{throw}{K}_0(\lambda y.x),h:=\lambda y.1,$$ and let $K_1:=(\lambda z.g\mathsf{true})[]$ be the sequence continuation waiting for the result of the first call $g1$, and put $K_2:=(\lambda z.h\mathsf{true})[]$. The following is the spine of the evaluation derivation; each double arrow replaces a conclusion by the premise selected by the named operational rule, rather than introducing a new reduction relation: The final judgment is the axiom val0. The first call of $g$ throws $h=\lambda y.1$ back to the let frame $K_0$. Rule sub substitutes $h$ for $f$ and executes both calls. The original static derivation licensed the two occurrences of $f$ at distinct instances, but dynamically $h$ is only the integer constant function, so $h\mathsf{true}$ also returns $1$. For the diagnostic only, extend the signature with $\mathsf{not}:\mathsf{bool}\to \mathsf{bool}$, its two Boolean evaluation clauses, and a clause returning $\mathsf{wrong}$ on a non-Boolean argument. Then $\mathsf{not}P:\mathsf{bool}$, but evaluation first obtains $1$ from $P$ and the new primitive clause returns $\mathsf{wrong}$. This temporary observation primitive is not part of the fixed signature used in theorem 35.46.

The failed invariant is now explicit. The saved frame $K_0$ needs its hole at the polytype $\mathrm{\forall }u.u\to u$, because the body uses $f$ at two instances. Equation (35.5), however, can give a reified continuation only a monotype argument. Fixing the answer monotype $\alpha =\mathsf{bool}$ for this counterexample, the unrestricted proof has $$x:{\mathsf{Close}}_{\varnothing }(u\to u)⊢K_0[x]:\mathsf{bool},$$ not the premise $x:u\to u⊢K_0[x]:\mathsf{bool}$ required by seize.

One exact repair restricts the language itself to values-only let: every term $\mathsf{let}x\mathsf{be}{e}_1\mathsf{in}{e}_2$ must have a syntactic value $e_1$. The bind rule and the continuation form $\mathsf{let}x\mathsf{be}K\mathsf{in}e$ then disappear; value-bound lets still use ML-Let and may still generalize. This is the paper’s values-only language, not the distinct policy which retains arbitrary let right-hand sides but generalizes only selected ones.

Proof of Lemma 35.44 — Admissible type substitution

Proof. Induct on typing. Variable and constant instances compose their witnessing instantiations with $S$. Abstraction and application use the induction hypotheses on their premises. In a let, alpha-rename the variables closed by ${\mathsf{Close}}_{\mathrm{\Gamma }}$ away from the domain and range of $S$. Since $S$ fixes $\mathrm{\Gamma }$, closing the substituted right-hand-side type binds the same renamed variables; apply the two induction hypotheses and rebuild ML-Let. Fixing the rigid answer parameters ensures that the reified-continuation boundary (35.5) is unchanged. ◻

Proof of Lemma 35.45 — Generalized Damas–Milner substitution

Proof. First, replacing a declaration by a more general scheme preserves typing. This follows by induction on the typing derivation: at the replaced variable, transitivity of $⊒$ preserves every monotype instance selected by ML-Var; constants, lambdas, and applications rebuild immediately. In a let case, a more general context has no additional free type variables, so its closure of the right-hand-side monotype is at least as general as the old closure. Apply the same replacement fact to the let-bound declaration in the body, then rebuild with ML-Let.

For substitution, prove the stronger claim with an arbitrary additional context $\mathrm{\Delta }$, disjoint from $z$: from $\mathrm{\Gamma },\mathrm{\Delta },z:\sigma ⊢e:\tau$, derive $\mathrm{\Gamma },\mathrm{\Delta }⊢e[w/z]:\tau$. Induct on the displayed typing derivation. If the last rule is ML-Var at $z$, then $\sigma \succcurlyeq \tau$. Since ${\mathsf{Close}}_{\mathrm{\Gamma }}(\rho )⊒\sigma$, also ${\mathsf{Close}}_{\mathrm{\Gamma }}(\rho )\succcurlyeq \tau$. Hence a substitution $S$ of monotypes for the variables closed in $\rho$, fixing $\mathrm{ftv}(\mathrm{\Gamma })\cup \mathrm{ftv}(\alpha )$, satisfies $\rho [S]=\tau$. Lemma 35.44 applied to $\mathrm{\Gamma }⊢w:\rho$ gives $\mathrm{\Gamma }⊢w:\tau$, and weakening adds $\mathrm{\Delta }$. A different variable and a constant are unchanged.

Rules ML-Abs and ML-App follow by extending $\mathrm{\Delta }$ with the lambda binder, using exchange for the finite-map contexts, and applying the induction hypotheses. In the ML-Let case, apply the first induction hypothesis to its right-hand side. For its body, the induction hypothesis initially retains the scheme ${\mathsf{Close}}_{\mathrm{\Gamma },\mathrm{\Delta },z:\sigma }({\rho }_1)$ of the let variable. Removing $z:\sigma$ can only quantify more variables, so $${\mathsf{Close}}_{\mathrm{\Gamma },\mathrm{\Delta }}({\rho }_1)⊒{\mathsf{Close}}_{\mathrm{\Gamma },\mathrm{\Delta },z:\sigma }({\rho }_1).$$ The scheme-strengthening fact from the first paragraph replaces the retained declaration by ${\mathsf{Close}}_{\mathrm{\Gamma },\mathrm{\Delta }}({\rho }_1)$; ML-Let then rebuilds the substituted term.

The run-time value clause for a reified continuation is stable under the same infrastructure. From $K:\rho \mathsf{cont}$ obtain $x:\rho ⊢K[x]:\alpha$. A type substitution $S$ gives $x:\rho [S]⊢K[x]:\alpha$, because $S$ fixes the rigid variables of the answer monotype; hence $K:\rho [S]\mathsf{cont}$. In the term-substitution induction a reified $K$ is unchanged because run-time continuations are term-closed. The partial-$\mathsf{throw}$ value uses ML-App. Thus the five surface rules and both additional run-time value forms are covered. Taking $\mathrm{\Delta }=\varnothing$ proves the statement. ◻

Proof of Theorem 35.46 — Values-only soundness

Proof. Use induction on the evaluation derivation. Each substitution step uses lemma 35.45. Its monomorphic specialization takes $\sigma =\rho$; its value-bound-let specialization takes $\sigma ={\mathsf{Close}}_{\varnothing }(\rho )$.

For val0, the premise $x:\tau ⊢[][x]:\alpha$ forces the hole to be used at $\alpha$, so substitution gives $v:\alpha$. For val1, monomorphic plugging gives $K[v]:\alpha$; apply the induction hypothesis to $[]⊢K[v]\Downarrow a$. In the fn case, inversion gives $e_1:\rho \to \tau$ and $e_2:\rho$. The pushed continuation has $$y:\rho \to \tau ⊢K[y{e}_2]:\alpha ,$$ so the induction hypothesis applies to evaluation of $e_1$. The arg case is the same calculation with $y:\rho ⊢K[v_{1}y]:\alpha$. The beta case follows from monomorphic substitution. The sub case follows from value substitution at ${\mathsf{Close}}_{\varnothing }(\rho )$. There is no bind case.

For seize, inversion of $\mathsf{callcc}v:\tau$ gives $v:\tau \mathsf{cont}\to \tau$. The theorem’s continuation premise and (35.5) give $K:\tau \mathsf{cont}$; hence $vK:\tau$, and the induction hypothesis applies to the rule premise. For jump, inversion of $\mathsf{throw}{K}^{\prime }v:\tau$ gives a monotype $\rho$ with $K^{\prime }:\rho \mathsf{cont}$ and $v:\rho$. By the definition of reified continuation typing, $z:\rho ⊢K^{\prime }[z]:\alpha$, so the induction hypothesis applies to $K^{\prime }⊢v\Downarrow a$. Finally, a well-typed operator value of arrow type is a lambda, $\mathsf{callcc}$, or a partial application of $\mathsf{throw}$; a reified continuation has a $\mathsf{cont}$ type. Thus the wrong rule cannot close a typed derivation. These cases exhaust the evaluator and establish $a:\alpha$, which excludes the only nonvalue answer $\mathsf{wrong}$. For the corollary take $K=[]$ and $\alpha =\tau$, after standardizing the typing derivation’s quantified and flexible variables apart from $\mathrm{ftv}(\tau )$; then regard $\mathrm{ftv}(\tau )$ as the rigid parameters of that theorem instance. ◻

The repair blocks $P$ before evaluation: its let right-hand side $E$ is an application of $\mathsf{callcc}$, not a syntactic value. The theorem does not identify every safe nonvalue and does not license a purity or effect generalization beyond the language fixed in convention 35.43. It is the values-only half of the soundness result proved by Harper, Duba, and MacQueen [HDM93].

Suggested first pass.

Begin with exercise 35.9, exercise 35.10. Continue with exercise 35.11 and exercise 35.8; then use the remaining problems to test the normalization, dependent, and ML-polymorphism boundaries. No problem in this seminar is a prerequisite for a later chapter.

Exercise 35.9¶

★★☆ Let $K=\bullet ;{\mathsf{add}}_3[];[]7$, where the top frame expects a function $\mathsf{Nat}\to \mathsf{Nat}$. Derive $K:(\mathsf{Nat}\to \mathsf{Nat})\Rightarrow \mathsf{Nat}$, compute $K_h^{\mathsf{k}}$, and verify its target type binder by binder. Then run the source and target states for the returned value $\lambda x:\mathsf{Nat}.x$.

Referenced from 4 locations

• Control Operators and Classical Proofs
• ch:control-operators: ch:control-operators

Exercise 35.10¶

★★★ Fix $K:A\Rightarrow R$ and a closed value $a:A$. Let $C$ be the case frame $$\mathsf{case}[]\mathsf{of}\{\mathsf{inl}x\mapsto x;\mathsf{inr}q\mapsto \mathsf{throw}a\mathsf{to}q\},$$ so $C:(A+\mathsf{Cont}A)\Rightarrow A$. Derive $K;C:(A+\mathsf{Cont}A)\Rightarrow R$, start ${\mathsf{lem}}_A$ under that stack, and splice both traces of proposition 35.16 into one uninterrupted run ending at $K◃a$. Translate the case frame and the restored injection frame to CPS and check the corresponding target reductions.

Referenced from 4 locations

• Control Operators and Classical Proofs
• ch:control-operators: ch:control-operators

Exercise 35.11¶

★★☆ For a $0$-free context $E$, expand the translation of $$⟨E[{\mathsf{shift}}_{0}k.e]\mid x.e_r⟩.$$ Perform the deep-handler contraction and every beta step until the translation of $$e[(\lambda z.⟨E[z]\mid x.e_r⟩)/k]$$ appears. State where $0$-freeness is used.

Referenced from 4 locations

• Control Operators and Classical Proofs
• ch:control-operators: ch:control-operators

Exercise 35.12¶

★☆☆ Construct a fictitious translation which maps every source state to one fixed target value. It satisfies a zero-or-more-step simulation. Explain formally why it cannot prove theorem 35.13, and identify the exact use of positivity in that proof.

Referenced from 3 locations

• Control Operators and Classical Proofs
• ch:control-operators: ch:control-operators

Exercise 35.13¶

★☆☆ Impose the syntactic rule that $\mathsf{wit}p$ and $\mathsf{prf}p$ are formed only when $p$ is a value. Show precisely which two expressions in the numeral-collapse derivation become ill formed. Explain why this observation blocks that derivation but is not, by itself, a preservation proof for a complete dependent control calculus.

Referenced from 3 locations

• Control Operators and Classical Proofs
• ch:control-operators: ch:control-operators

Exercise 35.14¶

★★★ Practical project.control-machine-cps Implement the finite stack machine and its represented CPS spine in Kappa. Maintain the invariant that a captured stack is the complete ordered frame list and that applying a saved continuation replaces, rather than extends, the current list; the saved list remains available to later callers. The four discriminatory cases must check complete-spine capture, stack replacement on throw, persistence across two callers, and the two-stage LEM change-of-mind trace. Direct/CPS equality, the declared positive costs, and the DNE constructor equality are smoke outputs only, not independent evidence. Mutate capture to retain only the top frame; the mutant must still type-check and audit cleanly but fail the complete-spine and LEM cases. Appendix E records the four acceptance commands, and appendix F gives the construction stages.

Referenced from 4 locations

• Control Operators and Classical Proofs
• Object calculus checker and evaluator
• ch:control-operators: ch:control-operators

Sources.

Griffin identified typed control with classical proofs [Gri90]. Harper develops the stack-machine and CPS background [Har16]. Kameyama and Hasegawa give the equational boundary for delimited control [KH03]. The four typed correspondences between handlers and control follow Piróg, Polesiuk, and Sieczkowski [PPS19]. Herbelin gives the Sigma-type counterexample and identifies the vacuity rule as the load-bearing boundary [Her05]; Miquey supplies the sequent-calculus presentation and value-restriction repair used here [Miq19].

Harper, Duba, and MacQueen supply the ML evaluator and exact values-only theorem; their footnote 3 credits the polymorphic counterexample jointly to Lillibridge and Harper [HDM93].