Control calculi and dependent projection

${\lambda }_{\mathsf{K}}$: surface, machine, and runtime typing

The call-by-value continuation calculus extends the simply typed products, sums, $\mathbf{0}$, $\mathbf{1}$, naturals, and arrows by $$A::=\cdots \mid \mathsf{Cont}A,e::=\cdots \mid \mathsf{letcc}k:\mathsf{Cont}A\mathsf{in}e\mid \mathsf{throw}e\mathsf{to}e.$$ Its two new surface rules are

$\mathrm{\Gamma },k:\mathsf{Cont}A⊢e:A$

$\mathrm{\Gamma }⊢\mathsf{letcc}k:\mathsf{Cont}A\mathsf{in}e:A$

$\mathrm{\Gamma }⊢e_1:A$$\mathrm{\Gamma }⊢e_2:\mathsf{Cont}A$$\mathrm{\Gamma }⊢B\mathsf{type}$

$\mathrm{\Gamma }⊢\mathsf{throw}{e}_1\mathsf{to}{e}_2:B$

Runtime values additionally contain $\mathsf{cont}(K)$, and States are $K▹e$ and $K◃v$. The complete pure roots are The three push roots for $⟨e_1,e_2⟩$, $\mathsf{inl}e$, and $\mathsf{inr}e$ apply only when their complete subject is not already a value; the corresponding return roots handle value subjects. This is the same value-first side condition used in the chapter. Writing $C$ for the displayed pair of case branches, the remaining pure roots are There is no return root for the abort frame. The complete control roots are

For a fixed run answer $R$, frame typing is exactly The case row requires $x:A{⊢}_R{e}_1:C$ and $y:B{⊢}_R{e}_2:C$. Stack, internal value, and state typing are

$\bullet :R\Rightarrow R$

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

$K;F:A\Rightarrow R$

$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 fixed-answer CPS signature

The pure target has the same base, product, sum, and empty types and no control forms. Value and computation types are $$\begin{array}{c}{\mathbf{0}}^{\mathsf{v}}=\mathbf{0},{\mathbf{1}}^{\mathsf{v}}=\mathbf{1},{\mathsf{Nat}}^{\mathsf{v}}=\mathsf{Nat},(A\times B{)}^{\mathsf{v}}=A^{\mathsf{v}}\times B^{\mathsf{v}},\\ (A+B{)}^{\mathsf{v}}=A^{\mathsf{v}}+B^{\mathsf{v}},(A\to B{)}^{\mathsf{v}}=A^{\mathsf{v}}\to B^{\mathsf{c}},(\mathsf{Cont}A{)}^{\mathsf{v}}=A^{\mathsf{v}}\to \mathbf{0},\\ A^{\mathsf{c}}=(A^{\mathsf{v}}\to \mathbf{0})\to \mathbf{0}.\end{array}$$ Values translate homomorphically, except $$(\lambda x.e{)}^{\mathsf{v}}=\lambda x.e^{\mathsf{c}},\mathsf{cont}(K{)}^{\mathsf{v}}=K_h^{\mathsf{k}},v^{\mathsf{c}}=\lambda k.k{v}^{\mathsf{v}}.$$ The complete nonvalue term translation is For case, the continuation $k$ is passed to the translation of the selected branch. Fix fresh $h:R^{\mathsf{v}}\to \mathbf{0}$. The complete stack translation is The case-frame clause is $$\lambda s.\mathsf{case}s\mathsf{of}\{\mathsf{inl}x\mapsto e_1^{\mathsf{c}}{K}_h^{\mathsf{k}};\mathsf{inr}y\mapsto e_2^{\mathsf{c}}{K}_h^{\mathsf{k}}\}.$$ Finally $$\Vert K▹e{\Vert }_h=e^{\mathsf{c}}{K}_h^{\mathsf{k}},\Vert K◃v{\Vert }_h=K_h^{\mathsf{k}}{v}^{\mathsf{v}}.$$

The PPS ordered-row core and its four scoped deltas

The common kind, type/effect/row, term, and evaluation-context grammars are The variable subscripts are metanotational kind tags, and ${\epsilon }_{\mathrm{ext}}$ ranges over one of the four extension-specific effect forms below. A metavariable $\sigma$ ranges over an expression of the kind demanded by its judgment. Thus the raw grammar keeps types, single effects, and ordered rows distinct. Rows are ordered. Writing a single effect after the slash abbreviates the row $\epsilon \cdot \iota$. Kinding consists of K-Var, K-Arr, K-All, K-Nil, and K-Cons:

