Effect capabilities, explicit labels, and tunnelling

This appendix freezes the three independent calculi used by chapter 32. Identical letters in different cards do not identify judgments across cards.

System $\mathsf{Xi}$

The selected source and runtime syntax is The contexts and judgments are $$\begin{array}{c}\mathrm{\Gamma }::=\varnothing \mid \mathrm{\Gamma },x:\tau ,\mathrm{\Delta }::=\varnothing \mid \mathrm{\Delta },f:\sigma ,\mathrm{\Xi }::=\varnothing \mid \mathrm{\Xi },\ell :\tau ,\\ \mathrm{\Gamma }⊢e:\tau ,\mathrm{\Gamma }\mid \mathrm{\Delta }\mid \mathrm{\Xi }⊢b:\sigma ,\mathrm{\Gamma }\mid \mathrm{\Delta }\mid \mathrm{\Xi }⊢s:\tau .\end{array}$$ All judgments are relative to a fixed operation signature $\mathrm{\Omega }$, with $\mathrm{\Omega }(F)={\tau }_1\to {\tau }_0$. This arrow abbreviates the single-value, no-block-parameter type $(({\tau }_1),())\to {\tau }_0$; block-context lookup is rightmost. The selected pure fragment contains exactly unit, integer and Boolean constants and variables; its constant signature is $\mathcal{C}(())=1$, $\mathcal{C}(n)=\mathsf{Int}$, and $\mathcal{C}(\mathsf{true})=\mathcal{C}(\mathsf{false})=\mathsf{Bool}$. Value types contain no block type. Expressions contain no block variable or block abstraction. This syntactic separation is the second-class restriction.

The complete selected typing rules are

$x:\tau \in \mathrm{\Gamma }$

$\mathrm{\Gamma }⊢x:\tau$

$\mathcal{C}(v)=\tau$

$\mathrm{\Gamma }⊢v:\tau$

$\mathrm{\Delta }(f)=\sigma$

$\mathrm{\Gamma }\mid \mathrm{\Delta }\mid \mathrm{\Xi }⊢f:\sigma$

$\mathrm{\Gamma },\overline{x}:\overline{\tau }\mid \mathrm{\Delta },\overline{f}:\overline{\sigma }\mid \mathrm{\Xi }⊢s:\tau$

$\mathrm{\Gamma }\mid \mathrm{\Delta }\mid \mathrm{\Xi }⊢\{(\overline{x}:\overline{\tau },\overline{f}:\overline{\sigma })\Rightarrow s\}:(\overline{\tau },\overline{\sigma })\to \tau$

$\mathrm{\Gamma }⊢e:\tau$

$\mathrm{\Gamma }\mid \mathrm{\Delta }\mid \mathrm{\Xi }⊢e:\tau$

$\mathrm{\Gamma }\mid \mathrm{\Delta }\mid \mathrm{\Xi }⊢s_0:{\tau }_0$$\mathrm{\Gamma },x:{\tau }_0\mid \mathrm{\Delta }\mid \mathrm{\Xi }⊢s_1:{\tau }_1$

$\mathrm{\Gamma }\mid \mathrm{\Delta }\mid \mathrm{\Xi }⊢\mathsf{val}x=s_0;s_1:{\tau }_1$

$\mathrm{\Gamma }\mid \mathrm{\Delta }\mid \mathrm{\Xi }⊢b:\sigma$$\mathrm{\Gamma }\mid \mathrm{\Delta },f:\sigma \mid \mathrm{\Xi }⊢s:\tau$

$\mathrm{\Gamma }\mid \mathrm{\Delta }\mid \mathrm{\Xi }⊢\mathsf{def}f=b;s:\tau$

$\mathrm{\Gamma }\mid \mathrm{\Delta }\mid \mathrm{\Xi }⊢b:(\overline{\tau },\overline{\sigma })\to {\tau }_0$$(\mathrm{\Gamma }⊢e_i:{\tau }_i{)}_i$$(\mathrm{\Gamma }\mid \mathrm{\Delta }\mid \mathrm{\Xi }⊢b_j:{\sigma }_j{)}_j$

