Capability and Region Types for Typed Memory Management

Prerequisites. Direct starred prerequisites: none. No later core chapter depends on this route.

Let a source computation bind one integer that it never returns: $$\mathsf{let}x=1\mathsf{in}2\mathsf{end}.$$ Region inference may place the dead binding in a fresh local region while placing the returned integer in an outer region. Three static facts are distinct: the result must not mention the local region, the body may access it only while it is live, and explicit deallocation requires unique authority. Tofte–Talpin region inference proves the first two [TT97]; the Walker–Crary–Morrisett capability calculus proves the third [WCM00].

Tofte–Talpin region inference

Write $\rho$ for a region variable, $ϵ$ for an effect variable, and $\varphi$ for a finite region effect: a set of effect variables and actions $\mathsf{get}(\rho )$ and $\mathsf{put}(\rho )$. A type with place is a pair $\mu =(\tau ,\rho )$; an arrow type carries the arrow effect $ϵ.\varphi$, the pair of a handle $ϵ$ and a latent effect $\varphi$. The exact source and target cores are The full type grammar adds region- and effect-polymorphic schemes. A type environment $\mathit{TE}$ assigns those schemes to source variables. Write $\mathrm{frv}(X)$ for the free region variables of the displayed object or tuple of objects $X$. The inference judgment $$\mathit{TE}⊢e⇝e^{\prime }:\mu ,\varphi$$ means that source term $e$ translates to annotated term $e^{\prime }$, has type with place $\mu$, and may perform the region actions in $\varphi$.

Rules 20, 21, 25, and 27 suffice for the opening calculation:

$\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$

$$\frac{\begin{array}{c}\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\end{array}}{\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}\mathrm{RI}-\mathrm{Let}$$ Rule 27 is the scope boundary: $$\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}$$ There is no premise forbidding $\rho$ in the body effect. The rule exists precisely to discharge those local effects. Freshness concerns the surrounding type environment and the result type-with-place.

Take an outer region ${\rho }_0$ for the returned integer and a fresh local region $\rho$ for the dead binding. The inferred target is $$\mathsf{letregion}\rho \mathsf{in}\mathsf{let}x=1\mathsf{at}\rho \mathsf{in}2\mathsf{at}{\rho }_0\mathsf{end}\mathsf{end},$$ and its effect calculation is The result type with place is $(\mathsf{int},{\rho }_0)$, so $\rho \notin \mathrm{frv}(\mu )$; the empty initial $\mathit{TE}$ discharges the other freshness premise.

Let $\mathcal{P}$ map types, type schemes, and environments to their Milner counterparts by erasing places, region variables, and effects. Fixing ${\rho }_0$ and ${ϵ}_0$, let $\mathcal{R}$ relate Milner objects to region objects by choosing ${\rho }_0$ at every place and the arrow effect $${ϵ}_0.\{\mathsf{get}({\rho }_0),\mathsf{put}({\rho }_0),{ϵ}_0\}$$ at every arrow; its clauses for simple and compound schemes preserve their distinct quantifier shapes. These are the projection and relation of Tofte–Talpin Section 5.3.

Proof of Theorem 50.1 — Region inference refines Milner typing

Proof. Part 1 is Tofte–Talpin Lemma 5.1, by induction on the region derivation. Part 2 is Lemma 5.2. The displayed $\mathcal{R}$ is a relation rather than a function because simple and compound type schemes have different shapes. The variable case selects the appropriate scheme rule; the lambda case uses the effect-enlargement premise. Lemma 5.3 gives simultaneous type, region, and effect substitution. Neither direction claims principal effects or optimal placement. ◻

Semantic correspondence