$\alpha ::\kappa \in \mathrm{\Delta }$

$\mathrm{\Delta }⊢\alpha ::\kappa$

$\mathrm{\Delta }⊢{\tau }_1::\mathsf{T}$$\mathrm{\Delta }⊢\rho ::\mathsf{R}$$\mathrm{\Delta }⊢{\tau }_2::\mathsf{T}$

$\mathrm{\Delta }⊢{\tau }_1\stackrel{\rho }{\to }{\tau }_2::\mathsf{T}$

$\mathrm{\Delta },\alpha ::\kappa ⊢\tau ::\mathsf{T}$

$\mathrm{\Delta }⊢\mathrm{\forall }\alpha ::\kappa .\tau ::\mathsf{T}$

$\mathrm{\Delta }⊢\iota ::\mathsf{R}$

$\mathrm{\Delta }⊢\epsilon ::\mathsf{E}$$\mathrm{\Delta }⊢\rho ::\mathsf{R}$

$\mathrm{\Delta }⊢\epsilon \cdot \rho ::\mathsf{R}$

The term judgment $\mathrm{\Delta };\mathrm{\Gamma }⊢e:\tau /\rho$ is generated by P-Var, P-Lam, P-App, P-Gen, P-Inst, P-Sub, and P-Lift, exactly:

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

$\mathrm{\Delta };\mathrm{\Gamma }⊢x:\tau /\iota$

$\mathrm{\Delta };\mathrm{\Gamma },x:{\tau }_1⊢e:{\tau }_2/\rho$

$\mathrm{\Delta };\mathrm{\Gamma }⊢\lambda x.e:{\tau }_1\stackrel{\rho }{\to }{\tau }_2/\iota$

$\mathrm{\Delta };\mathrm{\Gamma }⊢e_1:{\tau }_1\stackrel{\rho }{\to }{\tau }_2/\rho$$\mathrm{\Delta };\mathrm{\Gamma }⊢e_2:{\tau }_1/\rho$

$\mathrm{\Delta };\mathrm{\Gamma }⊢e_1{e}_2:{\tau }_2/\rho$

$\mathrm{\Delta },\alpha ::\kappa ;\mathrm{\Gamma }⊢e:\tau /\iota$$\alpha \notin \mathsf{FV}(\mathrm{\Gamma })$

$\mathrm{\Delta };\mathrm{\Gamma }⊢e:\mathrm{\forall }\alpha ::\kappa .\tau /\iota$

$\mathrm{\Delta }⊢\sigma ::\kappa$$\mathrm{\Delta };\mathrm{\Gamma }⊢e:\mathrm{\forall }\alpha ::\kappa .\tau /\rho$

$\mathrm{\Delta };\mathrm{\Gamma }⊢e:\tau [\sigma /\alpha ]/\rho$

$\mathrm{\Delta };\mathrm{\Gamma }⊢e:{\tau }_1/{\rho }_1$

$\mathrm{\Delta };\mathrm{\Gamma }⊢e:{\tau }_2/{\rho }_2$

$\mathrm{\Delta }⊢\epsilon ::\mathsf{E}$$\mathrm{\Delta };\mathrm{\Gamma }⊢e:\tau /\rho$

$\mathrm{\Delta };\mathrm{\Gamma }⊢[e]:\tau /\epsilon \cdot \rho$

Subtyping has reflexive, contravariant/covariant arrow, universal, nil-row, and same-head row-cons rules. In full:

$\mathrm{\Delta }⊢\rho ::\mathsf{R}$

Core roots are beta and $[v]⟼v$, closed under $E$. Freeness starts at $0\text{-}\mathsf{free}([])$, is preserved by application frames, and satisfies $$\frac{n\text{-}\mathsf{free}(E)}{(n+1)\text{-}\mathsf{free}([E])}.$$

The exact deep-handler delta is $$\epsilon ={\mathrm{\Delta }}_0.{\tau }_1\Rightarrow {\tau }_2,$$ with rules

$\mathrm{\Delta },{\mathrm{\Delta }}_0⊢{\tau }_1::\mathsf{T}$$\mathrm{\Delta },{\mathrm{\Delta }}_0⊢{\tau }_2::\mathsf{T}$

$\mathrm{\Delta }⊢{\mathrm{\Delta }}_0.{\tau }_1\Rightarrow {\tau }_2::\mathsf{E}$

$(n+1)\text{-}\mathsf{free}(E)$

$n\text{-}\mathsf{free}(\mathsf{handle}E\{x,r.e_h;y.e_r\})$