$\mathrm{\Gamma }\mid \mathrm{\Delta }\mid \mathrm{\Xi }⊢b(\overline{e},\overline{b}):{\tau }_0$

$\mathrm{\Omega }(F)={\tau }_1\to {\tau }_0$$\mathrm{\Gamma }\mid \mathrm{\Delta },F:{\tau }_1\to {\tau }_0\mid \mathrm{\Xi }⊢s:\tau$$\mathrm{\Gamma },x:{\tau }_1\mid \mathrm{\Delta },k:{\tau }_0\to \tau \mid \mathrm{\Xi }⊢s_h:\tau$

$\mathrm{\Gamma }\mid \mathrm{\Delta }\mid \mathrm{\Xi }⊢\mathsf{handle}\{F\Rightarrow s\}\mathsf{with}\{(x,k)\Rightarrow s_h\}:\tau$

$\mathrm{\Xi }={\mathrm{\Xi }}_0,\ell :\tau ,{\mathrm{\Xi }}_{+}$$\mathrm{\Gamma },x:{\tau }_1\mid \mathrm{\Delta },k:{\tau }_0\to \tau \mid {\mathrm{\Xi }}_0⊢s_h:\tau$

$\mathrm{\Gamma }\mid \mathrm{\Delta }\mid \mathrm{\Xi }⊢{\mathsf{cap}}_{\ell }\{(x,k)\Rightarrow s_h\}:{\tau }_1\to {\tau }_0$

$\ell \notin \mathrm{dom}(\mathrm{\Xi })$$\mathrm{\Gamma }\mid \mathrm{\Delta }\mid \mathrm{\Xi },\ell :\tau ⊢s:\tau$