The ordinary semantics evaluates $E⊢e\Downarrow v$ in source environment $E$. The region semantics evaluates $s,VE,R⊢e^{\prime }\Downarrow v^{\prime },s^{\prime }$, where $R$ maps region variables to concrete region names and $s$ is a region-indexed store. Tofte and Talpin’s coinductive relation $\mathcal{C}(R,\mathit{TE},E,s,VE)\mathsf{w}\mathsf{.}\mathsf{r}\mathsf{.}\mathsf{t}\mathsf{.}\varphi \cup {\varphi }^{\prime }$ relates configurations. A region environment $R$ connects an effect $\varphi$ to $s$ when $\mathrm{frv}(\varphi )\subseteq \mathrm{dom}(R)$ and $R(\rho )\in \mathrm{dom}(s)$ for every $\rho \in \mathrm{frv}(\varphi )$; $R{\equiv }_{\varphi }{R}^{\prime }$ means agreement on $\mathrm{frv}(\varphi )$.

Proof of Theorem 50.2 — Tofte–Talpin semantic correspondence

Proof. This is Theorem 6.1 of Tofte and Talpin. Section 7 defines consistency; Section 8 proves its closure and store-extension properties. Section 9 uses an outer induction on the source-evaluation derivation and, in each case, an inner induction on the region-inference derivation. In the region case, Lemma 5.3 permits choosing $\rho \notin \mathrm{frv}({\varphi }^{\prime })$ in addition to RI-Letregion’s freshness for $\mathit{TE}$ and $\mu$. Allocate a fresh concrete region, invoke the induction hypothesis, and remove it; the two freshness facts separately protect the result and continuation. This chapter imports that complete proof for the exact source and target cores displayed above. ◻

Effects approximate future region use, whereas tracing collection follows reachability; neither approximation contains the other. The later ML Kit work turns constraints into spreading and fixed-point computations. The historical and engineering account belongs to the region-memory retrospective [TBEH04], not to Theorem 6.1.

The capability machine

Walker, Crary, and Morrisett use region variables $\rho$, concrete region names $\nu$, and regions $r::=\rho \mid \nu$. The runtime value $\mathsf{handle}(\nu )$, a region handle, is distinct from the compile-time name $\nu$. Selected syntax is The capability variable $\epsilon$ ranges over unknown authority. The duplicable authority $\{r^{+}\}$ permits shared access; the unique authority $\{r^1\}$ permits destruction. The stripping operation $\bar{C}$ changes unique flags to duplicable ones, distributes over $\oplus$, and is idempotent. In particular, $$\varnothing \oplus C=C,\overline{\{r^1\}}=\{r^{+}\},\overline{C_1\oplus C_2}=\overline{C_1}\oplus \overline{C_2},\overline{\stackrel{―}{C}}=\bar{C}.$$ The judgment $\mathrm{\Delta }⊢C_1{=}_{\mathsf{Cap}}{C}_2$ is the congruence generated by these equations, associativity, commutativity, and the bounded variables in $\mathrm{\Delta }$. Write $\mathrm{\Delta }⊢C_1{\le }_{\mathsf{Cap}}{C}_2$ when some $C_3$ satisfies $\mathrm{\Delta }⊢C_1{=}_{\mathsf{Cap}}{C}_2\oplus C_3$. Stripped authority is idempotent; $\{r^1\}\oplus \{r^1\}$ is not satisfiable. Subcapability admits $\{r^1\}\le \{r^{+}\}$, not the converse.

A memory $M$ maps $\nu$ to finite region heaps. A memory type $\mathrm{\Psi }$ maps each $\nu$ to a region type $\mathrm{{\rm Y}}$, which maps allocated labels to their heap-value types. The judgment $⊢M:\mathrm{\Psi }$ checks the same region names and gives every allocated label the heap-value type recorded by $\mathrm{{\rm Y}}$. The declaration judgment $$\mathrm{\Psi };\mathrm{\Delta };\mathrm{\Gamma };C⊢d\Rightarrow {\mathrm{\Delta }}^{\prime };{\mathrm{\Gamma }}^{\prime };C^{\prime }$$ threads authority. The expression rules connecting it to programs are

$\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$

