Effect-capability signatures, translations, and metatheorems

System $\mathsf{Xi}$ interface

Fix the operation signature $\mathrm{\Omega }(F)={\tau }_1\to {\tau }_0$; it is suppressed from every judgment below, and $\mathrm{\Delta }(f)$ is rightmost lookup. The source interface consists of $$\mathrm{\Gamma }⊢e:\tau ,\mathrm{\Gamma }\mid \mathrm{\Delta }\mid \varnothing ⊢b:\sigma ,\mathrm{\Gamma }\mid \mathrm{\Delta }\mid \varnothing ⊢s:\tau .$$ The runtime interface replaces the empty label context by a finite $\mathrm{\Xi }$. Runtime labels have answer types, capabilities have block type ${\tau }_1\to {\tau }_0$, and delimiters bind one fresh label. Runtime configurations are derivation indexed: a generated capability retains the outer derivation of its handler body, and the displayed extrinsic X-Cap rule decomposes the ordered allocation stack as ${\mathrm{\Xi }}_0,\ell :\tau ,{\mathrm{\Xi }}_{+}$ and types that body under its exact birth prefix ${\mathrm{\Xi }}_0$. Block substitutions on runtime derivations must respect these restricted occurrence contexts; crossed later delimiters remain in the reified continuation, not in the stored clause. Reduction is $s⟶s^{\prime }$, generated by the rules in subappendix A.29 and closed under the displayed evaluation contexts. Generatedness is the reachability predicate ${\mathsf{Gen}}_{\mathrm{\Omega }}(s)$, and lemma 32.4 preserves it together with scope respect across every reduction step.

The local proof chain is $$\begin{array}{c}\text{weakening and substitution}\\ \Downarrow \\ \text{canonical forms}\\ \Downarrow \\ \text{progress and preservation}\\ \Downarrow \\ \text{absence of reachable undelimited capability states}.\end{array}$$ The conclusion is only the printed System-$\mathsf{Xi}$ safety consequence. It is not the Effekt source theorem, abstraction safety, noninterference, or a theorem about the full implementation.

The named Effekt-to-System-$\mathsf{Xi}$ translation

Fix a canonical order on finite Effekt sets. The source name classes for values, ordinary blocks, and operations are pairwise disjoint, and target block-context lookup is rightmost so the capability introduced by a handler shadows an outer same-operation capability only in its handled premise. If $\mathrm{\Sigma }(F)={\tau }_1\to {\tau }_0$, define $${\mathsf{CapOp}}_{\mathrm{\Sigma }}(F)={\tau }_1\to {\tau }_0.$$ For $\overline{F}=F_1,\dots ,F_n$, abbreviate $$\overline{{\mathsf{CapOp}}_{\mathrm{\Sigma }}(\overline{F})}={\mathsf{CapOp}}_{\mathrm{\Sigma }}(F_1),\dots ,{\mathsf{CapOp}}_{\mathrm{\Sigma }}(F_n).$$ Then Extend $\mathsf{CapTy}$ pointwise to $\mathrm{\Delta }$. The statement map is directed by the source typing derivation: $\mathrm{\Sigma }$ supplies operation types, and the current $\mathrm{\Delta }$ supplies the ordered capability list used at a block call. The short clauses are The two binding clauses are and The call clause takes $\overline{F}$ from the declared source block type. Operation declarations disappear; handler translation binds the capability and resumption explicitly. In the handler proof, the common outer target context is $${\mathsf{CapTy}}_{\mathrm{\Sigma }}(\mathrm{\Delta }),{\mathsf{CapEff}}_{\mathrm{\Sigma }}((\epsilon \setminus \{F\})\cup {\epsilon }_h).$$ Its handled premise receives a terminal binding for $F$, which shadows any outer $F$ required by ${\epsilon }_h$; the clause sees the unextended outer context. This is the exact target counterpart of source effect subtraction. The theorem interface is $$\begin{array}{c}\mathrm{\Gamma }\mid \mathrm{\Delta }\mid \mathrm{\Sigma }⊢s:\tau \mid \epsilon \\ ⟹\\ \mathrm{\Gamma }\mid {\mathsf{CapTy}}_{\mathrm{\Sigma }}(\mathrm{\Delta }),{\mathsf{CapEff}}_{\mathrm{\Sigma }}(\epsilon )\mid \varnothing ⊢{\mathsf{CapStmt}}_{\mathrm{\Sigma },\mathrm{\Delta }}(s):\tau .\end{array}$$ The proof is theorem 32.15. Combining it with System-$\mathsf{Xi}$ safety gives the selected Effekt effect-safety corollary, not a new System-$\mathsf{Xi}$ theorem.

