Region and capability interfaces

Tofte–Talpin inference has the form $$\mathit{TE}⊢e⇝e^{\prime }:\mu ,\varphi ,\varphi ::=\varnothing \mid ϵ\mid \{\mathsf{get}(\rho )\}\mid \{\mathsf{put}(\rho )\}\mid {\varphi }_1\cup {\varphi }_2.$$ Constants, variables, and sequencing carry effects as follows:

$\mathit{TE}⊢c⇝c\mathsf{at}\rho :(\mathsf{int},\rho ),\{\mathsf{put}(\rho )\}$

$\mathit{TE}(x)=(\tau ,\rho )$

$\mathit{TE}⊢x⇝x:(\tau ,\rho ),\varnothing$

$\mathit{TE}⊢e_1⇝e_1^{\prime }:({\tau }_1,{\rho }_1),{\varphi }_1$$\mathit{TE},x:({\tau }_1,{\rho }_1)⊢e_2⇝e_2^{\prime }:\mu ,{\varphi }_2$

$\mathit{TE}⊢\mathsf{let}x=e_1\mathsf{in}{e}_2\mathsf{end}⇝\mathsf{let}x=e_1^{\prime }\mathsf{in}{e}_2^{\prime }\mathsf{end}:\mu ,{\varphi }_1\cup {\varphi }_2$

Its delimiter is $$\frac{\begin{array}{c}\mathit{TE}⊢e⇝e^{\prime }:\mu ,\varphi \\ \rho \notin \mathrm{frv}(\mathit{TE},\mu )\end{array}}{\mathit{TE}⊢e⇝\mathsf{letregion}\rho \mathsf{in}{e}^{\prime }\mathsf{end}:\mu ,\varphi \setminus \{\mathsf{get}(\rho ),\mathsf{put}(\rho )\}}\mathrm{RI}-\mathrm{Letregion}.$$ The body effect may contain $\rho$; the rule discharges it.

The capability core uses $$r::=\rho \mid \nu ,C::=\epsilon \mid \varnothing \mid \{r^{+}\}\mid \{r^1\}\mid C_1\oplus C_2\mid \bar{C}.$$ Access and allocation require authority for $r$; deallocation requires and consumes $\{r^1\}$. The state judgment combines memory realization, capability satisfiability, and expression typing. Expressions sequence declarations and may halt only after consuming all linear capability:

$\mathrm{\Psi };\mathrm{\Delta };\mathrm{\Gamma };C⊢d\Rightarrow {\mathrm{\Delta }}^{\prime };{\mathrm{\Gamma }}^{\prime };C^{\prime }$$\mathrm{\Psi };{\mathrm{\Delta }}^{\prime };{\mathrm{\Gamma }}^{\prime };C^{\prime }⊢e$

$\mathrm{\Psi };\mathrm{\Delta };\mathrm{\Gamma };C⊢\mathsf{let}d\mathsf{in}e$

$\mathrm{\Psi };\mathrm{\Delta };\mathrm{\Gamma }⊢v:\mathsf{int}$$\mathrm{\Delta }⊢C{=}_{\mathsf{Cap}}\varnothing$

$\mathrm{\Psi };\mathrm{\Delta };\mathrm{\Gamma };C⊢\mathsf{halt}v$

The declaration rules are

$\rho \notin \mathrm{dom}(\mathrm{\Delta })$$x\notin \mathrm{dom}(\mathrm{\Gamma })$

$\mathrm{\Psi };\mathrm{\Delta };\mathrm{\Gamma };C⊢\mathsf{newrgn}\rho ,x\Rightarrow \mathrm{\Delta },\rho :\mathsf{Rgn};\mathrm{\Gamma },x:\rho \mathsf{handle};C\oplus \{{\rho }^1\}$

$\mathrm{\Psi };\mathrm{\Delta };\mathrm{\Gamma }⊢v:r\mathsf{handle}$$\mathrm{\Psi };\mathrm{\Delta };\mathrm{\Gamma }⊢h\mathsf{at}r:\tau$$\mathrm{\Delta }⊢C{\le }_{\mathsf{Cap}}{C}^{\prime }\oplus \{r^{+}\}$

$\mathrm{\Psi };\mathrm{\Delta };\mathrm{\Gamma };C⊢x=h\mathsf{at}v\Rightarrow \mathrm{\Delta };\mathrm{\Gamma },x:\tau ;C$