$\mathrm{\Gamma }\mid \mathrm{\Delta }\mid \mathrm{\Xi }⊢{\mathrm{\#}}_{\ell }\{s\}:\tau$

The ordered label context records allocation origin. In ${\mathrm{\Xi }}_0,\ell :\tau ,{\mathrm{\Xi }}_{+}$, the stored handler body is typed in the birth prefix ${\mathrm{\Xi }}_0$; ${\mathrm{\Xi }}_{+}$ contains only delimiters allocated after $\ell$. This exact prefix premise, rather than deletion from an unordered set, is what preserves the clause type when a request crosses intervening delimiters.

Evaluation contexts and contexts not binding $\ell$ are Reduction is compatible closure under $H$ of Handler allocation is The remaining root contraction captures the delimited context: The label chosen by X-Handle-beta is fresh. Source terms contain no labels; runtime typing extends $\mathrm{\Xi }$ only through X-Delim.

Effekt

The selected Effekt source is The judgments are $\mathrm{\Gamma }⊢e:\tau$ and $\mathrm{\Gamma }\mid \mathrm{\Delta }\mid \mathrm{\Sigma }⊢s:\tau \mid \epsilon$, where $\mathrm{\Sigma }(F)={\tau }_1\to {\tau }_0$. Value variables, ordinary block variables, and operation names are pairwise disjoint syntactic classes; binders are alpha-renamed before extension. Expressions use X-Var and X-Const. The complete statement rules are

$\mathrm{\Gamma }⊢e:\tau$

$\mathrm{\Gamma }\mid \mathrm{\Delta }\mid \mathrm{\Sigma }⊢e:\tau \mid \varnothing$

$\mathrm{\Gamma }\mid \mathrm{\Delta }\mid \mathrm{\Sigma }⊢s_0:{\tau }_0\mid {\epsilon }_0$$\mathrm{\Gamma },x:{\tau }_0\mid \mathrm{\Delta }\mid \mathrm{\Sigma }⊢s_1:{\tau }_1\mid {\epsilon }_1$

$\mathrm{\Gamma }\mid \mathrm{\Delta }\mid \mathrm{\Sigma }⊢\mathsf{val}x=s_0;s_1:{\tau }_1\mid {\epsilon }_0\cup {\epsilon }_1$

$\mathrm{\Gamma },\overline{x}:\overline{\tau }\mid \mathrm{\Delta },\overline{g}:\overline{\sigma }\mid \mathrm{\Sigma }⊢s_0:{\tau }_0\mid {\epsilon }_0^{\prime }$$\mathrm{\Gamma }\mid \mathrm{\Delta },f:(\overline{\tau },\overline{\sigma })\to {\tau }_0/{\epsilon }_0\mid \mathrm{\Sigma }⊢s:\tau \mid \epsilon$

$\mathrm{\Gamma }\mid \mathrm{\Delta }\mid \mathrm{\Sigma }⊢\mathsf{def}f(\overline{x}:\overline{\tau },\overline{g}:\overline{\sigma }):{\tau }_0/{\epsilon }_0=s_0;s:\tau \mid ({\epsilon }_0^{\prime }\setminus {\epsilon }_0)\cup \epsilon$

$\mathrm{\Delta }(f)=(\overline{\tau },\overline{\sigma })\to \tau /\epsilon$$(\mathrm{\Gamma }⊢e_i:{\tau }_i{)}_i$$(\mathrm{\Delta }(g_j)={\sigma }_j{)}_j$

$\mathrm{\Gamma }\mid \mathrm{\Delta }\mid \mathrm{\Sigma }⊢f(\overline{e},\overline{g}):\tau \mid \epsilon$

$\mathrm{\Gamma }\mid \mathrm{\Delta }\mid \mathrm{\Sigma },F:{\tau }_1\to {\tau }_0⊢s:\tau \mid \epsilon$$F\notin \epsilon$

$\mathrm{\Gamma }\mid \mathrm{\Delta }\mid \mathrm{\Sigma }⊢\mathsf{effect}F(x:{\tau }_1):{\tau }_0;s:\tau \mid \epsilon$

$\mathrm{\Sigma }(F)={\tau }_1\to {\tau }_0$$\mathrm{\Gamma }⊢e:{\tau }_1$

$\mathrm{\Gamma }\mid \mathrm{\Delta }\mid \mathrm{\Sigma }⊢\mathsf{do}F(e):{\tau }_0\mid \{F\}$

$\mathrm{\Sigma }(F)={\tau }_1\to {\tau }_0$$\mathrm{\Gamma }\mid \mathrm{\Delta }\mid \mathrm{\Sigma }⊢s:\tau \mid \epsilon$$\mathrm{\Gamma },x:{\tau }_1\mid \mathrm{\Delta },\mathsf{resume}:{\tau }_0\to \tau /\varnothing \mid \mathrm{\Sigma }⊢s_h:\tau \mid {\epsilon }_h$

$\mathrm{\Gamma }\mid \mathrm{\Delta }\mid \mathrm{\Sigma }⊢\mathsf{try}\{s\}\mathsf{with}F\{(x:{\tau }_1)\Rightarrow s_h\}:\tau \mid (\epsilon \setminus \{F\})\cup {\epsilon }_h$

Effekt has no separate direct reduction relation in this chapter. Its semantics is the named syntax translation of Appendix D followed by System $\mathsf{Xi}$ reduction.

The tunnelling calculus

The selected syntax is Here $h_{\mathsf{v}}$ is an atomic handler variable; binders use $h$ as its metavariable. This repairs the self-referential production printed in the source. The source core has only unit; this book adds $\mathsf{Int}$, integer literals, and the three formation rules below for the chapter’s observable examples. Contexts are $\mathrm{\Delta }$ for effect variables, $P$ for handler variables, $\mathrm{\Gamma }$ for term variables, and $\mathrm{\Xi }$ for labels. The four judgments are $$\begin{array}{c}\mathrm{\Delta }\mid P\mid \mathrm{\Xi }⊢T\mathsf{type},\mathrm{\Delta }\mid P\mid \mathrm{\Xi }⊢\overline{e}\mathsf{effects},\\ \mathrm{\Delta }\mid P\mid \mathrm{\Gamma }\mid \mathrm{\Xi }⊢t:[T{]}_{\overline{e}},\mathrm{\Delta }\mid P\mid \mathrm{\Gamma }\mid \mathrm{\Xi }⊢h:\mathsf{F}\mid e.\end{array}$$ They are relative to a fixed interface signature $\mathcal{O}$; the premise $\mathsf{op}(\mathsf{F})=T\to S$ abbreviates $\mathcal{O}(\mathsf{F})=T\to S$, and $T\to S$ abbreviates $T\to [S{]}_{\varnothing }$. Effect sequences are identified up to permutation, duplicate removal, and flattening under effect substitution. The four characteristic rules are printed in Figure 10 of the source paper. The formation, ordinary typing, subtyping, and effect-inclusion rules below are the exact closure printed in Appendix A.1 of Cornell technical report 1813/60202. In particular, application and let assign one common effect to their premises; union-effect forms are derived with T-Sub, not substituted for the published rules. The complete table begins with well-formedness:

$\mathrm{\Delta }\mid P\mid \mathrm{\Xi }⊢\varnothing \mathsf{effects}$

$\alpha \in \mathrm{\Delta }$

$\mathrm{\Delta }\mid P\mid \mathrm{\Xi }⊢\alpha \mathsf{effects}$

$\ell \in \mathrm{dom}(\mathrm{\Xi })$

$\mathrm{\Delta }\mid P\mid \mathrm{\Xi }⊢\ell \mathsf{effects}$

$P(h)=\mathsf{F}$

$\mathrm{\Delta }\mid P\mid \mathrm{\Xi }⊢h.\mathsf{lbl}\mathsf{effects}$

$\mathrm{\Delta }\mid P\mid \mathrm{\Xi }⊢{\overline{e}}_1\mathsf{effects}$$\mathrm{\Delta }\mid P\mid \mathrm{\Xi }⊢{\overline{e}}_2\mathsf{effects}$

$\mathrm{\Delta }\mid P\mid \mathrm{\Xi }⊢{\overline{e}}_1,{\overline{e}}_2\mathsf{effects}$

$\mathrm{\Delta }\mid P\mid \mathrm{\Xi }⊢1\mathsf{type}$

$\mathrm{\Delta }\mid P\mid \mathrm{\Xi }⊢\mathsf{Int}\mathsf{type}$

$\mathrm{\Delta }\mid P\mid \mathrm{\Xi }⊢S\mathsf{type}$$\mathrm{\Delta }\mid P\mid \mathrm{\Xi }⊢T\mathsf{type}$$\mathrm{\Delta }\mid P\mid \mathrm{\Xi }⊢\overline{e}\mathsf{effects}$

$\mathrm{\Delta }\mid P\mid \mathrm{\Xi }⊢S\to [T{]}_{\overline{e}}\mathsf{type}$

$\mathrm{\Delta },\alpha \mid P\mid \mathrm{\Xi }⊢T\mathsf{type}$

$\mathrm{\Delta }\mid P\mid \mathrm{\Xi }⊢\mathrm{\forall }\alpha .T\mathsf{type}$

$\mathrm{\Delta }\mid P,h:\mathsf{F}\mid \mathrm{\Xi }⊢T\mathsf{type}$$\mathrm{\Delta }\mid P,h:\mathsf{F}\mid \mathrm{\Xi }⊢\overline{e}\mathsf{effects}$

$\mathrm{\Delta }\mid P\mid \mathrm{\Xi }⊢\mathrm{\Pi }h:\mathsf{F}.[T{]}_{\overline{e}}\mathsf{type}$

The term and handler rules are

$\mathrm{\Delta }\mid P\mid \mathrm{\Gamma }\mid \mathrm{\Xi }⊢():[1{]}_{\varnothing }$

$\mathrm{\Delta }\mid P\mid \mathrm{\Gamma }\mid \mathrm{\Xi }⊢n:[\mathsf{Int}{]}_{\varnothing }$

$x:T\in \mathrm{\Gamma }$

$\mathrm{\Delta }\mid P\mid \mathrm{\Gamma }\mid \mathrm{\Xi }⊢x:[T{]}_{\varnothing }$

$\mathrm{\Delta }\mid P\mid \mathrm{\Xi }⊢S\mathsf{type}$$\mathrm{\Delta }\mid P\mid \mathrm{\Gamma },x:S\mid \mathrm{\Xi }⊢t:[T{]}_{\overline{e}}$

$\mathrm{\Delta }\mid P\mid \mathrm{\Gamma }\mid \mathrm{\Xi }⊢\lambda x:S.t:[S\to [T{]}_{\overline{e}}{]}_{\varnothing }$

$\mathrm{\Delta }\mid P\mid \mathrm{\Gamma }\mid \mathrm{\Xi }⊢t_1:[S\to [T{]}_{\overline{e}}{]}_{\overline{e}}$$\mathrm{\Delta }\mid P\mid \mathrm{\Gamma }\mid \mathrm{\Xi }⊢t_2:[S{]}_{\overline{e}}$

$\mathrm{\Delta }\mid P\mid \mathrm{\Gamma }\mid \mathrm{\Xi }⊢t_1{t}_2:[T{]}_{\overline{e}}$

$\mathrm{\Delta }\mid P\mid \mathrm{\Xi }⊢S\mathsf{type}$$\mathrm{\Delta }\mid P\mid \mathrm{\Gamma }\mid \mathrm{\Xi }⊢t_1:[S{]}_{\overline{e}}$$\mathrm{\Delta }\mid P\mid \mathrm{\Gamma },x:S\mid \mathrm{\Xi }⊢t_2:[T{]}_{\overline{e}}$

$\mathrm{\Delta }\mid P\mid \mathrm{\Gamma }\mid \mathrm{\Xi }⊢\mathsf{let}x:S=t_1\mathsf{in}{t}_2:[T{]}_{\overline{e}}$

Type subtyping is the least transitive relation generated by

$\mathrm{\Delta }\mid P\mid \mathrm{\Xi }⊢1\le 1$

$\mathrm{\Delta }\mid P\mid \mathrm{\Xi }⊢\mathsf{Int}\le \mathsf{Int}$

$\mathrm{\Delta }\mid P\mid \mathrm{\Xi }⊢T_2\le T_1$$\mathrm{\Delta }\mid P\mid \mathrm{\Xi }⊢S_1\le S_2$$\mathrm{\Delta }\mid P\mid \mathrm{\Xi }⊢{\overline{e}}_1\le {\overline{e}}_2$

$\mathrm{\Delta }\mid P\mid \mathrm{\Xi }⊢T_1\to [S_1{]}_{{\overline{e}}_1}\le T_2\to [S_2{]}_{{\overline{e}}_2}$

$\mathrm{\Delta },\alpha \mid P\mid \mathrm{\Xi }⊢T_1\le T_2$

$\mathrm{\Delta }\mid P\mid \mathrm{\Xi }⊢\mathrm{\forall }\alpha .T_1\le \mathrm{\forall }\alpha .T_2$

$\mathrm{\Delta }\mid P,h:\mathsf{F}\mid \mathrm{\Xi }⊢T_1\le T_2$$\mathrm{\Delta }\mid P,h:\mathsf{F}\mid \mathrm{\Xi }⊢{\overline{e}}_1\le {\overline{e}}_2$

$\mathrm{\Delta }\mid P\mid \mathrm{\Xi }⊢\mathrm{\Pi }h:\mathsf{F}.[T_1{]}_{{\overline{e}}_1}\le \mathrm{\Pi }h:\mathsf{F}.[T_2{]}_{{\overline{e}}_2}$

$\mathrm{\Delta }\mid P\mid \mathrm{\Xi }⊢T_1\le T_2$$\mathrm{\Delta }\mid P\mid \mathrm{\Xi }⊢T_2\le T_3$

$\mathrm{\Delta }\mid P\mid \mathrm{\Xi }⊢T_1\le T_3$

Effect inclusion and term subsumption are

$(\mathrm{\forall }j)(\mathrm{\exists }i).e_{1j}=e_{2i}$$(\mathrm{\Delta }\mid P\mid \mathrm{\Xi }⊢e_{2i}\mathsf{effects}{)}_i$

$\mathrm{\Delta }\mid P\mid \mathrm{\Xi }⊢{\overline{e}}_1\le {\overline{e}}_2$

$\mathrm{\Delta }\mid P\mid \mathrm{\Gamma }\mid \mathrm{\Xi }⊢t:[T_1{]}_{{\overline{e}}_1}$$\mathrm{\Delta }\mid P\mid \mathrm{\Xi }⊢T_1\le T_2$$\mathrm{\Delta }\mid P\mid \mathrm{\Xi }⊢{\overline{e}}_1\le {\overline{e}}_2$

$\mathrm{\Delta }\mid P\mid \mathrm{\Gamma }\mid \mathrm{\Xi }⊢t:[T_2{]}_{{\overline{e}}_2}$

The usual union-effect application and sequencing rules are admissible by subsuming their premises to a common finite join before applying T-App or T-Let.

$\mathrm{\Delta },\alpha \mid P\mid \mathrm{\Gamma }\mid \mathrm{\Xi }⊢t:[T{]}_{\varnothing }$

$\mathrm{\Delta }\mid P\mid \mathrm{\Gamma }\mid \mathrm{\Xi }⊢\mathrm{\Lambda }\alpha .t:[\mathrm{\forall }\alpha .T{]}_{\varnothing }$

$\mathrm{\Delta }\mid P\mid \mathrm{\Gamma }\mid \mathrm{\Xi }⊢t:[\mathrm{\forall }\alpha .T{]}_{{\overline{e}}_0}$$\mathrm{\Delta }\mid P\mid \mathrm{\Xi }⊢\overline{e}\mathsf{effects}$

$\mathrm{\Delta }\mid P\mid \mathrm{\Gamma }\mid \mathrm{\Xi }⊢t[\overline{e}]:[T[\overline{e}/\alpha ]{]}_{{\overline{e}}_0}$

$\mathrm{\Delta }\mid P,h:\mathsf{F}\mid \mathrm{\Gamma }\mid \mathrm{\Xi }⊢t:[T{]}_{\overline{e}}$

$\mathrm{\Delta }\mid P\mid \mathrm{\Gamma }\mid \mathrm{\Xi }⊢\lambda h:\mathsf{F}.t:[\mathrm{\Pi }h:\mathsf{F}.[T{]}_{\overline{e}}{]}_{\varnothing }$

$\mathrm{\Delta }\mid P\mid \mathrm{\Gamma }\mid \mathrm{\Xi }⊢t:[\mathrm{\Pi }h:\mathsf{F}.[T{]}_{\overline{e}}{]}_{{\overline{e}}_0}$$\mathrm{\Delta }\mid P\mid \mathrm{\Gamma }\mid \mathrm{\Xi }⊢h:\mathsf{F}\mid e$

$\mathrm{\Delta }\mid P\mid \mathrm{\Gamma }\mid \mathrm{\Xi }⊢th:[T[h]{]}_{\overline{e}[h],{\overline{e}}_0}$

$P(h)=\mathsf{F}$

$\mathrm{\Delta }\mid P\mid \mathrm{\Gamma }\mid \mathrm{\Xi }⊢h:\mathsf{F}\mid h.\mathsf{lbl}$

$\mathrm{\Delta }\mid P\mid \mathrm{\Gamma }\mid \mathrm{\Xi }⊢h:\mathsf{F}\mid e$$\mathsf{op}(\mathsf{F})=T\to S$

$\mathrm{\Delta }\mid P\mid \mathrm{\Gamma }\mid \mathrm{\Xi }⊢\Uparrow h:[T\to [S{]}_e{]}_{\varnothing }$

$\mathrm{\Xi }(\ell )=[S{]}_{\overline{e}}$$\mathsf{op}(\mathsf{F})=T_1\to T_2$$\mathrm{\Delta }\mid P\mid \mathrm{\Gamma },x:T_1,k:T_2\to [S{]}_{\overline{e}}\mid \mathrm{\Xi }⊢t:[S{]}_{\overline{e}}$

$\mathrm{\Delta }\mid P\mid \mathrm{\Gamma }\mid \mathrm{\Xi }⊢({\mathsf{handler}}^{\mathsf{F}}xk.t{)}^{\ell }:\mathsf{F}\mid \ell$

$\ell \notin \mathrm{dom}(\mathrm{\Xi })$$\mathrm{\Delta }\mid P\mid \mathrm{\Gamma }\mid \mathrm{\Xi },\ell :[T{]}_{\overline{e}}⊢t:[T{]}_{\overline{e},\ell }$$\mathrm{\Delta }\mid P\mid \mathrm{\Xi }⊢T\mathsf{type}$$\mathrm{\Delta }\mid P\mid \mathrm{\Xi }⊢\overline{e}\mathsf{effects}$

$\mathrm{\Delta }\mid P\mid \mathrm{\Gamma }\mid \mathrm{\Xi }⊢{\Downarrow }_{[T{]}_{\overline{e}}}^{\ell }t:[T{]}_{\overline{e}}$

Here $T[h]$ and $\overline{e}[h]$ replace the bound handler variable by its argument and replace $h.\mathsf{lbl}$ by the argument label. Every context extension in this card binds a fresh name; the explicit first premise of T-Down records the delimiter-label instance of that convention. Since the type and effect well-formedness premises are checked before the fresh label is added, WF-Label derives $\ell \notin \mathrm{fl}(T,\overline{e})$; this is not an independent hypothesis.

Values and evaluation contexts are Contextual refinement quantifies over the larger program-context grammar Its well-formedness judgment is $⊢C:\mathrm{\Delta }\mid P\mid \mathrm{\Gamma }\mid \mathrm{\Xi }\mid [T{]}_{\overline{e}}⟹T^{\prime }$. These are not the evaluation contexts $K$. Reduction is compatible closure under $K$ of The tunneled request contraction is where $H={\mathsf{handler}}^{\mathsf{F}}xk.t$, $\mathsf{op}(\mathsf{F})=T_1\to T_2$, and $K$ does not bind $\ell$.

Source-bounded finer cards

Control-flow linearity uses the comparison predicate $\mathsf{uses}(r,M)\le q$, $q\in \{1,\omega \}$, from section 32.5; no rule of the source calculus is imported.

The Olaf source boundary uses the typing judgment $$\mathrm{\Delta }\mid \mathrm{\Theta }\mid \mathrm{\Gamma }\mid \mathrm{\Xi }⊢t:[\tau {]}_c$$ and configuration transition $L;t⟶L^{\prime };t^{\prime }$. Its operation signatures, continuation types, lifetime effects, fixpoint handlers, and rules belong to the source calculus of [ZSM20]; section 32.5 records its theorem boundary. No Olaf rule is imported into System $\mathsf{Xi}$, Effekt, or the tunnelling calculus.

The locality source card distinguishes ordinary bindings $\mathrm{\Gamma };x:\tau$ from global bindings $\mathrm{\Gamma };x{:}_{◻}\tau$ and restricts contexts by $$\varnothing /◻=\varnothing ,(\mathrm{\Gamma };x:\tau )/◻=\mathrm{\Gamma }/◻,(\mathrm{\Gamma };x{:}_{◻}\tau )/◻=(\mathrm{\Gamma }/◻);x{:}_{◻}\tau .$$ Its characteristic introduction rule is

$\mathrm{\Gamma }/◻{⊢}_{\mathsf{V}}v:\tau$

$\mathrm{\Gamma }{⊢}_{\mathsf{V}}\mathsf{box}v:◻\tau$

The effect-reflection card uses $y(\mathrm{\Sigma })$, $W_{\mathrm{\Sigma }}(\tau )$, $\mathsf{reflect}$, and ${\mathsf{reify}}_{\mathrm{\Sigma }}$ with

$\mathrm{\Gamma }{⊢}_{\mathsf{V}}{v}_1:y(\mathrm{\Sigma })$$\mathsf{op}:{\tau }_1⇝{\tau }_2\in \mathrm{\Sigma }$$\mathrm{\Gamma }{⊢}_{\mathsf{V}}{v}_2:◻{\tau }_1$$\mathrm{\Gamma };x:◻{\tau }_2{⊢}_{\mathsf{C}}c:{\tau }_3$

$\mathrm{\Gamma }{⊢}_{\mathsf{C}}\mathsf{reflect}(v_1(\mathsf{op}))(v_2,x.c):{\tau }_3$

$\mathrm{\Gamma };x:y(\mathrm{\Sigma }){⊢}_{\mathsf{C}}c:◻\tau$

$\mathrm{\Gamma }{⊢}_{\mathsf{C}}{\mathsf{reify}}_{\mathrm{\Sigma }}(x.c):W_{\mathrm{\Sigma }}(◻\tau )$

These two cards belong to [Whi26]; they supply no rule to the three principal calculi of this appendix section.