Tunnelling logical-relation interface

The selected source and dynamic interfaces are $$\mathrm{\Delta }\mid P\mid \mathrm{\Xi }⊢T\mathsf{type},\mathrm{\Delta }\mid P\mid \mathrm{\Xi }⊢e\mathsf{effects},$$ $$\mathrm{\Delta }\mid P\mid \mathrm{\Gamma }\mid \mathrm{\Xi }⊢t:[T{]}_e,\mathrm{\Delta }\mid P\mid \mathrm{\Gamma }\mid \mathrm{\Xi }⊢h:\mathsf{F}\mid e,t⟶t^{\prime }.$$ The first two judgments and the ordinary typing rules are the chapter’s exact closure around the four characteristic rules printed in Figure 10. Appendix A.1 of Cornell technical report 1813/60202 supplies the common-effect T-App/T-Let rules, the type and effect preorders, and T-Sub. Appendix B supplies Compatibility Lemmas 7–19 for the rules it enumerates [ZM19b]; the chapter separately proves the omitted T-Let case by evaluation-context composition. Union-effect forms are derived by subsumption to a common join. These results remain theorems about the tunnelling calculus, not about a translation to System $\mathsf{Xi}$.

The explicit label parameter is a finite well-formed context $\mathrm{\Xi }$. Every context extension binds a fresh name; in particular T-Down requires both $\ell \notin \mathrm{dom}(\mathrm{\Xi })$ before extending $\mathrm{\Xi }$ and $\ell \notin \mathrm{fl}(T,\overline{e})$ before discharging the delimiter. The numerical step index is hidden by the later modality. The tunnelling relation does not quantify over a separate order of future label contexts. Closing environments have the shapes The semantic signature is $$\mathcal{W},\mathcal{O},\mathcal{T},\mathcal{K},\mathcal{S},\mathcal{V},\mathcal{H},\mathcal{U},$$ with open lifting by the environments above. The compatibility lemmas state that every typing rule preserves ${⪯}_{\mathsf{log}}$, and together establish the fundamental property. The imported boundary is Theorems 1–3 of [ZM19a]: parametricity (the fundamental property), closed type safety, and logical-refinement soundness for the tunnelling calculus, with the report supplying the complete rule and compatibility boundary [ZM19b]. No System-$\mathsf{Xi}$ translation is part of this interface.

Olaf optional boundary

Olaf uses $$\mathrm{\Delta }\mid \mathrm{\Theta }\mid \mathrm{\Gamma }\mid \mathrm{\Xi }⊢t:[\tau {]}_c,L;t⟶L^{\prime };t^{\prime }.$$ Its new invariant is that lifetime effects occur in effect sequences and its continuation types record effects on both sides of control transfer. Assuming $\mathrm{\Xi }$ and $\mathrm{\Gamma }$ are well formed, the imported results are Theorems 1–3 of [ZSM20]: parametricity, closed empty-effect type safety, and logical-refinement soundness for Olaf. They do not add bidirectional operations to the preceding calculi or imply linear resumptions.

Source-bounded comparison cards

The control-flow linearity card uses the local occurrence predicate $$\mathsf{uses}(r,M)\le q$$ only to distinguish zero, one, and multiple syntactic resumption uses. It imports no theorem: Tang et al.’s soundness results require their full qualified type system, constraint entailment, and operational semantics [THLM24].

White’s locality card fixes the dependent context restriction $y(\mathrm{\Sigma })$ and box introduction rule of §3.2, Figure 2, pp. 12–13; the reflection card fixes $W_{\mathrm{\Sigma }}(\tau )$, $\mathsf{reify}$, and $\mathsf{reflect}$ from §3.4, Figure 4, pp. 14–15 [Whi26]. The semantic comparison in §4.8, p. 23 belongs only to that calculus. These cards import definitions and rules, not a System-$\mathsf{Xi}$, Effekt, tunnelling, or Olaf theorem.

Metatheorem and evidence ledger