$\mathrm{\Delta };\mathrm{\Gamma }⊢v:\delta {\tau }_1/\iota$$\mathrm{\Delta }⊢\delta ::{\mathrm{\Delta }}_0$$\mathrm{\Delta }⊢\epsilon ::\mathsf{E}$

$\mathrm{\Delta };\mathrm{\Gamma }⊢\mathsf{do}v:\delta {\tau }_2/\epsilon$

$\mathrm{\Delta };\mathrm{\Gamma }⊢e:\tau /\epsilon \cdot \rho$$\mathrm{\Delta },{\mathrm{\Delta }}_0;\mathrm{\Gamma },x:{\tau }_1,r:{\tau }_2\stackrel{\rho }{\to }{\tau }_r⊢e_h:{\tau }_r/\rho$$\mathrm{\Delta };\mathrm{\Gamma },y:\tau ⊢e_r:{\tau }_r/\rho$

$\mathrm{\Delta };\mathrm{\Gamma }⊢\mathsf{handle}e\{x,r.e_h;y.e_r\}:{\tau }_r/\rho$

For $0$-free $E$, its operation root substitutes $$\lambda z.\mathsf{handle}E[z]\{x,r.e_h;y.e_r\}$$ for $r$; its return root substitutes the returned value in $e_r$.

The exact ${\mathsf{shift}}_0$ delta is $\epsilon ={\mathrm{\Delta }}_0.\tau /\rho$:

$\mathrm{\Delta },{\mathrm{\Delta }}_0⊢\tau ::\mathsf{T}$$\mathrm{\Delta },{\mathrm{\Delta }}_0⊢\rho ::\mathsf{R}$

$\mathrm{\Delta }⊢{\mathrm{\Delta }}_0.\tau /\rho ::\mathsf{E}$

$(n+1)\text{-}\mathsf{free}(E)$

$n\text{-}\mathsf{free}(⟨E\mid x.e_r⟩)$

$\mathrm{\Delta },{\mathrm{\Delta }}_0;\mathrm{\Gamma },k:{\tau }^{\prime }\stackrel{\rho }{\to }\tau ⊢e:\tau /{\rho }_0$$\mathrm{\Delta }⊢{\tau }^{\prime }::\mathsf{T}$$\mathrm{\Delta }⊢\epsilon \cdot {\rho }_0::\mathsf{R}$

$\mathrm{\Delta };\mathrm{\Gamma }⊢{\mathsf{shift}}_{0}k.e:{\tau }^{\prime }/\epsilon \cdot {\rho }_0$

$\mathrm{\Delta }⊢\delta ::{\mathrm{\Delta }}_0$$\mathrm{\Delta };\mathrm{\Gamma }⊢e:{\tau }^{\prime }/\epsilon \cdot \delta \rho$$\mathrm{\Delta };\mathrm{\Gamma },x:{\tau }^{\prime }⊢e_r:\delta \tau /\delta \rho$

$\mathrm{\Delta };\mathrm{\Gamma }⊢⟨e\mid x.e_r⟩:\delta \tau /\delta \rho$

For $0$-free $E$, $$⟨E[{\mathsf{shift}}_{0}k.e]\mid x.e_r⟩⟼e[(\lambda z.⟨E[z]\mid x.e_r⟩)/k].$$

The shallow-handler delta is recursive: $\epsilon =\mu \alpha .{\mathrm{\Delta }}_0.{\tau }_1\Rightarrow {\tau }_2$. Put ${\delta }^{\epsilon }=\delta [\alpha \mapsto \epsilon ]$. Its rules are

$\mathrm{\Delta },\alpha ::\mathsf{E},{\mathrm{\Delta }}_0⊢{\tau }_1::\mathsf{T}$$\mathrm{\Delta },\alpha ::\mathsf{E},{\mathrm{\Delta }}_0⊢{\tau }_2::\mathsf{T}$

$\mathrm{\Delta }⊢\epsilon ::\mathsf{E}$

$\mathrm{\Delta };\mathrm{\Gamma }⊢v:{\delta }^{\epsilon }{\tau }_1/\iota$$\mathrm{\Delta }⊢\delta ::{\mathrm{\Delta }}_0$$\mathrm{\Delta }⊢\epsilon ::\mathsf{E}$

$\mathrm{\Delta };\mathrm{\Gamma }⊢\mathsf{do}v:{\delta }^{\epsilon }{\tau }_2/\epsilon$