Four declaration rules expose the resource boundary: $$\frac{\begin{array}{c}\rho \notin \mathrm{dom}(\mathrm{\Delta })\\ x\notin \mathrm{dom}(\mathrm{\Gamma })\end{array}}{\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{Cap}-\mathrm{New}$$ $$\frac{\begin{array}{c}\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^{+}\}\end{array}}{\mathrm{\Psi };\mathrm{\Delta };\mathrm{\Gamma };C⊢x=h\mathsf{at}v\Rightarrow \mathrm{\Delta };\mathrm{\Gamma },x:\tau ;C}\mathrm{Cap}-\mathrm{Alloc}$$ $$\frac{\begin{array}{c}\mathrm{\Psi };\mathrm{\Delta };\mathrm{\Gamma }⊢v:r\mathsf{handle}\\ \mathrm{\Delta }⊢C{=}_{\mathsf{Cap}}{C}^{\prime }\oplus \{r^1\}\end{array}}{\mathrm{\Psi };\mathrm{\Delta };\mathrm{\Gamma };C⊢\mathsf{freergn}v\Rightarrow \mathrm{\Delta };\mathrm{\Gamma };C^{\prime }}\mathrm{Cap}-\mathrm{Free}$$ For example, Cap-New followed by Cap-Alloc derives allocation under $\{{\rho }^1\}$, since unique authority is a subcapability of duplicable access authority. Cap-Free then consumes exactly the unique occurrence.

The machine dynamics has the same phase distinction: where $\nu \notin \mathrm{dom}(M)$ in the first line; $\nu \in \mathrm{dom}(M)$ and $\ell$ is fresh in its heap in the second; and $M(\nu .\ell )=⟨v_0,\dots ,v_{n-1}⟩$ with in the third. The free rule likewise requires $\nu \in \mathrm{dom}(M)$.

Proof of Lemma 50.4 — Capability–memory correspondence

Proof. Invert the single satisfiability rule. The normal form lists exactly the distinct names in $\mathrm{\Psi }$. Capability-equality cardinality preservation keeps unique occurrences unique; stripping may change $1$ to $+$ but does not change the name set. Removing the unique singleton and the matching memory-type entry yields the final clause. These are the report’s CECP lemma and Lemmas 34–35. ◻

Proof of Theorem 50.5 — Capability preservation and progress

Proof. These are technical-report Lemmas 36–37. Preservation uses substitution, memory-type extension, and memory garbage collection. In the free case, Cap-Free exposes a unique singleton and lemma 50.4 removes it together with its region. Progress inverts Cap-Program; canonical memory typing turns every typed address into an allocated label, while satisfiability turns every required region authority into a live concrete region. Thus allocation, projection, and free have matching dynamic rules. ◻

Proof of Corollary 50.6 — Capability-calculus memory safety

Proof. Induct on the reduction length with preservation and finish with progress. This is technical-report Theorem 39. ◻

Proof of Theorem 50.7 — Complete collection

Proof. A terminating run ends in a well-typed halt by preservation and progress. Invert Cap-Halt. By lemma 50.4, satisfiability under empty authority forces $\mathrm{\Psi }=\{\}$. Inversion of memory typing forces $M=\{\}$. This is technical-report Theorem 40. ◻

A separate region calculus and its CPS translation

The source of the Walker–Crary–Morrisett translation is not the inference language above. It is a second, explicitly typed region calculus: Its effects record region access without distinguishing $\mathsf{get}$ from $\mathsf{put}$. Its delimiter binds both a compile-time region variable and the runtime handle. The projection and delimiter rules are and $$\frac{\begin{array}{c}\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 })\end{array}}{\mathrm{\Delta };\mathrm{\Gamma }{⊢}_R\mathsf{letregion}\rho ,x_{\rho }\mathsf{in}e:\tau ,\psi \setminus \{\rho \}}\mathrm{R}-\mathrm{Letregion}$$ Again the body may mention $\rho$; the conclusion discharges it.