$\mathrm{\Psi };\mathrm{\Delta };\mathrm{\Gamma }⊢v:⟨{\tau }_0,\dots ,{\tau }_{n-1}⟩\mathsf{at}r$$\mathrm{\Delta }⊢C{\le }_{\mathsf{Cap}}{C}^{\prime }\oplus \{r^{+}\}$

$\mathrm{\Psi };\mathrm{\Delta };\mathrm{\Gamma };C⊢x={\pi }_{i}v\Rightarrow \mathrm{\Delta };\mathrm{\Gamma },x:{\tau }_i;C$

$\mathrm{\Psi };\mathrm{\Delta };\mathrm{\Gamma }⊢v:r\mathsf{handle}$$\mathrm{\Delta }⊢C{=}_{\mathsf{Cap}}{C}^{\prime }\oplus \{r^1\}$

$\mathrm{\Psi };\mathrm{\Delta };\mathrm{\Gamma };C⊢\mathsf{freergn}v\Rightarrow \mathrm{\Delta };\mathrm{\Gamma };C^{\prime }$

The program boundary is $$\frac{\begin{array}{c}⊢M:\mathrm{\Psi }\\ \mathrm{\Psi }\vDash C\\ \mathrm{\Psi };\cdot ;\cdot ;C⊢e\end{array}}{⊢(M,e)}\mathrm{Cap}-\mathrm{Program}.$$ The separate WCM region calculus has $\psi ::=\alpha \mid \varnothing \mid \{r\}\mid {\psi }_1\cup {\psi }_2$. Projection records the accessed region, and the region delimiter discharges it only under the displayed scope conditions:

$\mathrm{\Delta };\mathrm{\Gamma }{⊢}_{R}e:⟨{\tau }_0,\dots ,{\tau }_{n-1}⟩\mathsf{at}r,\psi$

$\mathrm{\Delta };\mathrm{\Gamma }{⊢}_R{\pi }_{i}e:{\tau }_i,\psi \cup \{r\}$

$\mathrm{\Delta },\rho :\mathsf{Rgn};\mathrm{\Gamma },x_{\rho }:\rho \mathsf{handle}{⊢}_{R}e:\tau ,\psi$$\rho \notin \mathrm{ftv}(\tau )\cup \mathrm{dom}(\mathrm{\Delta })$$x_{\rho }\notin \mathrm{dom}(\mathrm{\Gamma })$

$\mathrm{\Delta };\mathrm{\Gamma }{⊢}_R\mathsf{letregion}\rho ,x_{\rho }\mathsf{in}e:\tau ,\psi \setminus \{\rho \}$

The named translation has $\mathsf{CapOf}(\alpha )=\alpha$ and $\mathsf{CapOf}(\{r\})=\{r^{+}\}$. Its meta-level continuation consumes fresh unique authority with $\mathsf{freergn}$; it introduces no target lambda.

The three source-bounded comparison cards retain their distinct judgments. Cyclic regions add only the pointer covariance rule

$\gamma ⊢r_{\mathrm{long}}⪰r_{\mathrm{short}}$

$\mathrm{\Delta };\gamma ⊢\mathsf{ptr}(\tau ,r_{\mathrm{long}})\le \mathsf{ptr}(\tau ,r_{\mathrm{short}})$

The L3 card instead types allocation, deallocation, and exchange by

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

$\mathrm{\Delta };\mathrm{\Gamma }⊢\mathsf{new}e:\mathrm{\exists }\rho .(\mathsf{Cap}\rho \tau \otimes !\mathsf{Ptr}\rho )$

$\mathrm{\Delta };\mathrm{\Gamma }⊢e:\mathrm{\exists }\rho .(\mathsf{Cap}\rho \tau \otimes !\mathsf{Ptr}\rho )$

$\mathrm{\Delta };\mathrm{\Gamma }⊢\mathsf{free}e:\mathrm{\exists }\rho .\tau$

$\mathrm{\Delta };{\mathrm{\Gamma }}_1⊢e_1:\mathsf{Cap}\rho {\tau }_1$$\mathrm{\Delta };{\mathrm{\Gamma }}_2⊢e_2:\mathsf{Ptr}\rho$$\mathrm{\Delta };{\mathrm{\Gamma }}_3⊢e_3:{\tau }_3$

$\mathrm{\Delta };{\mathrm{\Gamma }}_1,{\mathrm{\Gamma }}_2,{\mathrm{\Gamma }}_3⊢\mathsf{swap}{e}_1{e}_2{e}_3:\mathsf{Cap}\rho {\tau }_3\otimes {\tau }_1$