$\mathrm{\Delta };\mathrm{\Gamma }⊢e:\tau /\epsilon \cdot \rho$$\mathrm{\Delta },{\mathrm{\Delta }}_0;\mathrm{\Gamma },x:{\tau }_1[\epsilon /\alpha ],r:{\tau }_2[\epsilon /\alpha ]\stackrel{\epsilon \cdot \rho }{\to }\tau ⊢e_h:{\tau }_r/\rho$$\mathrm{\Delta };\mathrm{\Gamma },y:\tau ⊢e_r:{\tau }_r/\rho$

$\mathrm{\Delta };\mathrm{\Gamma }⊢\mathsf{handle}e\{x,r.e_h;y.e_r\}:{\tau }_r/\rho$

Its operation root substitutes $\lambda z.E[z]$ for $r$, without reinstalling the handler.

The ${\mathsf{control}}_0$ delta is $\epsilon =\mu \alpha .{\mathrm{\Delta }}_0.{\tau }_1\Rightarrow {\tau }_2/\rho$:

$\mathrm{\Delta },\alpha ::\mathsf{E},{\mathrm{\Delta }}_0⊢{\tau }_1::\mathsf{T}$$\mathrm{\Delta },\alpha ::\mathsf{E},{\mathrm{\Delta }}_0⊢{\tau }_2::\mathsf{T}$$\mathrm{\Delta },\alpha ::\mathsf{E},{\mathrm{\Delta }}_0⊢\rho ::\mathsf{R}$

$\mathrm{\Delta }⊢\epsilon ::\mathsf{E}$

$\mathrm{\Delta },{\mathrm{\Delta }}_0;\mathrm{\Gamma },k:{\tau }^{\prime }\stackrel{\epsilon \cdot \rho [\epsilon /\alpha ]}{\to }{\tau }_1[\epsilon /\alpha ]⊢e:{\tau }_2[\epsilon /\alpha ]/{\rho }_0$$\mathrm{\Delta }⊢{\tau }^{\prime }::\mathsf{T}$$\mathrm{\Delta }⊢\epsilon \cdot {\rho }_0::\mathsf{R}$

$\mathrm{\Delta };\mathrm{\Gamma }⊢{\mathsf{control}}_{0}k.e:{\tau }^{\prime }/\epsilon \cdot {\rho }_0$

For ${\tau }_e={\delta }^{\epsilon }{\tau }_1$, ${\tau }_r={\delta }^{\epsilon }{\tau }_2$, and ${\rho }_r={\delta }^{\epsilon }\rho$,

$\mathrm{\Delta }⊢\delta ::{\mathrm{\Delta }}_0$$\mathrm{\Delta };\mathrm{\Gamma }⊢e:{\tau }_e/\epsilon \cdot {\rho }_r$$\mathrm{\Delta };\mathrm{\Gamma },x:{\tau }_e⊢e_r:{\tau }_r/{\rho }_r$

$\mathrm{\Delta };\mathrm{\Gamma }⊢⟨e\mid x.e_r⟩:{\tau }_r/{\rho }_r$

Its capture root substitutes $\lambda z.E[z]$, omitting the reset. Every handler/reset context lowers the freeness index by one; every capture root requires a $0$-free context.

The nonhomomorphic term clauses whose signatures the deltas support are

For parity, the four single-effect translations are For the reverse shallow clause, put $$H(a,b_1,b_2,g):=\mathrm{\forall }{\mathrm{\Delta }}_0.\mathsf{SD}({\tau }_1)\to (\mathsf{SD}({\tau }_2)\stackrel{a\cdot g}{\to }{b}_1)\stackrel{g}{\to }{b}_2.$$ Then In every displayed $\mathrm{\forall }{\mathrm{\Delta }}_0$, the quantifier scopes the entire following arrow expression and retains the declared kind of every member of ${\mathrm{\Delta }}_0$.

The hypothetical dependent commuting-projection boundary

This is a separate call-by-name calculus, not ${\lambda }_{\mathsf{K}}$. Contexts are sorted: $$\mathrm{\Gamma }::=\varnothing \mid \mathrm{\Gamma },x:\mathsf{Nat}\mid \mathrm{\Gamma },a:A\mid \mathrm{\Gamma },k÷A\mid \mathrm{\Gamma },k÷\mathsf{Nat}.$$ Here $k÷A$ names a proof continuation accepting an $A$-proof, and $k÷\mathsf{Nat}$ names a number continuation. The rules below print these entries as $k:\mathrm{\neg }A$ and $k:\mathsf{Nat}\to \mathrm{\perp }$ for readability; they are continuation names rather than formulas or ordinary functions. Formula formation and the number/proof leaves are

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

$\mathrm{\Gamma }⊢t:\mathsf{Nat}$$\mathrm{\Gamma }⊢u:\mathsf{Nat}$