The running region-calculus term is $$e_{\mathsf{pairFirst}}=\mathsf{letregion}\rho ,x_{\rho }\mathsf{in}{\pi }_0(⟨1,2⟩\mathsf{at}{x}_{\rho }).$$ Allocation gives the pair type $⟨\mathsf{int},\mathsf{int}⟩\mathsf{at}\rho$; R-Project returns an integer while retaining effect $\{\rho \}$, and R-Letregion discharges that effect because the result type contains no free $\rho$.

The named effect-to-capability translation is total on that grammar: $$\mathsf{CapOf}(\alpha )=\alpha ,\mathsf{CapOf}(\varnothing )=\varnothing ,\mathsf{CapOf}(\{r\})=\{r^{+}\},$$ $$\mathsf{CapOf}({\psi }_1\cup {\psi }_2)=\mathsf{CapOf}({\psi }_1)\oplus \mathsf{CapOf}({\psi }_2).$$ Every translated arrow effect is stripped, hence duplicable; equality of such capabilities is therefore set equality. Terms use the context- and continuation-indexed translation ${\mathsf{CPS}}_{\mathrm{\Delta };\mathrm{\Gamma };\mathrm{\Theta }}(e;k)$. The delimiter uses a WCM meta-level continuation, written $$k=⟨x_k;e_k⟩.$$ Its application is the target term $$\mathsf{apply}(k,v)=\mathsf{let}{x}_k=v\mathsf{in}{e}_k.$$ The delimiter clause is where ${\mathrm{\Theta }}^{\prime }$ extends both the current capability $C_{\mathrm{\Theta }}$ and its bound $B_{\mathrm{\Theta }}$ by $\{{\rho }^1\}$. No object-level lambda is introduced.

Proof of Theorem 50.8 — Region-to-capability CPS type preservation

Proof. This is technical-report Theorem 52. Its strengthened induction carries a translation environment $\mathrm{\Theta }$, current capability $C_{\mathrm{\Theta }}$, and bound $B_{\mathrm{\Theta }}$ satisfying $B_{\mathrm{\Theta }}=B_{\mathrm{\Theta }}\oplus \mathsf{CapOf}(\psi )$. Lemmas 43–48 preserve well-formedness, substitution, equality, and effect inclusion. In the R-Letregion case both $C_{\mathrm{\Theta }}$ and the bound grow by $\{{\rho }^1\}$, the translated body runs while $\rho$ is live, and the continuation is typed by Cap-Free. Instantiating the strengthened result with empty contexts yields the theorem. ◻

For $e_{\mathsf{pairFirst}}$, dynamics chooses a concrete $\nu$. The authority calculation is $$\varnothing \stackrel{Cap-New}{\to }\{{\nu }^1\}\stackrel{Cap-Alloc,Cap-Project}{\to }\{{\nu }^1\}\stackrel{Cap-Free\mathsf{handle}(\nu )}{\to }\varnothing .$$ After the last arrow, both $M(\nu )$ and authority for $\nu$ are absent.

Cyclone: handles, inference, and region order

Cyclone combines explicit handles, lexically scoped regions, effects, local inference, and region subtyping in a C-like language [GMJ^+02]. Let $\gamma ⊢r_{\mathrm{long}}⪰r_{\mathrm{short}}$ mean that the region-order context $\gamma$ proves the first region outlives the second. A pointer into the longer-lived region may be used where the shorter guarantee is expected: $$\frac{\gamma ⊢r_{\mathrm{long}}⪰r_{\mathrm{short}}}{\mathrm{\Delta };\gamma ⊢\mathsf{ptr}(\tau ,r_{\mathrm{long}})\le \mathsf{ptr}(\tau ,r_{\mathrm{short}})}\mathrm{Cyc}-\mathrm{Region}-\mathrm{Sub}$$ The reverse coercion is not derivable.

