Modal-effect signatures and preservation ledger

Target interface

The target is the parameterized calculus $\mathsf{Met}[\mathcal{T}]$, not METL and not the earlier contextual-modal calculus. Its signature is $$\begin{array}{c}\mathrm{\Gamma }⊢D:\mathsf{Eff},D{\equiv }_{\mathcal{T}}{D}^{\prime },E{⪯}_{\mathsf{e}}F,\\ \mathrm{\Gamma }⊢A{\equiv }_{\mathsf{Met}}B,\mathrm{\Gamma }⊢\mu \Rightarrow \nu @F,\\ \mathrm{\Omega }\mid \mathrm{\Gamma }⊢M:A@E,(M;\mathrm{\Omega })⟶(N;{\mathrm{\Omega }}^{\prime }).\end{array}$$ The two validity assumptions are $$E{⪯}_{\mathsf{e}}\varnothing \Rightarrow E=\varnothing ,\ell {⪯}_{\mathsf{e}}{\ell }^{\prime },E\wedge \ell \ne {\ell }^{\prime }\Rightarrow \ell {⪯}_{\mathsf{e}}E.$$ Under these assumptions, the imported target endpoints are progress and subject reduction for $\mathsf{Met}[\mathcal{T}]$. Progress permits a normal unhandled request exactly when its label occurs in the displayed ambient effect context. Empty-effect safety is the corollary at $E=\varnothing$; termination is not a conclusion.

System $F_{\epsilon }$ encoding interface

The source judgments are $\mathrm{\Gamma }{⊢}_{v}V:A$ and $\mathrm{\Gamma }{⊢}_{c}M:A!E$. The translation target is $\mathsf{Met}[{\mathcal{R}}_{\mathrm{sc}}]$, where scoped-row equivalence preserves multiplicity. The theorem interface is $$\begin{array}{c}\mathrm{\Gamma }{⊢}_{c}M:A!E\\ \Downarrow \\ ⟨⟨\mathrm{\Gamma }⟩{⟩}_{\mathsf{r}}⊢⟨⟨M⟩{⟩}_{\mathsf{r}}:⟨⟨A⟩{⟩}_{\mathsf{r}}@⟨⟨E⟩{⟩}_{\mathsf{r}},\end{array}M⟶N⟹⟨⟨M⟩{⟩}_{\mathsf{r}}{⟶}^{\ast }⟨⟨N⟩{⟩}_{\mathsf{r}}.$$ The second conclusion is a forward multi-step simulation for one typed source step. It is not reflection, full abstraction, adequacy, or an inverse.

System $C$ encoding interface

The source judgments distinguish values, blocks, and computations. The target is $\mathsf{Met}[\mathcal{S}]$, and the proof is simultaneous over $$\mathrm{\Gamma }{⊢}_{v}V:A,\mathrm{\Gamma }{⊢}_{b}P:T\mid C,\mathrm{\Gamma }{⊢}_{c}M:A\mid C.$$ The computation endpoint is $$\mathrm{\Gamma }{⊢}_{c}M:A\mid C⟹⟨⟨\mathrm{\Gamma }⟩{⟩}_{\mathsf{c}}⊢⟨⟨M⟩{⟩}_{\mathsf{c}}:⟨⟨A⟩{⟩}_{\mathsf{c}}@⟨⟨C⟩{⟩}_{\mathsf{c}}.$$ For a well-typed source configuration step, $$(M;\mathrm{\Omega })⟶(N;{\mathrm{\Omega }}^{\prime })⟹(⟨⟨M⟩{⟩}_{\mathsf{c}};⟨⟨\mathrm{\Omega }⟩{⟩}_{\mathsf{c}}){⟶}^{\ast }(⟨⟨N⟩{⟩}_{\mathsf{c}};⟨⟨{\mathrm{\Omega }}^{\prime }⟩{⟩}_{\mathsf{c}}).$$ Fresh local-label generation and the block/capability substitution lemma are part of this endpoint. It neither proves a theorem about the full Effekt implementation nor removes System $C$’s second-class restriction.

Evidence ledger

The exact imported endpoints are Theorems 3.7–3.8 (§3.7, p. 18), Theorems 4.1–4.2 (§4.2, p. 20), and Theorems 5.1–5.2 (§5.2, p. 23) of Tang and Lindley [TL26]; the target-design and METL-artifact boundary is Tang et al. [TWD^+25]. The two imported encoding proofs are independent. Their common target is a span, not a triangle or an equivalence.