Lexical-handler compilation ledger

2024 source and target.

The source is the untyped, A-normal, closure-converted, hoisted Lexa calculus of definition 34.2; its formal handler has one unary operation and its resumptions are dynamically one-shot. The target is the Salt abstract machine of definition 34.5, with heap-allocated stacks and no handler-specific opcode. The translation adds four trampoline code labels.

2024 endpoint.

Initial and final configurations are related, final integers agree, and every Lexa step has a nonempty finite Salt simulation. Therefore $$G\Downarrow B\wedge B\ne \mathsf{stuck}⟹{\mathcal{T}}_{\mathsf{Lexa}\to \mathsf{Salt}}(G)\Downarrow B.$$ This is behavior preservation for the displayed untyped languages. It is not source type safety, stuckness preservation or reflection, whole-compiler correctness, or correctness of LLVM and native code.

2025 source and target.

The joint SL typing-and-translation signature is $$\mathrm{\Theta }\mid \mathrm{\Delta }\mid \mathrm{\Sigma }\mid \mathrm{\Gamma }⊢t:\tau ⇝\underset{―}{t}.$$ SL has generative labels, capability and label parameters, and capture annotations. TL erases dynamic handler identities and carries clues plus static call-site metadata for search. Its simulation relation uses the typing-enriched source ${\mathsf{SL}}^{\ast }$, promises, and run-time evidence.

2025 endpoint.

One well-typed SL configuration step is matched by zero or more TL steps to a related configuration. A closed well-typed SL program that terminates at a value translates to a TL program terminating at its related value. The zero-mainline conclusion is syntactic and implementation-layout evidence: ordinary paths do not create or pass handler identities or consult hopper data. The paper’s benchmark results are not a formal cost theorem.

Typed CPS endpoint.

The source is ${\mathrm{\Lambda }}_{\mathsf{cap}}$, the target is pure System F, and the imported results are source progress and preservation, translation typing, and operational simulation at that signature. No theorem is transferred between this card, untyped Lexa/Salt, and SL/TL.

Generalised-continuation endpoint.

The source is row-typed ${\lambda }^{†}$, with distinct deep and shallow handler types; the higher-order CPS target is an untyped two-level calculus whose continuation frames separate pure frames, a return clause, and an operation dispatcher. Source type soundness is Theorem 1. CPS simulation is Theorem 7, backward simulation is Lemma 7, and termination correspondence is Corollary 1. The two source-to-source translations have separate typing and simulation Theorems 2–5. Parameterised-to-deep simulation is Theorem 9. These are ${\lambda }^{†}$ results, not lexical-identity results.

The exact source locators are [MGLZ24], [MGJZ25], and [SBMO22]. The generalised-continuation endpoints are Theorems 1–9 at the subdivisions listed in theorem 34.14 of [HLA20].