Cyclone’s right-expression judgment has the form $\mathrm{\Delta };\mathrm{\Gamma };\gamma ;ϵ{⊢}_{\mathsf{rhs}}e:\tau$. Here $\mathrm{\Delta }$ binds type and region names, $\mathrm{\Gamma }$ binds values, $\gamma$ records outlives constraints, and the live-region effect $ϵ$ is a set of regions—not a set of $\mathsf{get}/\mathsf{put}$ actions. For a live lexical region $r$, the two relevant judgments are The first two lines expose the core context discipline; the last is a bounded execution schematic, not executable Cyclone code. The cited technical report proves type soundness [GMJ^+01]. The PLDI paper summarizes the design. Neither document proves correspondence for a particular compiler revision.

Three source-bounded system cards

Proof of Theorem 50.10 — Core L^3 soundness

Proof. This is Theorem 3.1 and Corollary 3.1 of [AFM07]. Their logical relation interprets $\mathsf{Cap}\ell \tau$ by a singleton owned store fragment and $\mathsf{Ptr}\ell$ by an empty fragment; the fundamental induction therefore validates the three rules and frames every disjoint store fragment. ◻

For a cell initially containing $7$, swapping in a pair transforms $$\text{before: }\mathsf{Cap}\rho \mathsf{int},\text{after: }\mathsf{Cap}\rho (\mathsf{int}\times \mathsf{int}).$$ An unrestricted reference calculus must keep one fixed content type; it cannot validate this strong update without an additional exclusivity argument.

Proof of Theorem 50.12 — Linear-region safety

Proof. This is Theorem 1 of [FMA06]. The paper reports a Twelf verification for a richer target. The displayed theorem is only target safety; its lexical-region, first-class-region, and unique-pointer encodings are sketches rather than separately stated preservation theorems. ◻

For the paper’s FRGN translation, a stack of regions becomes a nested linear tuple of capabilities. The $\mathsf{letRgn}$ clause allocates a fresh capability, pairs it onto that tuple, translates the body, then projects the same capability and feeds it to $\mathsf{freergn}$. Consequently the one-step interface calculation is $$S{⟼}_{\mathsf{FRGN}}S\otimes \mathsf{cap}\rho {⟼}_{\mathsf{FRGN}}S\otimes \mathsf{cap}\rho {⟼}_{\mathsf{FRGN}}S.$$ The first and last arrows are the displayed allocation and deallocation steps; the middle arrow summarizes accesses that thread the capability. This is a representation calculation at the paper’s translation signature, not a separate theorem for the sketched Cyclone encodings.

Proof of Theorem 50.14 — Monadic-region soundness

Proof. Preservation, progress, and soundness are Theorems 3.1–3.3; translation preservation and closed-program correctness are Theorems 5.1–5.2 of [FM06]. The source proofs carry tower-domain typing through fresh-stack extension and substitute the dead markers on exit. ◻

Parametricity prevents a result of $\mathsf{runRGN}$ from exposing $\gamma$. An existential package could hide a name but still permit the package to escape; the rank-2 interface instead scopes every client of the handle under the quantifier. A one-cell run allocates, reads, and removes its store before returning the integer: $$\mathsf{runRGN}(\mathrm{\Lambda }\gamma .\lambda h.\mathsf{new}h7\gg {=}_{\mathsf{FRGN}}\lambda r.\mathsf{read}r)\Downarrow 7.$$

Affe combines ML inference with affine kinds and scoped shared or exclusive borrows [RST20]. It is a useful modern comparison, but its borrow regions are not a theorem-preserving presentation of either the Tofte–Talpin or WCM calculus.

Sources.

Tofte–Talpin Sections 5.2–5.4 own inference, Milner refinement, and substitution; Sections 7–9 own Theorem 6.1 [TT97]. Walker–Crary–Morrisett Sections 2–3 and technical-report Appendices A–B own capability safety, complete collection, and CPS preservation [WCM00]. The four later designs retain their own signatures and theorem boundaries.