Chapter 34Optional

Lexical Effect Handlers and Direct Compilation

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

The wrong handler on the right stack

An operation name does not identify a lexical handler instance. Consider two handlers for one operation $ask$ : the outer instance returns $7$ , and the inner instance returns $9$ . A function is defined while only the outer instance is in scope: $\begin{aligned} with h_{o u t} = handler (ask \mapsto 7) in \\ let f = λ () . raise h_{o u t} ask () in \\ with h_{i n} = handler (ask \mapsto 9) in f () . \end{aligned}$ Lexical resolution records $h_{o u t}$ at the raise site, so the result is $7$ . A runtime that searches only for the nearest frame named $ask$ selects $h_{i n}$ and returns $9$ . Both handlers are live. The failure is loss of binding identity, not absence of a handler.

Definition 34.1 — Name search and identity search ¶

Let a runtime stack be a finite sequence of frames, written from innermost to outermost. A handler frame has the form $hdl (L, F, c)$ , where $L$ is a runtime handler identity, $F$ is an operation name, and $c$ is its clause. Define $\begin{aligned} findName (F, S) & : = the first hdl (L, F, c) in S, \\ findId (L, S) & : = the first hdl (L, F, c) in S . \end{aligned}$ Both functions are partial. Lexical handling uses $findId$ after the source binder has supplied $L$ ; dynamic name search uses $findName$ .

Referenced from 3 locations

Lexical Effect Handlers and Direct Compilation

For $S = hdl (L_{i n}, ask, 9) :: call (f) :: hdl (L_{o u t}, ask, 7) :: ϵ,$ the two searches calculate to $\begin{aligned} findName (ask, S) & = hdl (L_{i n}, ask, 9), \\ findId (L_{o u t}, S) & = hdl (L_{o u t}, ask, 7) . \end{aligned}$ The compiled program must preserve the second result even when the target represents both handler frames by ordinary stack data.

Exercise 34.1 ¶

★☆☆ Insert a third $ask$ handler between $call (f)$ and the outer handler in $S$ . Calculate both searches, and state the least datum a compiler must preserve to keep the result $7$ .

Referenced from 3 locations

The untyped Lexa source machine

The direct compiler begins below typing. This matters: the first preservation theorem is a theorem about observable behavior of an untyped intermediate language, not a source type-safety theorem.

Definition 34.2 — The 2024 Lexa system card ¶

Lexa is the A-normal, closure-converted, hoisted intermediate language of Ma, Ge, Lee, and Zhang. Code labels $P$ are static; data labels $L$ are generated at run time. Each formal handler has one unary operation, and a captured resumption is dynamically one-shot. Programs contain closed top-level functions, while handler code and handled code receive an explicit closure environment. The calculus is untyped. Its operational semantics is the abstract machine in [MGLZ24].

Referenced from 4 locations

The complete Lexa source-machine rules are collected in subappendix A.31; the calculations below name the rule used at each transition.

The value and term grammar is $\begin{array}{rcl} c & ::= & i ∣ P ∣ ns, \\ v & ::= & x ∣ c, \\ e & ::= & v ∣ v_{1} + v_{2} ∣ newref (\bar{v}) ∣ π_{i} (v) ∣ v_{1} [i] \leftarrow v_{2} ∣ v_{0} (\bar{v}) \\ ∣ handle P_{b} with P_{o} under v ∣ raise v_{1} v_{2} ∣ resume v_{1} v_{2} ∣ exit v, \\ t & ::= & v end ∣ let x = e in t, \\ G & ::= & letrec P_{1} = λ {\bar{x}}_{1} . t_{1}, \dots, P_{n} = λ {\bar{x}}_{n} . t_{n} . \end{array}$ The constant $ns$ is a nonsense word used to invalidate a consumed resumption. It is not a source exception.

Definition 34.3 — Lexa configurations ¶

