Control operators, CPS, and classical proofs

Chapter 17 fixes closed call-by-value simply typed products, sums, $0$, $1$, naturals, arrows, and the primitive ${\mathsf{add}}_m$, extended only by $\mathsf{Cont}A$, $\mathsf{letcc}$, and $\mathsf{throw}$. Runtime continuations are persistent whole stacks. The machine includes every pure evaluation frame, both throw phases, and an internal $\mathsf{cont}(K)$; continuation values are not source syntax. All frames and states carry one ambient run answer $R$. There is no recursion, store, exception primitive, delimiter, effect row, or dependent type in this signature.

Closed value substitution and canonical continuations are lemma 35.2. Preservation, deterministic progress, and safety are theorem 35.3, theorem 35.4, corollary 35.5. The final throw root discards its current stack and restores a stack with the same ambient answer type; canonical forms is used when the second throw frame returns.

The pure target is simply typed products, sums, $0$, $1$, naturals, and arrows with compatible $\beta \delta$-reduction. The answer type is fixed to $0$, while a fresh open variable $h:R^{\mathsf{v}}\to \mathbf{0}$ represents the empty source stack. The translation includes every source term, every machine frame, internal continuation values, and both state directions. CPS substitution, typing, and positive-step simulation are lemma 35.10, theorem 35.11, theorem 35.12. Positivity transfers target strong normalization to ${\lambda }_{\mathsf{K}}$, and progress plus canonical forms gives consistency, by theorem 35.13, corollary 35.14.

Proposition 35.15 derives $\mathsf{Cont}(\mathsf{Cont}A)\to A$. Proposition 35.16 derives $A+\mathsf{Cont}A$ and records both the initial right return and the later left return through the same caller stack. These are typed programs with nonlocal operational behavior, not new definitional equalities of the pure calculus.

The handler/control bridge is separate from ${\lambda }_{\mathsf{K}}$. Its common core has kinds $\mathsf{T},\mathsf{E},\mathsf{R}$, ordered rows, quantification over all three kinds, explicit generalization, instantiation, subtyping, and lift, and $n$-freeness for delimiter scope. Generalization requires its bound variable to be absent from $\mathsf{FV}(\mathrm{\Gamma })$; repeated generalization first alpha-renames the effect binders away from the term context. An omitted trailing $\iota$ after a single effect is a stated abbreviation, not a change of kind.

Deep handlers use effects ${\mathrm{\Delta }}_0.{\tau }_1\Rightarrow {\tau }_2$; ${\mathsf{shift}}_0$ uses ${\mathrm{\Delta }}_0.\tau /\rho$. Every $\mathrm{\forall }{\mathrm{\Delta }}_0$ scopes the complete translated operation function and retains each binder kind. Translation commutes with kind substitution, value substitution, context plugging, and freeness. Both directions preserve typing and source roots by a positive target sequence. Only deep-handler-to-${\mathsf{shift}}_0$ requires arbitrary-context ${⟶}_i^{+}$, because one administrative beta contraction occurs beneath a lambda; the reverse direction uses ordinary evaluation reduction. These statements are exactly lemma 35.25, theorem 35.30. The named syntax translations are $\mathsf{DH}(-)$ and $\mathsf{DD}(-)$; double brackets remain reserved for denotations.

Shallow handlers and ${\mathsf{control}}_0$ use recursive single effects $\mu \alpha .\cdots$, because their resumed continuations omit the handler or reset and may expose the same leading effect again. Both translations preserve kinding, typing, substitution, plugging, freeness, and source roots. Both semantic directions use ordinary positive evaluation reduction; neither uses ${⟶}_i$. The exact result is lemma 35.36, theorem 35.40. No theorem swaps deep with ${\mathsf{control}}_0$, shallow with ${\mathsf{shift}}_0$, or these delimited calculi with ${\lambda }_{\mathsf{K}}$. The two named translations are $\mathsf{SH}(-)$ and $\mathsf{SD}(-)$.

Definition 35.41 is an explicitly hypothetical call-by-name calculus with strong existential projections, proof and number $\mathsf{callcc}$, arbitrary-result throw, compatibility below $\mathsf{callcc}$, and a commuting first-projection rule. It derives $1=0$ by proposition 35.42. This counterexample does not execute in the CBV ${\lambda }_{\mathsf{K}}$ machine. Requiring $\mathsf{wit}$ and $\mathsf{prf}$ to eliminate proof values blocks the displayed term but is not claimed as a complete soundness proof for dependent control.

The whole-stack machine, safety boundary, and CPS organization follow the KPCF and continuation chapters of Harper’s Practical Foundations for Programming Languages [Har16]. Kameyama–Hasegawa, Section 2.1, Section 3 Theorem 1, and Section 6.2 Theorem 9 delimit the shift/reset equational and CPS boundary [KH03]. Piróg–Polesiuk–Sieczkowski, printed pp. 30:2–30:14, Figures 1–14 and Theorems 1–12, supply the exact four typed handler/control directions and their asymmetric semantic scopes [PPS19]. Herbelin, §2.6–2.7 and Corollary 5, supplies the Sigma-type collapse and the exact role of vacuity [Her05]. Miquey, Section 2.1, printed p. 8:6, Section 2.2, printed pp. 8:7–8 and footnote 6, supplies the sequent-calculus presentation and value-restriction boundary [Miq19].

Appendix E’s Kappa companion represents stack and CPS spines as ordinary data. Four discriminatory cases corroborate complete-spine capture, stack replacement, persistence, and the LEM change-of-mind trace. The remaining direct/CPS, declared-cost, and DNE constructor equalities are smoke checks, not independent evidence. Kappa has no raw control primitive, and the artifact proves none of the metatheorems above. The archived PPS Coq supplement is separate compatibility evidence at its historical Coq 8.8.2 boundary.