appendix sectionnotation

Control operators and classical proofs

symbol	meaning	first
symbol	meaning	first
$Cont A$ , $letcc$ , $throw$	continuation type, whole-stack capture, and reinstatement	35.1
$F, K$ , $K ▹ e$ , $K ◃ v$	frame, stack, evaluation state, and return state	35.1
$s ⟶ s^{'}$ , $s ⟶^{*} s^{'}$	one stack-machine transition and its finite closure	35.1
$cont (K)$ , $K : A \Rightarrow R$	internal persistent continuation value and stack typing	35.1
$A^{v}$ , $A^{c}$ , $e^{c}$	CPS value type, computation type, and term translation	35.7, 35.8
$K_{h}^{k}$ , $‖ s ‖_{h}$	stack-as-function and machine-state CPS translations	35.9
$e ⟶_{β δ} e^{'}$ , $e ⟶_{β δ}^{*} e^{'}$	one CPS-target beta-delta step and its finite closure	35.8
${dne}_{A}$ , ${lem}_{A}$	control terms for DNE and excluded middle	35.15, 35.16
$T, E, R$ , $ι$ , $ε \cdot ρ$	PPS kinds, empty ordered row, and row extension	35.18
$Δ; Γ ⊢ e : τ / ρ$	PPS type-and-ordered-effect judgment	35.18
$n - free (E)$	balance of unmatched lifts above the hole; application preserves it, a lift raises it, and the matching delimiter discharges one	35.18
$[e]$ , $E [e]$	PPS lift/control mask and metalevel plugging into a one-hole context	35.18
$k \div A$ , $k \div N$	continuation-context entries for value and natural-result continuations	35.41
$do$ , $handle$ , ${shift}_{0}$ , ${control}_{0}$	deep/shallow operations and delimited capture forms	35.19, 35.20, 35.31
$DH (-)$ , $DD (-)$	named PPS syntax translations between ${shift}_{0}$ and deep handlers	35.30
$SH (-)$ , $SD (-)$	named PPS syntax translations between ${control}_{0}$ and shallow handlers	35.40
$e ⟶_{i} e^{'}$	contraction closed by arbitrary one-hole term contexts	35.30
$wit$ , $prf$ , ${callcc}_{k}$	hypothetical CBN strong projections and captured-context form	35.41