$\mathrm{\Gamma }⊢t=u\mathsf{prop}$

$\mathrm{\Gamma },x:\mathsf{Nat}⊢A\mathsf{prop}$

$\mathrm{\Gamma }⊢\mathrm{\exists }x:\mathsf{Nat}.A\mathsf{prop}$

$n\in \mathbb{N}$

$\mathrm{\Gamma }⊢n:\mathsf{Nat}$

$x:\mathsf{Nat}\in \mathrm{\Gamma }$

$\mathrm{\Gamma }⊢x:\mathsf{Nat}$

$a:A\in \mathrm{\Gamma }$

$\mathrm{\Gamma }⊢a:A$

The exact strong-pair and equality rules are

$\mathrm{\Gamma }⊢t:\mathsf{Nat}$$\mathrm{\Gamma }⊢p:A[t/x]$

$\mathrm{\Gamma }⊢(t,p):\mathrm{\exists }x:\mathsf{Nat}.A$

$\mathrm{\Gamma }⊢p:\mathrm{\exists }x:\mathsf{Nat}.A$

$\mathrm{\Gamma }⊢\mathsf{wit}p:\mathsf{Nat}$

$\mathrm{\Gamma }⊢p:\mathrm{\exists }x:\mathsf{Nat}.A$

$\mathrm{\Gamma }⊢\mathsf{prf}p:A[\mathsf{wit}p/x]$

$t\equiv u$

$\mathrm{\Gamma }⊢\mathsf{refl}:t=u$

$\mathrm{\Gamma }⊢p:t=u$$\mathrm{\Gamma }⊢q:B[t/x]$

$\mathrm{\Gamma }⊢\mathsf{subst}pq:B[u/x]$

Conversion along congruential formula convertibility is the explicit rule

$\mathrm{\Gamma }⊢p:A$$A\equiv B$

$\mathrm{\Gamma }⊢p:B$

Proof and number control have

$\mathrm{\Gamma },k:\mathrm{\neg }A⊢p:A$

$\mathrm{\Gamma }⊢{\mathsf{callcc}}_{k}p:A$

$\mathrm{\Gamma },k:\mathrm{\neg }A⊢p:A$$\mathrm{\Gamma }⊢B\mathsf{prop}$

$\mathrm{\Gamma },k:\mathrm{\neg }A⊢{\mathsf{throw}}_{k}p:B$

$\mathrm{\Gamma },k:\mathsf{Nat}\to \mathrm{\perp }⊢t:\mathsf{Nat}$

$\mathrm{\Gamma }⊢{\mathsf{callcc}}_{k}t:\mathsf{Nat}$

$\mathrm{\Gamma },k:\mathsf{Nat}\to \mathrm{\perp }⊢t:\mathsf{Nat}$$\mathrm{\Gamma }⊢B\mathsf{prop}$

$\mathrm{\Gamma },k:\mathsf{Nat}\to \mathrm{\perp }⊢{\mathsf{throw}}_{k}t:B$

The assumption $k:\mathrm{\neg }A$ names a captured proof context accepting $A$ with command answer sort $\mathrm{\perp }$; $k:\mathsf{Nat}\to \mathrm{\perp }$ analogously names a captured number context. They are not lambda-bound function variables and are invoked only by their matching throws. Pair projections, equality substitution, commuting, and vacuity are $$\begin{array}{c}\mathsf{wit}(t,p)⟼t,\mathsf{prf}(t,p)⟼p,\mathsf{subst}\mathsf{refl}p⟼p,\\ \mathsf{wit}({\mathsf{callcc}}_{k}p)⟼{\mathsf{callcc}}_k(\mathsf{wit}(p[k\circ \mathsf{wit}/k])),\\ {\mathsf{callcc}}_{k}u⟼u(k\notin \mathsf{FV}(u)).\end{array}$$ Reduction is closed under both sorts of $\mathsf{callcc}$. The value-restricted variant changes Dep-Wit and Dep-Prf so their premise must be a syntactic $V$; no soundness theorem beyond that boundary is imported.

The polymorphic continuation counterexample card

For the separate ML assignment card, let ${\mathsf{Close}}_{\mathrm{\Gamma }}(\tau )$ universally quantify exactly $\mathrm{ftv}(\tau )\setminus \mathrm{ftv}(\mathrm{\Gamma })$, and write $\sigma \succcurlyeq \tau$ for monotype instantiation. Its complete rules are

$\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$

At a fixed answer monotype, its continuation evaluator is generated by

$[]⊢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$