A Lexa configuration is $⟨ M ∣ H ∣ K ∣ E ∣ t ⟩ .$ The code memory $M$ maps code labels to closed functions. The heap $H$ maps data labels to tuples or captured contexts $cont (K)$ . A local environment $E$ maps variables to values. Frames and contexts are $\begin{aligned} F & ::= (E, let x = [] in t) ∣ hdl (L, P_{o}, L_{e n v}, []), \\ K & ::= ϵ ∣ K \cdot F . \end{aligned}$ Write $C ⟶ C^{'}$ for one Lexa-machine transition and $C ⟶^{*} C^{'}$ for its reflexive–transitive closure.

Referenced from 2 locations

Lexical Effect Handlers and Direct Compilation

Installing a handler generates its identity. Suppressing unchanged $M, H$ , the root has the form $\begin{aligned} ⟨ K ∣ E ∣ let x = handle P_{b} with P_{o} under v_{e n v} in t ⟩ \\ \overset{L - H a n d l e}{⟶} ⟨ \begin{matrix} K \cdot (E, let x = [] in t) \cdot hdl (L, P_{o}, L_{e n v}, []) \\ ∣ [x_{e n v} \mapsto L_{e n v}, x_{h d l} \mapsto L] ∣ t_{b} \end{matrix} ⟩, \end{aligned}$ where $L$ is fresh, $M (P_{b}) = λ (x_{e n v}, x_{h d l}) . t_{b}$ , and $E (v_{e n v}) = L_{e n v}$ .

In the next two roots only the unchanged code memory $M$ is suppressed. Suppose the active context uniquely factors as $K \cdot hdl (L, P_{o}, L_{e n v}, []) \cdot K^{'} .$ Raising to $L$ captures the suffix through the suspended let frame: $\begin{aligned} ⟨ H ∣ K \cdot hdl (L, P_{o}, L_{e n v}, []) \cdot K^{'} ∣ E ∣ let x = raise L v in t ⟩ \\ \overset{L - R a i s e}{⟶} ⟨ \begin{matrix} H [L_{k} \mapsto cont (hdl (L, P_{o}, L_{e n v}, []) \cdot K^{'} \cdot (E, let x = [] in t))] \\ ∣ K ∣ E_{o} ∣ t_{o} \end{matrix} ⟩, \end{aligned}$ where $L_{k}$ is fresh, $M (P_{o}) = λ (x_{e n v}, y, k) . t_{o}$ , and $E_{o} = [x_{e n v} \mapsto L_{e n v}, y \mapsto E (v), k \mapsto L_{k}]$ . The factorization is by identity $L$ . A nearer frame with the same operation name but a different identity remains inside $K^{'}$ and is captured rather than selected.

If $H (L_{k}) = cont (K^{'} \cdot (E^{'}, let x^{'} = [] in t^{'})),$ then resumption reinstalls those frames and writes $ns$ at $L_{k}$ : $\begin{aligned} ⟨ H ∣ K ∣ E ∣ let x = resume L_{k} v in t ⟩ \\ \overset{L - R e s u m e}{⟶} ⟨ H [L_{k} \mapsto ns] ∣ K \cdot (E, let x = [] in t) \cdot K^{'} ∣ E^{'} [x^{'} \mapsto E (v)] ∣ t^{'} ⟩ . \end{aligned}$ The update makes a second resume stuck in this untyped formal calculus. The implementation has a separately stated, limited multishot extension; it is not part of the 2024 theorem.

Example 34.4 — The inner handler is captured ¶

Let the stack $S$ from definition 34.1 be the handler-bearing part of $K$ , and raise to $L_{o u t}$ . Rule L-Raise factors at the outer frame. The captured suffix therefore begins with the inner frame: $K^{'} = hdl (L_{i n}, ask, 9) \cdot call (f) \cdot ϵ .$ The selected code is the clause stored at $L_{o u t}$ , so it returns $7$ . If that clause resumes, the inner frame becomes active again. Lexical selection and deep resumption are therefore separate actions.

Referenced from 2 locations

Lexical Effect Handlers and Direct Compilation

Exercise 34.2 ¶

★☆☆ Starting from a heap with $H (L_{k}) = cont (K^{'})$ , apply L-Resume twice to the same $L_{k}$ . State the heap after the first step and identify the failed premise at the second attempt.

Referenced from 3 locations

Salt: ordinary instructions and three trampolines

The target does not acquire a distinguished handler instruction. Salt is an assembly-like machine with heap-allocated stacks. Its words, operands, and instruction sequences are $\begin{array}{rcl} ℓ & ::= & L ∣ P ∣ next (ℓ), \\ w & ::= & ℓ ∣ i ∣ ns, \\ o & ::= & r ∣ w, \\ ι & ::= & add r, o ∣ mkstk r ∣ salloc i ∣ sfree i ∣ malloc r_{d}, i \\ ∣ mov r_{d}, o ∣ load r_{d}, [r_{s} + i] ∣ store [r_{d} + i], o ∣ push o ∣ pop r \\ ∣ call o ∣ jmp o ∣ return ∣ halt, \\ I & ::= & ϵ ∣ ι; I . \end{array}$ A Salt state is $⟨ M ∣ H ∣ R ⟩$ . Its register file has distinguished stack and instruction pointers $sp$ and $ip$ . If $H (L) = nil :: w_{1} :: \dots :: w_{m}$ , then $L^{m}$ names its top. In particular, $mov sp, L^{j}$ both changes stacks and truncates the selected stack above $L^{j}$ .

Definition 34.5 — The 2024 Salt target card ¶

The target of the published translation is exactly the Salt machine just displayed. It has general heap, register, call, return, and stack operations; it has no handler-specific opcode. The translated program adds code labels $P_{handle}$ , $P_{handle_special}$ , $P_{raise}$ , and $P_{resume}$ . The machine and the complete translation are fixed by [MGLZ24].

Referenced from 4 locations

For an ordinary handler annotation $A$ , abbreviate the displayed semantic translation by $T_{Γ} (e) : = T_{Lexa \to Salt} (e)_{Γ}$ and its register-valued form by $T_{Γ}^{r} (v) : = T_{Lexa \to Salt} (v)_{Γ}^{r}$ . The three source forms compile at their redexes as follows: $\begin{aligned} T_{Γ} (handle P_{b} with P_{o} under v_{e n v}) & = T_{Γ}^{r_{4}} (A); T_{Γ}^{r_{3}} (v_{e n v}); \\ mov r_{2}, P_{o}; mov r_{1}, P_{b}; call P_{handle}, \\ T_{Γ} (raise v_{1} v_{2}) & = T_{Γ}^{r_{2}} (v_{2}); T_{Γ}^{r_{1}} (v_{1}); call P_{raise}, \\ T_{Γ} (resume v_{1} v_{2}) & = T_{Γ}^{r_{2}} (v_{2}); T_{Γ}^{r_{1}} (v_{1}); call P_{resume} . \end{aligned}$ These equations expose where lexical identity travels: $r_{1}$ contains an exchanger address for raise and a one-cell resumption object for resume. A trampoline is the short target routine that switches stacks around a handle, raise, or resume action.

The handle trampoline saves the parent $sp$ , allocates a new stack, and pushes a four-word header $P_{o} :: L_{e n v} :: A :: ℓ_{e x c h} .$ The exchanger initially points to the parent stack. Its body call therefore runs on a fresh stack whose header remembers exactly which operation code and closure environment belong to this handler instance. On normal return the trampoline pops the exchanged parent pointer, removes the other three header words, switches back, and returns.

Proposition 34.6 — The exchanger invariant ¶

At each reachable translated handler header, the exchanger contains either the top of its parent stack or the top of the suspended resumption stack. The raise and resume trampolines exchange these alternatives without copying the captured frames.

Referenced from 2 locations

Lexical Effect Handlers and Direct Compilation

Proof of Proposition 34.6 — The exchanger invariant

Proof. Immediately after $P_{handle}$ constructs the header, the fourth word is the saved parent $sp$ . On raise, $P_{raise}$ loads that word, stores the current $sp$ there, and moves the loaded word into $sp$ . Thus the header now points to the suspended stack while execution has returned to the handler stack. The fresh resumption object points to the same exchanger. On resume, $P_{resume}$ loads the exchanger through that object, loads its saved stack top, stores the current handler-stack top back into the exchanger, and switches to the loaded top. These are the only instructions that alter an exchanger after construction, so induction over target steps establishes the alternatives. ◻

The one-shot update is equally concrete. The first two resume instructions are $load r_{3}, [r_{1}]; store [r_{1}], ns .$ Only then does the trampoline dereference the exchanger in $r_{3}$ and switch stacks. A second use reads $ns$ , matching the failed premise of the Lexa L-Resume rule.

Exercise 34.3 ¶

★★☆ Let a handler header’s exchanger contain $L_{p}^{m}$ , while the active handled stack has top $L_{h}^{n}$ . Trace the exchanger and $sp$ through one raise and one resume. State which location the resumption object contains after raise and why the second resume cannot reach a well-formed exchanger.

Referenced from 3 locations

What the 2024 theorem proves

For either machine, a program behavior is $B ::= converge (i) ∣ stuck ∣ diverge .$ Convergence reaches the language’s designated final state with integer $i$ ; stuckness reaches a nonfinal state with no successor; divergence is an infinite reduction. Semantic preservation deliberately excludes stuck source programs: $G ⇓ B \land B \neq stuck ⟹ T_{Lexa \to Salt} (G) ⇓ B .$

Lemma 34.7 — Positive simulation criterion ¶

Let $R$ relate source and target states. Suppose initial states are related, related final states have the same integer, and $C_{s} R C_{t} C_{s} ⟶ C_{s}^{'} ⟹ \exists C_{t}^{'} . C_{t} ⟶^{+} C_{t}^{'} \land C_{s}^{'} R C_{t}^{'} .$ Then the translation preserves convergence and divergence.

Referenced from 4 locations

Lexical Effect Handlers and Direct Compilation

Proof of Lemma 34.7 — Positive simulation criterion

Proof. For a finite source run, induction concatenates the nonempty target segments. The final-state premise supplies the same integer. For an infinite source run, repeatedly choose the target segment supplied by simulation. Every segment is nonempty, so their concatenation is an infinite target run. The claim says nothing about source stuckness: a stuck source state supplies no step to simulate. ◻

Theorem 34.8 — Lexa-to-Salt semantic preservation ¶

The 2024 translation from the untyped Lexa program signature of definition 34.2 to the Salt signature of definition 34.5 preserves every non-stuck observable behavior.

Referenced from 5 locations

Lexical Effect Handlers and Direct Compilation

Proof of Theorem 34.8 — Lexa-to-Salt semantic preservation

Proof boundary. This is the published theorem of [MGLZ24]. Its configuration relation simultaneously relates source instruction position, evaluation context and environment, heaps and captured resumptions, and code memory. The source and target initial states are related; related final states expose the same integer; and every Lexa step is matched by one or more Salt steps. Lemma 34.7 then yields the stated behaviors. The appendix proof is imported at those exact signatures; it is not reproduced as a new type theorem or as correctness of the closure-conversion, LLVM, garbage collector, or native-code pipeline. ◻

Exercise 34.4 ¶

★★☆ For each of the following claims, say whether theorem 34.8 proves it: preservation of a terminating integer result; preservation of divergence; reflection of target stuckness; source type safety; correctness of LLVM code generation. Cite the premise or the missing signature in each case.

Referenced from 3 locations

A typed zero-mainline-overhead refinement

The 2025 development is not a typed retrofit of the preceding theorem. It uses a new source calculus $SL$ , a new target calculus $TL$ , and a distinct simulation relation.

Definition 34.9 — The 2025 SL/TL system card ¶

In $SL$ , handlers bind generative lexical labels, functions may abstract over capability variables and label variables, and applications instantiate both. Types include $τ ::= unit ∣ \forall [\bar{α}; \bar{ℓ} : \bar{F}] . (\bar{τ}) \overset{T}{\to} τ ∣ {cont}^{T} (τ, τ),$ where $T$ records a captured capability variable or labels. Typing and translation have the joint shape $Θ ∣ Δ ∣ Σ ∣ Γ ⊢ t : τ ⇝ \underset{―}{t} .$ The target $TL$ erases source labels and capabilities from terms; a raise carries a clue, and call and handler frames carry statically derived call-site metadata used only while searching. This is the system of [MGJZ25].

Referenced from 2 locations

Lexical Effect Handlers and Direct Compilation

A target clue is $⟨ q, F ⟩$ , with $q ::= \hat{i} ∣ \overset{˚}{i} ∣ \infty .$ Here $\hat{i}$ follows the callee’s $i$ -th label parameter, $\overset{˚}{i}$ follows its $i$ -th capability parameter, and $\infty$ searches a captured label of effect $F$ . Call-site metadata has the form $H = T_{0}; T; \bar{ℓ} : \bar{F},$ recording the callee’s capture set, capability instantiations, and label instantiations. The partial hopper function ${hopper}_{H}$ rewrites a clue when search crosses the call frame.

For example, if the callee’s label parameter $ℓ_{i} : F$ is instantiated by the caller’s label index $\hat{j}$ , then ${hopper}_{H} (⟨ \hat{i}, F ⟩) = ⟨ \hat{j}, F ⟩ .$ If a capability instantiation lists a unique label index with effect name $F$ , a clue $⟨ \overset{˚}{i}, F ⟩$ becomes that label clue. If the matching label is captured, $⟨ \infty, F ⟩$ is resolved from the callee’s recorded capture set. The source typing rules require nonambiguity—labels in the relevant capture set have distinct effect names—and nontrivial capability instantiations. Those premises make the needed hopper cases single-valued; the function is not claimed total on arbitrary metadata.

Example 34.10 — Two hops, one lexical identity ¶

Suppose $g$ ’s label parameter $ℓ_{0} : F$ is instantiated at one call site by its caller’s $ℓ_{2} : F$ , and that caller’s $ℓ_{2}$ is instantiated one frame higher by $ℓ_{1} : F$ . Search starts with $C_{0} = ⟨ \hat{0}, F ⟩$ . Put $C_{1} = ⟨ \hat{2}, F ⟩$ and $C_{2} = ⟨ \hat{1}, F ⟩$ . The two hoppers calculate ${hopper}_{H_{1}} (C_{0}) = C_{1}, {hopper}_{H_{2}} (C_{1}) = C_{2} .$ A nearer handler for a different label of the same effect name is skipped: the clue records provenance through the call sites, rather than the nearest-named $F$ . At the installing frame the index becomes $\hat{0}$ , the distinguished signal that this is the selected handler.

Referenced from 2 locations

Lexical Effect Handlers and Direct Compilation

Theorem 34.11 — SL-to-TL simulation and terminating preservation ¶

If a well-typed $SL$ configuration $M_{s}$ is related to a $TL$ configuration $M_{t}$ , then each source step is matched by zero or more target steps to a related configuration. Hence, if a closed joint judgment translates $t$ to $\underset{―}{t}$ and source evaluation terminates at $v$ , target evaluation terminates at a translated value $\underset{―}{v}$ .

Referenced from 4 locations

Proof of Theorem 34.11 — SL-to-TL simulation and terminating preservation

Proof boundary. These are Theorem 1 and Corollary 1 of [MGJZ25]. The relation is stated on a typing-enriched source ${SL}^{*}$ ; promises relate static source parameters to target indices, while evidence relates run-time source labels to target clues. The paper’s displayed source typing is deliberately described as strengthening previously sound systems and does not publish a new independent SL type-safety theorem in the main development. We import only the stated simulation and terminating corollary. ◻

Proposition 34.12 — The exact zero-mainline property ¶

For code translated by the 2025 compiler, a mainline call—one executed before any raise begins handler search—neither creates nor passes a reified handler identity and does not run handler search. The compiled implementation places hopper data in a static table keyed by return address; it does not construct or consult that data on mainline calls. Stackwalking and hopper lookup begin only after a raise.

Referenced from 3 locations

Proof of Proposition 34.12 — The exact zero-mainline property

Proof. Inspection of the translation erases source label and capability binders and their application arguments. A target raise retains only its initial clue. The target semantics annotates call frames with $H$ in order to state search, while the implementation recovers the corresponding hopper from the return address and a global data-section table. Thus the metadata is static program data, not a mainline stack or register value. This is a syntactic and implementation-layout statement. The cited work supplies measurements, not a cost semantics, so zero is not a proved equation between running times. ◻

Exercise 34.5 ¶

★★☆ Let a callee have label parameters $ℓ_{0} : F, ℓ_{1} : G$ , instantiated by the caller’s indices $\hat{3}, \hat{0}$ . Calculate the hopper results for $⟨ \hat{0}, F ⟩$ and $⟨ \hat{1}, G ⟩$ . Then duplicate effect name $F$ inside the relevant capture set and explain which nonambiguity premise, rather than an operational rule, rejects the metadata.

Referenced from 3 locations

Exercise 34.6 ¶

★★☆ Separate the following into a proved syntactic property, a proved semantic property, and engineering evidence: no reified handler identities on mainline paths; terminating SL-to-TL preservation; benchmark speedups for effect-infrequent programs. Explain why none alone establishes a formal constant-factor cost theorem.

Referenced from 3 locations

Generalised continuations for deep and shallow handlers

Lexical binding is not the only axis in the matrix. Hillerström, Lindley, and Atkey give one calculus in which deep and shallow handlers can be compared without identifying them.

Definition 34.13 — The λ ^ and CPS card ¶

The source $λ^{†}$ is fine-grain call-by-value with value types, computation types $A! E$ , row-polymorphic effect types, and handler types $C \Rightarrow_{δ} D, δ \in {deep, †} .$ Its characteristic terms are $return V$ , $let x \leftarrow M in N$ , $do ℓ V$ , and ${handle}^{δ} M with H$ . A deep resumption reinstalls its handler; a shallow resumption does not.

The target of the higher-order CPS translation is the untyped two-level calculus of Figure 9 in [HLA20]. Dynamic terms include two-argument application $U @ V @ W$ , $app V W$ , and $let r = {res}^{δ} V in N$ . A generalised continuation is a nonempty stack $κ = ⟨ θ, ⟨ χ_{r e t}, χ_{o p s} ⟩ ⟩ :: κ^{'},$ whose top frame separates a pure-frame stack $θ$ , a return clause $χ_{r e t}$ , and an operation dispatcher $χ_{o p s}$ . The translation is higher-order: static abstractions and applications are reduced while translating, while underlined dynamic constructs remain target code.

Referenced from 3 locations

Lexical Effect Handlers and Direct Compilation

Writing $C [-]$ for the Figure 10 higher-order translation, its load-bearing clauses are $\begin{aligned} C [return V] & = λ κ . app (↓ κ) C [V], \\ C [{handle}^{δ} M with H] & = λ κ . C [M] @ (⟨ ↑ [], C_{δ} [H] ⟩ :: κ) . \end{aligned}$ The operation clause projects the top $χ_{o p s}$ , passes it the operation label, payload, and reversed resumption stack, then passes the remaining $κ$ . The deep $res$ root prepends the captured pure frames to the current top frame, thereby retaining its handler. The shallow ${res}^{†}$ root instead restores the captured pure and handler frames ahead of the caller’s continuation; it does not reinstall the handler that captured the operation. This is the exact semantic difference, not a flag erased from the proof.

Theorem 34.14 — The generalised-continuation endpoints ¶

At the card of definition 34.13:

$λ^{†}$ has type soundness;
the higher-order CPS translation positively simulates every source step, has a backward simulation for terminating target runs, and therefore preserves and reflects termination at translated values;
the deep-to-shallow and shallow-to-deep encodings each have their own type and simulation results; and
parameterised handlers locally translate to ordinary deep handlers.

Referenced from 4 locations

Proof of Theorem 34.14 — The generalised-continuation endpoints

Proof boundary. These are, respectively, Theorem 1 (§3.4), Theorem 7 and Lemma 7 with Corollary 1 (§5.4.4), Theorems 2–3 (§4.1) and Theorems 4–5 (§4.2), and Theorem 9 (§7) of [HLA20]. The CPS target is untyped, so item 2 is not a target type-preservation theorem. Parameterised handlers extend a continuation frame with a state component and their CPS translation threads it; the paper explicitly notes that this is not a zero-cost CPS translation for the other variants. None of these statements mentions lexical handler identity, Lexa, Salt, SL, or TL. ◻

Exercise 34.7 ¶

★★☆ An operation is captured under a handler $H$ with pure suffix $θ$ . Describe the continuation installed by a deep resume and by a shallow resume. Which one can handle a second occurrence of the same operation after resumption? Explain why theorem 34.14 supplies two simulation cases rather than an equation identifying the resumptions.

Referenced from 3 locations

A typed CPS route, kept separate

There is also a higher-level typed compiler. Schuster, Brachthäuser, and Ostermann translate their lexical-handler calculus $Λ_{cap}$ to pure System F [SBMO22]. Its region and capability discipline gives source progress and preservation; the typed CPS translation has a target-typing theorem and a source-to-target operational simulation. Precisely, source progress and preservation are Theorems 4–5, effect safety is Corollary 6, evidence correspondence is Corollary 7, translated-term typing is Theorem 8 in §4.1, simulation is Theorem 10 in §4.2, and evaluation is Corollary 11 of [SBMO22]. The target is System F, not Salt or $TL$ , and the source is neither the untyped Lexa IR nor 2025 $SL$ . Consequently these theorems do not fill a typing premise in theorem 34.8, and the Lexa-to-Salt theorem does not validate this CPS translation.

Three implementation choices

Once the theorem cards are fixed, the implementation trade-off is visible. Capability passing makes handler authority an explicit value, so ordinary calls transmit that value and a raise follows it directly. Tunnelling gives effect-polymorphic or parametric code an authority boundary that prevents an unrelated intermediate handler from intercepting the operation. Direct Lexa reifies a lexical handler instance by its stack address; ordinary execution passes the address, and raise reaches the instance in constant-time stack switching. Zero Lexa erases that run-time identity from mainline paths and reconstructs its provenance by stackwalking only when an effect is raised. The last two therefore optimize opposite frequency regimes; neither dominates without a workload and cost model.

Mechanism	Mainline datum	Raise action	Formal target	Proved boundary
Capability passing	capability	apply/follow value	source-specific	typing/translation card
Tunnelling	effect authority	cross oblivious code	source-specific	tunnelling card
Direct Lexa	stack address	switch at exchanger	Salt	non-stuck behavior
Zero Lexa	none dynamic	stackwalk hoppers	$TL$	typed simulation
Typed CPS	CPS capability	invoke continuation	System F	typing and simulation

Handler families and translation boundaries

Family
interface
here
boundary
Deep algebraic	handler reinstalled	$λ^{†}$ card	higher-order CPS; deep/shallow encoding
Shallow algebraic	handler not reinstalled	$λ^{†}$ card	higher-order CPS; deep/shallow encoding
Parameterized	handler state parameter	$λ^{†}$ extension	local translation to deep
Row-typed	effects tracked by rows	$λ^{†}$ card	higher-order CPS at that signature
Lexical, untyped	generative identity; one-shot	Lexa/Salt	behavior preservation
Lexical, typed	label/capability capture	SL/TL	typed simulation
Higher-order	operations accept computations	comparison only	none added
Lexical CPS	region/capability discipline	$Λ_{cap}$ /F	typed CPS simulation

The remaining none added entry is mathematical information. Deep versus shallow handling changes whether the handler surrounds a resumed computation. Parameterized handlers pass state through clauses; row types classify possible operations; higher-order signatures admit computations inside operation parameters. None of those choices follows merely from lexical binding. A generalized continuation translation or a typed CPS compiler must therefore state its own source grammar, target grammar, typing theorem, and simulation. The four frozen cards above provide no universal handler compiler.

Executable evidence and source boundary

The executable supplement checks the chapter’s finite calculations: name search versus identity search, exchanger selection, one-shot invalidation, two hopper rewrites, and absence of search instructions from a mainline trace. These tests are witness calculations for the displayed models. They do not rerun the native Lexa compiler or reproduce published benchmark tables. Appendix E records the frozen sources, toolchains, integrity pins, and reproduction boundary. The published measurements remain cited engineering evidence, kept separate from theorem 34.8, theorem 34.11.

This chapter used the extended 2024 operational account and proof, the 2025 typed zero-overhead account and its extended appendix, and the typed $Λ_{cap}$ -to-System-F development. It has not proved whole-compiler correctness, principal effect inference, a universal deep/shallow translation, or a cost theorem for every handler implementation.

Exercise 34.8 ¶

★★☆ Choose one row of section 34.9 whose translation entry is none added. List the four signatures that a new preservation theorem would have to fix before it could be compared with the Lexa-to-Salt theorem. Why is changing only the handler’s resumption convention already enough to invalidate a proof by citation?

Referenced from 3 locations

Suggested first pass.

Begin with exercise 34.9, exercise 34.10; continue with exercise 34.11; then use the cost model and executable project to test the implementation boundary. No problem in this optional seminar is a prerequisite for a later chapter.

Exercise 34.9 ¶

★★★ Formalize stacks as lists and prove: if handler identities are unique, the factorization at a requested identity is unique. Give a counterexample after identities are replaced by operation names. State precisely whether the failure is nonexistence or nonuniqueness.

Referenced from 4 locations

Exercise 34.10 ¶

★★★ Prove lemma 34.7 in full. Your divergence case must explain why a zero-step target match would be insufficient and why source stuckness is outside the conclusion.

Referenced from 4 locations

Exercise 34.11 ¶

★★★ Construct metadata for two labels of the same effect name reachable through one capability parameter. Show the two possible successor clues. Then strengthen the metadata judgment with the published nonambiguity condition and prove that the corresponding hopper case is a partial function.

Referenced from 4 locations

Exercise 34.12 ¶

★★☆ Design a two-parameter symbolic cost comparison. Let $n$ be the number of ordinary calls and $m$ the number of raises; charge direct Lexa $d$ per ordinary call and $r_{d}$ per raise, and zero Lexa $z$ per ordinary call and $r_{z} (h)$ for a raise crossing $h$ frames. Derive the inequality under which zero Lexa wins. Explain why this calculation is a model chosen for the exercise, not a theorem imported from benchmark measurements.

Referenced from 3 locations

Exercise 34.13 ¶

★★★ Practical project.lexical-handler-traces Implement the finite checker and trace generator from section 34.10. The oracle must distinguish nearest-name from requested-identity lookup, reject a consumed resumption, calculate two successive hopper clues, and certify that an effect-free mainline trace contains no handler search. Add two mutants: replace identity lookup by name lookup, and omit resumption invalidation. Each mutant must fail a named oracle. The mainline case checks membership in a hand-written instruction list; it is not a compiler-generated trace. Emit one named oracle result for each finite calculation so this boundary is inspectable. Appendix E records the commands, and appendix F gives the implementation stages.

Referenced from 4 locations