1 Introduction↩︎

Modern safety guarantees often rest on controlling aliasing. Memory safety, deterministic resource management, and data-race freedom all require knowing when computations may touch the same mutable resource. This is hard in languages with unrestricted aliasing: objects cross abstraction boundaries, closures capture mutable state, and higher-order functions defer effects until invocation. The style is expressive, but mutability undermines local reasoning: a write through one reference can silently change what another reads, the familiar “spooky action at a distance”. With deallocation or parallelism, the same aliasing problem may lead to dangling pointers, double-frees, or data races.

Rust [1], [2] shows the value of static alias control. Its ownership and borrowing discipline supports safe resource management, memory safety without a garbage collector, and fearless concurrency [3]. But Rust obtains these guarantees by making exclusivity part of the language’s programming discipline. That design is hard to retrofit into languages where sharing is pervasive.

The tension appears even in a small Rust example. A mutable borrow and a shared borrow of the same value cannot both be live at once. Here a closure logs the vector’s length, with a push between two calls to it:

The closure log_length retains a shared borrow of v until its last call, so the push in between, which mutably borrows the vector, is rejected. The operations are sequenced: no data race or dangling reference can arise. The borrow checker rejects the program because of the alias the closure retains, not because the operations actually interfere. Closures that capture mutable state are a common setting in which shared-xor-mutable reasoning rejects safe higher-order patterns. Rust programmers work around this by restructuring the code or by switching to reference-counted cells with dynamically checked borrows [2], stepping outside the static discipline.

The need for alias control is not specific to systems programming. In higher-level languages, resources such as file handles, buffers, and network connections still call for exclusive access and affine ownership. The goal of this paper is to bring such guarantees to a real-world language where sharing remains the default: Scala. Programmers should be able to require separation or affine use where a resource-sensitive API needs it, without imposing an exclusivity discipline on ordinary code. We build on capturing types [4], [5] (or capture checking) which attach to a value’s type a capture set recording the capabilities the value may use. In this setting, capabilities are ordinary values: the effects code may perform are bounded by the capabilities it holds [6], and capture sets statically track where those capabilities flow. A file handle, a mutable buffer, or a network connection can be treated as a capability; a closure’s type records the capabilities it may exercise.

Capturing types have proven non-invasive and flexible. For higher-order code, effect polymorphism can stay implicit: closures over mutable state can be tracked without changing ordinary higher-order signatures. Capture checking is implemented in the Scala 3 compiler and has been applied to large parts of the Scala standard library [5] retroactively and non-invasively.

What they do not yet provide is exclusive use. Capture sets record which capabilities a value may use, but not whether access is read-only or exclusive, or whether a capability has been consumed. For a parallel combinator, capture sets describe what each closure may touch but cannot prevent both from writing to the same buffer. Likewise, they can record use of a file handle, but not that it has been consumed and its old aliases disabled.

We present System Capybara,¹ a calculus built around tracked capabilities. Drawing on linearity, uniqueness, ownership, and borrowing [7]–[9], Capybara adds selective alias control on top of Scala’s capture checking. Separation requires non-interfering memory footprints, for example when computations are passed to a parallel combinator. Read-only capabilities distinguish reads from writes: read-only uses of the same capability may overlap, and separation rejects an overlap only when one side may write or consume the shared capability. Consume models affinity and ownership transfer: once a capability is consumed, all aliases covered by it become unusable, so a consuming API can treat the capability as fresh. Aliasing remains permitted and tracked by default; separation, read-only access, and consumption are enforced only where an API asks for them. The Rust example above, ported to Capybara with a buffer in place of the vector, type-checks in sequence and is rejected when run in parallel with a write:

The technical challenge is to make these local requirements sound in a higher-order language with subtyping and both implicit and explicit capture polymorphism. We give a type-preserving translation from the surface calculus Capybara to CoreCapybara, a smaller core calculus on which we develop the metatheory, building on System Capless [5]. In the core, implicit and explicit capture polymorphism become universal quantification, consumption and freshness become existential capture, and separation obligations become modal types indexed by explicit constraints. CoreCapybara also guides our Scala 3 implementation: a separation checker that layers separation, consume, and read-only capabilities on the existing capture checker.

Several practical languages now expose substructural information in the type system: Linear Haskell through linear arrows, Swift and Mojo through ownership features, and OxCaml through modes [10]–[14]. OxCaml uses modal types for memory management, data-race freedom, and effects [15], [16]; in Capybara, modal types carry separation constraints over tracked capabilities.

Previous work on capture checking relied on syntactic type soundness [4], [5]. For Capybara, we instead give a semantic model of CoreCapybara, following the logical approach of Timany et al. [17]. In the model, a capture set denotes a runtime footprint: the locations a term may read, write, or consume. Semantic soundness states that well-typed terms produce only traces authorized by their footprints. This theorem, together with confluence of the reduction semantics, is the basis for the formal claims summarized below.

This paper makes the following contributions.

• We introduce System Capybara by example, showing how tracked capabilities support local reasoning about aliases and resources in ordinary Scala code (2).

• We formalize Capybara, a surface calculus that retrofits selective substructural reasoning onto capture checking (3).

• We define CoreCapybara, a compact core extending System Capless [5], and a type-preserving translation from Capybara to the core (4; details in 12).

• We prove semantic soundness for CoreCapybara, mechanized in Lean 4 [18], deriving type safety, memory safety (no use-after-free or double-free), separation, and read-only immutability; confluence gives data-race freedom for well-typed programs (5).

• We describe the implementation of the new Scala 3 separation checker layered on top of capture checking, and exercise it on resource-sensitive and concurrent case studies (6).

[sec:discussion,sec:related-work,sec:conclusion] discuss limitations and design choices, related work, and conclusions.

2 Capybara by Example↩︎

2.1 A Brief Introduction to Capturing Types↩︎

System Capybara extends capturing types [4], [5], so we introduce them first. Capturing types support safe resource and effect programming by recording in a value’s type the capabilities it may use. Resources and effects, such as file handles, mutable state, or control effects, are modeled as capabilities. A capture set lists them: T^$\set{x_1,\dots,x_n}$ denotes a T value that captures at most \(x_1,\dots,x_n\).

For example, given a mutable string buffer buf, the following is a closure that writes to it:

The closure has the capturing type (() -> Unit)^{buf}, often written () ->{buf} Unit. The shape type () -> Unit says that the function takes no argument and returns unit. The capture set {buf} makes it explicit that invoking the function may use the capability buf, and so may write to the buffer. A type whose capture set is non-empty, like () ->{buf} Unit, is called impure, while one with an empty capture set, like () -> Unit, is called pure.

A type system that tracks effects has to support effect polymorphism. A higher-order function such as list map should work whether the mapping operation it receives is pure or effectful. A naive treatment forces every higher-order signature to take an extra effect parameter, prohibitively intrusive for existing code [4]. Capturing types handle this with lightweight effect polymorphism [4], [5]. List map keeps its original signature, yet is effect-polymorphic:

Under the hood, lightweight effect polymorphism rests on subcapturing and root capabilities.

Subcapturing is like subtyping but over capture sets, written {x1,...,xn} <: {y1,...,ym}. At its core it is the subset relation: it holds whenever the left-hand set is a subset of the right. It also relates a variable to what its type captures. Name the closure from before,

so that sayHi has type () ->{buf} Unit. Then {sayHi} <: {buf}. Subsetting and transitivity yield further relations, for instance {} <: {sayHi} <: {buf, io}.

The second ingredient is the root capability any. It subsumes any capability. Therefore, {any} is the top capture set: every capture set is a subcapture of it. Return to def map[B](f: A => B): List[B]. Its parameter type A => B is shorthand for A ->{any} B, a function capturing any. By subcapturing, this signature accepts functions of any captures, pure or effectful, which makes map effect-polymorphic.

Note that map’s result type List[B] stays pure: map is strict, applying f during the call and retaining no reference to it. A lazy operation is different. Consider a function returning an iterator over a buffer’s lines:

Here Buffer^ abbreviates Buffer^{any}, so the parameter accepts any buffer. The iterator reads lines from buf on demand, so it retains the buffer capability. Its type Iterator[String]^{buf} captures buf. Using the iterator therefore produces mutation effects, which the capture set makes explicit.

2.2 Separating Anys From Anys↩︎

Capturing types track which capabilities a value uses, not whether they are separate or fresh. Every capability subcaptures any, so the types alone cannot show two capabilities disjoint.

This matters wherever non-interference does. For instance, consider a function that runs two operations in parallel:

Capturing types record what the two argument functions may use, but enforce no separation constraint between them. Nothing prevents passing two closures writing to the same buffer:

Each closure captures the mutable buffer buf and writes to it, so running the two in parallel is a data race. Ruling out such races calls for tracking separation in capturing types.

This is the gap Capybara closes. On top of capturing types it adds separation checking. It understands any differently: each any in a function’s parameters stands for capabilities separate from those of the other parameters and of the function itself. More concretely, Capybara reads the two anys in runParallel as distinct:

The subscripts are for exposition: they show how Capybara reads the signature internally; the source still writes a plain any. Capybara checks that the capabilities subsumed by the two anys do not interfere. The earlier call violates this: both closures write to buf, so any$_1$ and any$_2$ each subsume {buf} and interfere at buf. Capybara rejects the call with a separation error.

When two operations act on separate resources, Capybara accepts running them in parallel:

Each call to alloc returns a fresh capability (a notion we return to in 2.4), distinct from every other, so {f1} and {f2} are separate. Here any$_1$ subsumes {f1} and any$_2$ subsumes {f2}; the two do not interfere, so the check succeeds, and the parallel computation is indeed safe at runtime.

The obligation paid at call sites, that distinct anys stand for separate capabilities, becomes a guarantee for functions, which may assume distinct anys separate from each other. Consider a function that receives two buffers and updates them in parallel:

Calling runParallel in the body requires buf1 and buf2 to be separate. Capybara accepts the call because the two buffers capture distinct anys (any$_1$ and any$_2$). We call these anys roots. They are treated as separate from every other root in scope. The fresh of alloc is a root as well, a new one at each call, which is why f1 and f2 never alias. Roots are the minimal units of separation and freshness reasoning: two capture sets are separate when they trace back to non-interfering roots. As 2.5 shows, roots correspond to the quantified capture variables of the core calculus.

Capybara provides statically checked, data-race-free parallelism without giving up flexibility: a capability may be shared, provided the sharing is recorded in the types, and exclusivity is demanded only where safety requires it, as at a parallel call.

The following example adapts the Rust example of 1 into Capybara. The closure logSize reads v.size, so it captures v read-only and has type () ->{v.rd} Unit:

Calling logSize, pushing to v, and calling logSize again all type-check: the three run in sequence, and nothing interferes. Capturing types record that logSize has a reference to v, but do not reject the first two uses. Only the last line is rejected, where logSize and the write to v run in parallel and form a read/write conflict at v: separation is enforced when concurrency makes it matter. Where Rust rejects the program for the alias that logSize retains, Capybara rejects only the interfering use. This permissiveness matters for adoption: existing Scala code aliases pervasively, and a discipline that strictly restricts aliasing would be infeasible to adopt.

2.3 Read-Only Capabilities↩︎

Consider the following example, where two parallel operations read from the same buffer:

Both closures use buf, but only for reading, so they are data-race-free.

To accept such programs, Capybara introduces read-only capabilities. A capturing type carries a permission that limits what its value may be used for. It is written as a prefix qualifier on the type, as in ro Buffer^{...}. The permission ro restricts a reference to Buffer’s read-only operations:

f1r is a read-only view of f1, exposing its read-only methods but not its mutating ones. By default, a capability has read-write permission: every Buffer type seen so far omitted the qualifier. A read-write reference (Buffer^) may be used wherever a read-only one is expected (ro Buffer^), but not the reverse. In our Scala 3 implementation, the qualifier is never written but inferred (6.1).

The permission on a type constrains what a value may do. Capture sets instead record how a capability is used. Concretely, a capture set tags each of its elements with an access mode, which is either read-only or read-write. We write a read-only use with the suffix .rd. For instance, the closure () => f1.size calls a read operation of f1, so it has the capturing type () ->{f1.rd} Int.

Separation checks treat two read-only uses of the same capability as non-interfering, a principle familiar from fractional permissions [19], so the snippet type-checks. A read-only use concurrent with a read-write one still conflicts.

2.4 Always Consume Your Capabilities Fresh↩︎

Recall the two calls to alloc from before: each returned a fresh capability. Freshness is a global property. A fresh capability is aliased by nothing, so it is separate from anything else in the program. Capybara records this guarantee in the capture set with the special element fresh, as in Buffer^{fresh}. The element appears only in the result type of a function, as in alloc’s signature () -> Buffer^{fresh}: it states that every call returns a fresh capability.

There are two ways to obtain a fresh capability. The first is to create one outright: a constructor can return its newly allocated resource as fresh, since nothing in the program could alias it yet.

The second is to consume an existing capability. A parameter marked consume disables every other reference to its argument, so a reference returned by the call may be treated as fresh.

The call merge(f1, f2) consumes both buffers, so any later use of f1 or fn is rejected. With f1 and f2 disabled, nothing can reach the buffers through them, so the capability returned as f is fresh: the implementation of merge can freely assume that no other aliases exist for its two arguments, and return one of them exactly as if it had just been created.

Consuming a capability is allowed only when it is fresh. For instance, a parameter typed Buffer^ is separate but not fresh: the caller may still hold other references, so consuming it is rejected.

The parameter grants full read-write access, so the append succeeds. But merge would consume acc, and buildStr received acc as an argument that other code may still alias. Only a capability the function owns, one freshly created or passed under consume, may be passed to merge.

The three disciplines of this section are analogous to Rust’s three kinds of references. An owned value is a fresh capability: f returned by merge above owns its buffer. Only owned capabilities may be consumed, which is the counterpart of a move. A mutable borrow &mut Buffer is a tracked read-write alias, e.g. g: Buffer^{f}: it may read and write the buffer but not consume it, and it conflicts with every concurrent use of f. A shared borrow &Buffer is a read-only view, e.g. g: ro Buffer^{f.rd}: it may overlap with other reads, but not with writes. The disciplines differ in how exclusivity is enforced: Rust enforces shared-xor-mutable throughout each borrow’s lifetime; Capybara tracks aliases and demands exclusivity only at a consume or a separation check.

2.5 Capybara under the Hood↩︎

The language presented so far is a surface language that translates to a core calculus, CoreCapybara, which gives any, ro, consume, and fresh an explicit semantics. We preview the translation informally.

In the core, the translation of runParallel uses capture quantifiers for root capabilities and a modal type for separation, in the style of contextual modal type theory [20]:

The subscripted any$_1$ and any$_2$ of 2.2 are now explicit capture parameters, which a call instantiates with the arguments’ actual capture sets. The result is a modal type \([\Psi]\,T\), a \(T\) usable only under the separation constraint \(\Psi\), where \(C_1 \bowtie C_2\) constrains two capture sets to be separate; to run the function, the caller must prove {c$_1$} $\bowtie$ {c$_2$}. Dually, a fresh in a result type is existentially quantified: the result type of alloc translates to \(\exists c.\,\)Buffer^{c}, a buffer using some fresh capability, and binding the result unpacks the package, introducing a capture variable that nothing else in scope can mention. 12.9 gives the full translation.

A consume parameter receives an owned capability, so its any is quantified existentially rather than universally: the function translates to a consumer, whose argument arrives as a package and is unpacked on entry. The signature of the merge function in 2.4 becomes

The call site types each argument at Buffer^{fresh} and packs it with its capability: merge(f1, f2) translates to merge($\langle${f1}, f1$\rangle$, $\langle${f2}, f2$\rangle$). Packing consumes the witness, which disables f1 and f2.

3 Formalizing Capybara↩︎

This section formalizes Capybara, the surface language of 2. Its core calculus CoreCapybara, used for the metatheory, follows in 4.

[fig:syntax] gives the abstract syntax of Capybara. Its static semantics is split across three figures. 1 presents the main judgments: subcapturing, subbounding, term typing, and subtyping. 2 gives the capability-specific rules: kinding, separation, and sequential composition. 4 types the memory primitives, parallel composition, and conditionals (3.4).

None

3.1 Syntax↩︎

Capybara is a variant of CC\(_{<:\Box}\), the calculus of capturing types [4], extended with mutability permissions, consumption, and separation. Like CC\(_{<:\Box}\), its terms are in monadic normal form (MNF): applications operate on variables, and intermediate results are named by let bindings. The normal form matters for application, whose result type may mention the parameter. When the argument is a variable \(y\), the result type is the exact substitution \([x:=y]U\). MNF induces no loss of expressiveness, since a general application \(t_1\,t_2\) can always be written \(\LET x_1 = t_1 \IN \LET x_2 = t_2 \IN x_1\,x_2\).

A term is a variable, a value, an application, a type or capture application, a memory primitive, a parallel composition, a conditional, or a let-binding. A value is a term lambda, a type lambda, a capture lambda, or a constant. The memory primitives and parallel composition are typed in 3.4. The parameter of a term lambda carries a consume mode \(\alpha\), recording whether the argument may only be accessed (\(\epsilon\)) or also consumed (\(\CONSUME\)). 3.3 formalizes consume.

A capturing type \(m\,S\capt C\) consists of a permission \(m\) qualifying the type, a shape type \(S\), and a capture set \(C\); we omit the default permission \(\epsilon\) and write \(S\capt C\). The permission constrains what the value may be used for: by default a value is read-write (\(\epsilon\)), and the read-only permission \(\RO\) restricts it to non-mutating operations (recall 2.3’s ro Buffer^{...}). Mutabilities are ordered by a reflexive relation \(\preceq\), generated by \(\RO\preceq\epsilon\): read-only is the weaker of the two. The capture set over-approximates the capabilities a value of this type may use and at what access modes: each element \(\mu\,\theta\) pairs a capture \(\theta\) with an access mode \(\mu\). A mutability marks an access to a capability: \(\epsilon\,\theta\) uses it read-write, \(\RO\,\theta\) read-only. \(\CONSUME\,\theta\) instead marks that the capability is consumed.

Shape types include the top type, type variables, the three function types (term, type, and capture functions), reference types \(\REF[T]\), and the base types \(\TBOOL\) and \(\TUNIT\). A capture bound \(B\), used to bound a capture parameter, is either a concrete capture set or a mutability. For instance, \(\lambda[c<:\RO]t\) bounds \(c\) by capabilities with at most read-only access. Capability kinding (presented shortly) makes precise which capture sets a mutability bound accepts.

3.2 Typing, Subtyping and Subcapturing↩︎

Subcapturing \(\subs{\G}{C_1}{C_2}\) is a preorder. It subsumes set inclusion ( and ). resolves a variable to the capture set it was declared with: \(x:m\,S\capt C\in\G\) gives \(\subs{\G}{\set{x}}{C}\). and concern qualified capture sets. Qualifying \(\mu\,C\) restamps every element of \(C\) with the access mode \(\mu\): \[\begin{align} \epsilon\,C &= C & \RO\,C &= \set{\RO\,\theta \mid \mu\,\theta\in C} & \CONSUME\,C &= \set{\CONSUME\,\theta \mid \mu\,\theta\in C}. \end{align}\] lets a capture set be qualified down to a weaker mode, since \(\RO\preceq\epsilon\); extends this to a congruence under qualifying.

Subbounding \(\subs{\G}{B_1}{B_2}\) extends subcapturing to capture bounds \(B\). orders mutability bounds the same way as mutabilities; admits a capture set below a mutability bound \(m\) once it carries kind \(m\), a judgment defined at the end of this subsection. This is how \(c\) in \(\lambda[c<:\RO]t\) can be instantiated by any read-only capture set.

The judgment \(\typ{C}{\G}{t}{T}\) states that \(t\) evaluates to a value of type \(T\) with use set \(C\), the set of capabilities exercised during the evaluation of \(t\). types \(x\) at \(\set{x}\), refining its declared capture set to the singleton \(\set{x}\) and keeping its permission. types the same occurrence \(x\) at a read-only view instead, charging \(\set{\RO\,x}\). This formalizes the .rd suffix of 2.3, which is expository, not concrete syntax. is ordinary subsumption, weakening the use set and type subject to target well-formedness \(\wf{\G}{\cdot}\).

and give the \(\ANY\) mechanism of 2 its formal content. Both rest on root capability instantiation. A root capability occurs as an element \(\mu\,\ANY\) (or \(\mu\,\FRESH\)) of a capture set inside a type. Instantiating an occurrence with a capture set \(D\) replaces the element by \(D\) qualified at its mode: \[C[\ANY\leadsto D] = (C\setminus\set{\mu\,\ANY})\cup\mu\,D \qquad\text{where }\mu\,\ANY\in C,\] descending compositionally through all other capture sets and type formers. \(T[\ANY\leadsto D_1,\ldots,D_n]\) instantiates the \(n\) occurrences of \(\ANY\) in \(T\), read left to right, with \(D_1,\ldots,D_n\) respectively. The single-set form \(T[\ANY\leadsto D]\) gives every occurrence the same \(D\). \(\FRESH\)-instantiation is defined the same way. Intuitively, the two root capabilities stand for capture quantification, \(\ANY\) universal and instantiated by the caller, \(\FRESH\) existential and witnessed by the function body; the translation to CoreCapybara makes this reading literal (12).

Abstracting \(\lambda(\alpha\,x:T)t\) binds a fresh capture variable \(c\), mutability-bounded (\(\alpha\,c<:\epsilon\)), and checks the body against \(T\) with every \(\ANY\) in it instantiated to \(\set{c}\), written \(T[\ANY\leadsto\set{c}]\). At a call \(x\,y\), requires \(y\)’s type to have the form \(T[\ANY\leadsto D]\) for some access-only \(D\) separated from the callee’s spine capture set \(|(\forall(z:T)U)\capt C|\); 3.3 defines both judgments.

gives the \(\FRESH\) of 2.4 its formal content: it widens concrete capture sets to \(\FRESH\). A variable \(x\) declared at \(T[\FRESH\leadsto D_1,\ldots,D_n]\), an instance of the \(\FRESH\)-carrying type \(T\) with concrete witnesses \(D_1,\ldots,D_n\), can be typed at \(T\) itself. This is how merge returns one of its arguments at Buffer^{fresh}. The widening consumes the witnesses: each \(D_i\) must be access-only and consumable, and the rule charges \(D\cup\CONSUME\,D\) for \(D=D_1\cup\cdots\cup D_n\). The witnesses must moreover be pairwise disjoint (3.3), so that distinct \(\FRESH\)es never overlap.

types let bindings and opens \(\FRESH\)-carrying types such as the Buffer^{fresh} of 2.4. A binding \(\LET x=t\IN u\) binds \(x\) at \(T[\FRESH\leadsto\set{c_1},\ldots,\set{c_n}]\) for new consumable capture variables \(c_1,\ldots,c_n\), one per \(\FRESH\) that \(t\)’s declared type \(T\) carries. Distinct \(\FRESH\)es thus resolve to distinct roots: each names its own freshly created resource, which the continuation may access and consume independently of the others. The rule also sequences the use of \(t\) before that of \(u\) (\(\seqcomp{\G}{C_1}{C_2}\), 3.3), which enforces the consume semantics: nothing \(t\) consumes can be used in \(u\).

, , , and abstract and apply over type and capture parameters. is analogous to , abstracting over a capture parameter \(c\) bounded by \(B\); mirrors , requiring the instantiating capture set \(D\) to be separated from the callee’s own footprint and charging \(D\) alongside the callee.

Note that the abstraction rules have the empty use set: a lambda is already a value, so evaluating it uses no capabilities, and the body’s use set becomes the capture annotation of the function type. This makes the types of curried functions precise. Assume a capability \(\textsf{a}\), invoked by applying it to unit, and consider \(\lambda(z_1{:}\TUNIT)\,\lambda(z_2{:}\TUNIT)\,\textsf{a}\,z_2\). The inner body uses \(\set{\textsf{a}}\), so the term has the capturing type \[\forall(z_1{:}\TUNIT)\,(\forall(z_2{:}\TUNIT)\,\TUNIT)\capt\set{\textsf{a}},\] whose outer function is pure: the use of \(\textsf{a}\) is charged to the arrow whose application performs it.

The same precision means the outermost capture set of a function type understates what calling the function can do: the type above is pure at top level, yet applying the function and then its result exercises \(\textsf{a}\). The footprint that and check separation against is therefore the spine capture set \(|T|\), the capabilities \(T\) mentions along its spine: \[\begin{align} |\top| = |X| = |\TBOOL| = |\TUNIT| &= \set{} & |\forall[X<:S']U| &= |S'|\cup|U|\\ |m\,S\capt C| &= \mfree{C}\cup|S| & |\forall[c<:B]U| &= |U|\setminus c\\ |\forall(x:m\,S\capt C)U| &= \mfree{C}\cup(|U|\setminus x) & |\REF[T]| &= |T| \end{align}\] where \(\mfree{C}\) removes the root capabilities \(\ANY\) and \(\FRESH\) from \(C\). The recursion walks the spine of nested arrows, type bounds, and reference contents, unioning the capture set at each domain and codomain, so \(|T|\) collects every capability a value of type \(T\) can eventually use, not only those its outermost capture set names. Two kinds of elements are dropped along the way: the variables that nested binders introduce and the root capabilities. and type a function body treating its parameter as separate from the rest of the function. Checking the argument against the whole spine is what makes that assumption good at every later application.

Subtyping \(\subs{\G}{T_1}{T_2}\) has the usual reflexive-transitive shell , , a type variable rule , and one congruence per shape , , . Type and capture functions are contravariant in their bounds and covariant in their bodies under the extended context. Term functions are invariant in their domains: a function body treats its parameter’s capture set as a separation assumption (3.3), and narrowing the domain by subtyping would strengthen that assumption behind the function’s back. Call sites lose no flexibility, since still adapts an argument to the declared domain, and a function can always be \(\eta\)-expanded at a narrower domain. lifts shape subtyping and subcapturing to capturing types, \(\subs{\G}{m\,S_1\capt C_1}{m\,S_2\capt C_2}\) from \(\subs{\G}{S_1}{S_2}\) and \(\subs{\G}{C_1}{C_2}\), but keeps the permission \(m\) fixed on both sides. Consequently, subtyping alone can never turn a read-write value into a read-only one; only , applied to a variable occurrence, weakens a permission, and only weakens an access mode inside a capture set.

The judgment \(\typs{\G}{C}{m}\) certifies that the capabilities in \(C\) are used at most at mutability \(m\): kind \(\RO\) means \(C\) contains only read-only uses, while kind \(\epsilon\) also admits read-write uses and thus holds of every capture set . A set qualified read-only has kind \(\RO\) , and a capture variable declared with a mutability bound inherits that bound as its kind , so \(c<:\RO\in\G\) gives \(\set{c}:\RO\). Kinding is closed under union and inherited along subcapturing : a set below one of kind \(m\) itself has kind \(m\).

3.3 Separation and Consume↩︎

\(\sep{\G}{C_1}{C_2}\) certifies that two capture sets do not interfere. The check traces both sets back to their roots and compares the roots pairwise. The tracing is done by : to separate a set, it suffices to separate a set above it in subcapturing, in particular the roots it resolves to. makes the rule available on both sides. and then decompose the root sets into pairs of individual roots. Two leaves close the derivation. separates any two distinct roots: roots are the basic carriers of separation guarantees. separates any two access-only sets of kind \(\RO\), so capabilities may overlap freely at read-only mode.

\(\disj{\G}{C_1}{C_2}\) is the fragment of separation without . It admits no read-only sharing: two read-only views of the same capability are separate but not disjoint. Disjoint sets thus hold genuinely distinct capabilities, and uses it to keep its witnesses apart.

\(\seqcomp{\G}{C_1}{C_2}\) asks whether a computation using \(C_1\) can safely run before one using \(C_2\). This judgment is where the static semantics enforces consume: reads and writes end with the first computation, but a consumed capability stays gone, and nothing that runs later may use it. checks the judgment between a bound term and its continuation, between consuming the argument and the call itself. The check follows the same scheme as separation: traces \(C_1\) back to its roots, splits them, and two leaves decide. A part that consumes nothing is harmless ; a part that consumes must be separated from \(C_2\), keeping what it consumes unusable in the computation that follows .

\(\accessonly{\G}{C}\) holds when every capture variable \(C\) resolves to is tagged with a mutability rather than \(\CONSUME\) , and is closed under union and subcapturing. \(\consumable{\G}{C}\) holds when every capture variable \(C\) resolves to is declared with consume mode \(\CONSUME\) . The typing rules require access-only sets wherever they instantiate \(\ANY\), \(\FRESH\), or a capture binder: the witness \(D\) of , , and , and the witnesses of . A \(\CONSUME\)-qualified capability is more than a permission to access: using it kills the capability. Hiding one inside the instance of a capture variable would make the kill invisible, since an occurrence of the capture variable reads as a plain access, and nothing would record that using a set mentioning it may consume capabilities.

In the program of 3 (left), each \(\textsf{alloc}\) result carries one \(\FRESH\), so binds \(f_i : X\capt\set{c_i}\) with distinct consumable roots \(c_1\neq c_2\). At the first application \(\textsf{rp}\,f_1\), instantiates \(\ANY\) with \(D = \set{f_1}\), and the separation premise is trivial: the spine capture set of \(\textsf{rp}\)’s type is empty. The binding types \(g\) at \((\forall(op_2:X\capt\set{\ANY})\,\TUNIT)\capt\set{f_1}\): the partial application has captured \(f_1\). The second application \(g\,f_2\) is where separation is enforced: \(D = \set{f_2}\) meets the spine \(\set{f_1}\), and \(\sep{\G}{\set{f_2}}{\set{f_1}}\) follows because resolves each \(f_i\) to its root, separates the distinct roots, and carries the conclusion back. Passing the same resource twice would instead demand \(\sep{\G}{\set{f}}{\set{f}}\), which no rule derives. 4 returns to this program in its core form (3, right); 12.9 traces its translation.

3.4 Mutable State and Parallelism↩︎

None

The calculus so far manages capabilities but has no concrete effects. Mutable references, parallel composition, and conditionals give its guarantees operational content (4).

A reference of type \(\REF[T]\capt C\) is a mutable cell holding a \(T\). Allocation creates a fresh one: types \(\ALLOC x\) at \(\REF[T]\capt\set{\FRESH}\), so the receiving let binding names the new cell by a consumable capture variable of its own . Deallocation is the primitive consumer: requires \(\set{x}\) consumable and charges \(\set{\CONSUME\,x}\), after which sequential composition keeps the dead reference out of reach. Reading is a read-only effect: accepts a reference of either permission and charges the read-only view \(\set{\RO\,x}\). Writing requires the read-write permission and charges \(\set{x}\) .

The term \(\PAR t_1, t_2\) runs its two branches concurrently. requires the use sets of the two branches to be separated: two computations may run in parallel exactly when separation certifies that their capabilities do not interfere. Conditionals are standard . All these constructs carry over to the core calculus (4), whose dynamic semantics gives them operational meaning.

4 The Core Calculus CoreCapybara↩︎

CoreCapybara is the target of the type-preserving translation (12) and the calculus for our metatheory (5). It is a variant of System Capless [5], inheriting existential capture types, and shares the surface calculus’s monadic normal form. It makes surface contracts explicit: separation becomes modal types, freshness existential capture types, and read-only views reader values. We present only the constructs and judgments without surface counterparts; 10 gives the complete definitions, which follow the Lean mechanization.

4.1 Syntax and Judgments↩︎

[fig:core-syntax-delta] gives the delta over Capybara; [fig:core-syntax] gives the complete syntax. CoreCapybara carries over the surface abstractions, memory primitives, parallel composition, and conditionals, but replaces root capabilities with existential packs and unpacks, modal locks and unlocks, and reader values. A capture binding \(\alpha\,c<:B\) is access-only (\(\epsilon\)), consumable (\(\CONSUME\)), or killed (\(\KILLED\)); killed bindings arise only during typing.

The judgments of 3 carry over, with result types extended to existentials. Subcapturing also resolves access-only capture variables to their bounds and forgets read-only qualifiers . Below we give the changes to separation and the new satisfaction judgment \(\sat{\G}{[\Psi,\Phi]}\).

4.2 Modals and Separation↩︎

Separation \(\sep{\G}{C_1}{C_2}\) concludes at three leaves:

,̏C_1C_2 ,̏ ,̏C_1C_2

separates two read-only sets, while separates distinct consumable capture variables and replaces the surface . reads a modal lock’s assumptions: the entries of \(\Psi\) are pairwise separate, while \((C:m)\in\Phi\) bounds \(C\)’s kind by \(m\).

types its body under the recorded assumptions; eliminates the modality when those assumptions are satisfied, as defined by :

Locks make surface separation checks compositional. A translated function assumes that its parameter is separate from the function’s footprint; each call discharges that assumption at an unlock, which implements the separation premise of (12).

4.3 Consume, Freshness, and Existentials↩︎

A consumable capture variable may be consumed once. The kill operation marks every consumable root of \(C\) as killed: \[\G\ominus C \mathrel{\vcenter{:}}= \G\big[\;\alpha\,c<:B \;\mapsto\; \KILLED\,c<:B \;\big|\; \CONSUME\,c\in\roots{\G}{C}\;\big],\] where \(\roots{\G}{C}\) resolves the term variables of \(C\) through their capture sets until only capture variables remain (10). Killed variables may be neither accessed nor consumed.

therefore makes anything consumed by the bound term unusable in its continuation.

Fresh results are existential packages, introduced by packs and eliminated by unpacks:

consumes pairwise-disjoint witnesses and hides them behind existential capture variables, the premise that already imposes on the surface. The core disjointness judgment drops the lock leaf , so disjointness never rests on modal assumptions: each witness is a resource of its own, not a shared view. binds the witnesses as fresh consumable variables and records the freshness lock \([\Psi_w,\emptyset]\), making the witnesses separate from the continuation’s charge \(C_2\) (2). Accordingly, surface occurrences translate to packs and fresh roots introduced by translate to unpacks (12). A consumer lambda is a first-class unpacking function and the translated form of a \(\CONSUME\)-mode function:

binds the witness as a consumable root; sequences argument consumption before access to the consumer, preventing the former from disabling the latter.

In the core form of the running example (3, right), the body of \(\textsf{rp}\) is typed under \(\LOCK[\Psi,\emptyset]\), where supplies the separation of \(\set{d_1}\) from \(\set{d_2}\) that the surface program assumes. The two unpacks bind \(f_i : X\capt\set{c_i}\) with distinct consumable roots, and the applications instantiate \(d_1:=\set{f_1}\) and \(d_2:=\set{f_2}\), leaving \(g_4 : ([\Psi',\emptyset]\,\TUNIT)\capt\set{f_1,f_2}\) with the concrete lock \(\Psi' = (\set{f_1},\set{f_2})\). The final demands its satisfaction, \(\sep{\G}{\set{f_1}}{\set{f_2}}\): resolves each \(f_i\) to its root, and separates the two. Had both arguments been the same resource, the entries of \(\Psi'\) would share a root, and unlocking would be underivable.

4.4 References and Readers↩︎

Memory primitives keep their surface typing except where explicit core constructs take over. Allocation returns the fresh reference as a one-variable package:

Unpacking introduces a consumable capture variable; read-only views become reader values:

translates the surface view. The other constructs carry over, but memory operations require accessible, hence non-killed, references (10).

4.5 Dynamic Semantics↩︎

Evaluation runs a term against a heap, a finite map from locations to cells: \[H(l) \;::=\; v \;\mid\; \refcell{l'} \;\mid\; \deadcell{l'},\] A cell stores a value, a live reference to \(l'\), or a dead reference left by deallocation. At runtime, term variables additionally range over heap locations: monadic normal form lifts every intermediate value into a heap cell of its own (rule in 10), so a location acts as the runtime name of a value and reference cells store locations. A step from \(\cfg{H}{t}\) emits a trace of its accesses: \[\tau \;::=\; \cdot \;\mid\; e;\,\tau, \qquad\qquad e \;::=\; \RO\,l \;\mid\; \epsilon\,l \;\mid\; \ALLOC l \;\mid\; \DEALLOC l.\] The events \(\RO\,l\), \(\epsilon\,l\), \(\ALLOC l\), and \(\DEALLOC l\) record reads, writes, allocation, and deallocation, respectively; only memory primitives emit them:

Access and deallocation require a live cell. leaves a dead cell that matches no such premise, making use-after-free and double-free stuck.

With the location-only branch footprints \(C_1\) and \(C_2\) from , a left branch steps as follows:

Its trace must be authorized by the branch’s footprint: \[\begin{array}{lcl} \tauth{\cdot}{C} &\text{iff}& \text{true}\\ \tauth{(\mu\,l)\,\tau}{C} &\text{iff}& \mu\preceq\mu'\;\text{for some}\;\mu'\,l\in C,\;\text{and}\;\tauth{\tau}{C}\\ \tauth{(\ALLOC l)\,\tau}{C} &\text{iff}& \tauth{\tau}{C\cup\set{\epsilon\,l,\CONSUME\,l}}\\ \tauth{(\DEALLOC l)\,\tau}{C} &\text{iff}& \CONSUME\,l\in C\;\text{and}\;\tauth{\tau}{C} \end{array}\] Thus accesses require a sufficient mode, deallocation requires \(\CONSUME\), and allocation grants full rights to the new cell. The branch footprints must also be non-interfering: \[\nintf{C_1}{C_2} \quad\text{iff}\quad l_1\neq l_2\;\text{or}\;\mu_1=\mu_2=\RO \quad\text{for all}\;\mu_1\,l_1\in C_1\;\text{and}\;\mu_2\,l_2\in C_2,\] so a shared location is read-only in both. After a step, the footprint grows with newly allocated cells: \(C_1' = C_1\cup\set{\epsilon\,l,\CONSUME\,l\mid \ALLOC l\;\text{occurs in}\;\tau}\). is symmetric, and returns unit once both branches are answers. Well-typed programs satisfy authorization and non-interference, the conditions underlying confluence (5).

\(\redsto{\tau}\) is the reflexive-transitive closure of small-step reduction. Its sequential restriction \(\seqredsto{\tau}\) schedules a right branch only after the left reaches an answer. 10 gives both the complete relation and its big-step counterpart \(\evalsto{\tau}\), which follows the same schedule. Confluence (6) transfers results from sequential to arbitrary runs.

5 Metatheory↩︎

We prove CoreCapybara sound semantically [17]: the fundamental theorem gives type safety, memory safety, and immutability. We then prove confluence of the reduction semantics, which gives data-race freedom. The core development is mechanized in Lean 4 [18].² We sketch the model and results, then give the type-preserving translation that transfers them to Capybara. 11 contains the full model and its Lean correspondence; 12 proves the translation on paper.

5.1 A Logical Model of CoreCapybara↩︎

None

5 collects the definitions of the model. First, a capture set \(C\) denotes a footprint \(\fdenot{C}^H\), a capture set whose elements mention only heap locations (4); we omit the heap annotation when it is clear. A reference cell contributes itself but not its content, and a stored value contributes the footprint recorded when it was lifted, so the interpretation closes transitively over the heap; applying the mode \(\mu\) restamps every element a location contributes (3). The use set’s footprint thus lists every cell a term may touch and at what mode.

Next, a type \(T\) denotes a predicate \(\vdenot{T}\) on answers, relative to a world \((\Sigma,H)\): the runtime heap \(H\) and a store typing \(\Sigma\) assigning each reference cell a predicate for its content. The step index \(k\) breaks the circularity between store typing and type interpretation [21], [22] (\(\mathit{Rel}_k\) in 5). Evaluation moves to future worlds, related by the extension \(\wext{\Sigma'}{H'}{\Sigma}{H}\): it preserves the store typing and stored values, while a reference cell may change its content and may die but not revive; denotations are stable under extension. \(\vdenot{T}\) is also relative to a semantic environment \(\rho\), mapping term variables to locations, type variables to predicates, and capture variables to footprints. Altogether, \(a\in\vdenot{T}_\rho(k,\Sigma,H)\) reads: the answer \(a\) behaves as a \(T\)-value at \((\Sigma,H)\), for runs performing fewer than \(k\) reads; the expression denotation below makes this reading precise.

An answer names a value either directly or through a location, and the partial function \(\resolve\) recovers it. 5 shows a selection of the clauses; the remaining ones follow the same patterns (11). A reference is a cell location in the footprint \(\fdenot{C}\) of its capture set, and the denotation of its content type agrees with the predicate the store typing assigns, \(\Sigma(l)\approx_k\vdenot{T}_\rho\), at every lower index: the forward direction of the agreement types the value a read returns, the backward direction lets a write re-establish a well-typed store, and exposing contents only below the current index is what makes a read consume one unit of \(k\).

The clause for functions shows the Kripke structure: for every argument, the body is judged in every future world, so a stored function remains usable however memory evolves. The truncation \(\lfloor\Sigma\rfloor_j\) turns a world at index \(k\) into one at index \(j\); \(\memtyped{j}{\Sigma'}{H'}\) states that the world is well-typed, chiefly that every live cell’s content satisfies its assigned predicate; and a footprint is live when no cell it mentions is dead, so a call requires the captured cells to be still allocated (11). \(\edenot{E}\) is the expression denotation, defined below; its budget, here the closure footprint \(R_0\) of the abstraction’s capture annotation, upper-bounds the cells the body may touch once applied.

An existential package \(\EXCAP{c_1,\ldots,c_n}T\) requires pairwise disjoint witness footprints.

The expression denotation \(\edenot{E}^{R}\) lifts \(\vdenot{E}\) from answers to expressions: an expression inhabits it when it evaluates to an answer in \(\vdenot{E}\) while accessing only the locations in \(R\). \(\readsof{\tau}\) counts the read events of \(\tau\), and \(\safe{k}{H}{t}\) states that evaluation from \(\cfg{H}{t}\) does not get stuck within \(k\) reads (11). The trace clause \(\tauth{\tau}{R}\) (4) makes the use set operational: every access and every deallocation a run performs is charged to the budget at its declared mode.

The evaluation relation here is the sequentially scheduled big-step semantics (4), so the model constrains sequential runs only. Its guarantees extend to arbitrary interleavings through confluence (6): an interleaved run joins against a sequential run that the model provides, and either steps further or coincides with its answer up to a renaming of locations (11.7).

Finally, semantic typing \(\semtyp{C}{\G}{t}{E}\) lifts the interpretation to open terms, quantifying over every world and every environment \(\rho\) that realizes \(\G\): each binding inhabits its denotation, and distinct consumable capture variables denote disjoint footprints (11).

5.2 Soundness and Memory Safety↩︎

The proof is by induction on typing, with one compatibility lemma per rule.

These live-cell requirements rule out use-after-free and double-free.

The model also yields immutability: a read-only run cannot change the state it started with.

Allocation remains allowed: the program may create and use new cells freely; immutability concerns only the initial cells.

5.3 Separation and Concurrency↩︎

The footprint reading makes the separation judgment precise.

Non-interference of footprints is exactly the side condition of the parallel reduction rules (4), so by 4 a well-typed parallel composition never blocks on it. The two scheduling theorems below assume no typing, only well-formedness: \(\cfg{H}{t}\) is well-formed when every location \(t\) mentions is allocated in \(H\). They are stated up to trace equivalence: \(\tau_1\treq\tau_2\) when both traces perform the same per-location sequence of accesses and deallocations, ignoring events on cells the trace itself allocated (11.8); equivalent traces reorder only independent events.

Confluence makes scheduling unobservable in well-typed runs, yielding data-race freedom.

5.4 Translating Capybara to CoreCapybara↩︎

The translation \(\embed{\cdot}\) explains the separation and freshness reasoning of the surface calculus in terms of the core constructs that our logical model grounds, and carries the formal results of this section over to Capybara. This subsection presents its shape; 12 gives the full definitions and proofs.

Types translate in two variants. The plain translation \(\embed{T}\) serves domains and other invariant or contravariant positions, where \(\FRESH\) cannot occur. The result translation \(\eemb{T}\) closes \(\FRESH\) occurrences into existentials in covariant positions, including let-bound and function-result types: \[\eemb{T} = \EXCAP{c_1,\ldots,c_n}\,\embed{\freshinst{T}{\set{c_1},\ldots,\set{c_n}}},\] binding one capture variable per \(\FRESH\) occurrence, where \(\freshinst{T}{\cdots}\) instantiates the occurrences left to right (3.2). A \(\FRESH\)-free type translates plainly. Existential quantification is thus the meaning of \(\FRESH\), and universal quantification the meaning of \(\ANY\). Function types show both, together with the insertion of modal types: \(A = (\forall(x:T)U)\capt C\) translates to \[\embed{A} = \Big(\forall[\cstar<:\top]\; \forall\big(x:\embed{\anyinst{T}{\set{\cstar}}}\big)\; ([\Psi_A,\Phi_A]\,\eemb{U})\capt W_A\Big)\capt \embed{C}.\] The bound capture variable \(\cstar\) instantiates the \(\ANY\) of the domain, so the caller supplies the argument’s witness explicitly. The result becomes a modal type carrying the manufactured lock \(\Psi_A = (\set{\cstar},\,\langle R_A\rangle)\), where \(R_A\) resolves the arrow’s own capture annotation and domain captures to their roots and \(\langle R_A\rangle\) lists them as one entry per root: the parameter is separate from each root the function reaches, and those roots are pairwise separate. The lock is shallow: it reads only the arrow’s own annotation and domain, and a separation that a nested closure relies on lives in the nested arrow’s own lock, paid where that arrow is eliminated. The annotation \(W_A = \set{\cstar}\cup\embed{R_A}\) is the same root set read as a capture set, the resolved body charge of . For \(c<:\top\) and \(f:\REF[\TBOOL]\capt\set{c}\), the three binder forms instantiate this scheme as follows, with \(R_A=\roots{\G}{\set{f}}=\set{c}\): \[\begin{align} \text{\bfseries Term}\quad &\embed{(\forall(x:\top\capt\set{\ANY})\,\TUNIT)\capt\set{f}}\\[-2pt] &\quad= \Big(\forall[\cstar<:\top]\, \forall(x:\top\capt\set{\cstar})\, ([\Psi,\emptyset]\,\TUNIT)\capt\set{\cstar,c}\Big)\capt\set{f}, \qquad \Psi=(\set{\cstar},\set{c}) \\[5pt] \text{\bfseries Capture}\quad &\embed{(\forall[c'<:\RO]\,\TUNIT)\capt\set{f}}\\[-2pt] &\quad= \Big(\forall[c'<:\top]\, ([\Psi,\Phi]\,\TUNIT)\capt\set{c',c}\Big)\capt\set{f}, \qquad \Psi=(\set{c'},\set{c}), \quad \Phi=(\set{c'}:\RO) \\[5pt] \text{\bfseries Consume}\quad &\embed{(\forall(\CONSUME\,x:\top\capt\set{\ANY})\,\TUNIT)\capt\set{f}}\\[-2pt] &\quad= \Big(\forall\big(\<\cstar,x\>:\EXCAP{\cstar}\,\top\capt\set{\cstar}\big)\, ([\Psi,\emptyset]\,\TUNIT) \capt\set{\cstar,\CONSUME\,\cstar,c}\Big)\capt\set{f},\\[-2pt] &\Psi=(\set{\cstar,\CONSUME\,\cstar},\set{c}). \end{align}\] Here \(\ANY\) introduces a witness separated from \(f\)’s root, an \(\RO\) bound translates to \(\top\) while \(\Phi\) keeps its read-only assumption, and a consume parameter becomes a consumer that may consume the argument’s root.

Term translation is directed by the typing derivation: a surface variable may be typed by , , or , and the translated term depends on which. Write \(\embed{\G}^{\LOCK}\) for the translated context interleaved with the locks that the enclosing translated binders push.

The use sets agree up to root covering: \(P\sqsubseteq P'\) when \(P'\) covers every element of \(P\) at an equal or stronger mode. Most proof cases are homomorphic; the interesting ones synthesize the explicit constructs of 4. A occurrence, retyping \(x\) from \(T[\FRESH\leadsto D_1,\ldots,D_n]\) to \(T\), synthesizes a pack that consumes the witnesses, \(\embed{x} = \<\embed{D_1},\ldots,\embed{D_n},x\>\), and a \(\FRESH\)-carrying translates to an unpack. A occurrence synthesizes a reader value, \(\embed{x} = \RO\,x\). An application supplies the argument’s \(\ANY\)-witness \(D\) to the callee, applies it, and unlocks the result: \(\embed{x\,y} = \LET x_1 = x[\embed{D}]\IN \LET x_2 = x_1\,y\IN \UNLOCK\,x_2.\) The final unlock is where the separation premise of is paid: the instantiated lock demands \(\embed{D}\) separate from each root of \(R_A\), the translated image of \(\sep{\G}{D}{\,|(\forall(x:T)U)\capt C|\,}\) at the shallow part of the spine, with the deeper parts paid at the unlocks of the nested arrows. On the running example (3), the second application \(g\,f_2\) expands to exactly this shape, and its unlock demands \(\sep{\G}{\set{f_2}}{\set{f_1}}\): the premise that discharged in the surface is re-derived by on the consumable roots that the translated unpacks bind (12.9).

With type-preserving translation, type soundness, memory safety, immutability, and data-race freedom of CoreCapybara transfer to well-typed Capybara programs.

6 Case Studies↩︎

6.1 Implementation↩︎

We implemented Capybara in Scala 3 by extending its capture checker with a separation checker. It runs after capture-set computation and enforces separation and freshness.

The surface API uses three Scala markers: classes with tracked mutable state extend Mutable, mutating methods are marked update, and consuming methods consume:

With explicit receivers, the markers correspond to the modes of 3. inc takes its receiver at the default read-write permission, \(\textsf{inc} : \forall(\textsf{this} : \textsf{Counter}\capt\set{\ANY})\;\TUNIT\). get takes it read-only at \(\RO\,\textsf{Counter}\capt\set{\RO\,\ANY}\) and is callable through read-only views. finalize takes it at consume mode, \(\textsf{finalize} : \forall(\CONSUME\,\textsf{this} : \textsf{Counter}\capt\set{\ANY})\;\textsf{Int}\): a call consumes the receiver and kills its aliases.

The read-only qualifier ro of 2.3 does not appear in Scala syntax. Instead, the checker infers permissions from capture sets, which we call mode inference. A type whose capture set is in read-only mode is itself read-only: Counter^{any.rd} is understood as \(\RO\,\textsf{Counter}\capt\set{\RO\,\ANY}\). A read-only capture set of a Mutable type cannot be widened to a read-write one, as this would turn a read-only view into a read-write reference.

Separation and consume checking follow the root-based scheme of 3.3. The checker resolves every capture set to its peaks, the compiler’s term for roots (2.2). Two read-only peaks may overlap; an overlap in which one side writes is an error. For consume, the checker maintains a set of killed peaks: a consume call adds the peaks of its argument, and any later expression using one is rejected.

6.2 Mutable Builder of Immutable Data Structures↩︎

Immutable data structures such as strings or lists are ubiquitous in functional programming and immune to data races. Within separation-checked Scala, immutable lists are pure: no separation constraint applies, and they can be freely shared.

Efficient construction often uses a mutable builder, which must neither be shared nor reused after returning an immutable result. In Scala 3:

The update marker on append requires an exclusive, read-write reference, preventing mutable aliases across the call. complete consumes the builder and disables later access.

We can go one step further: for data structures such as arrays and byte buffers, we can obtain an immutable version simply by “freezing” the object, irrevocably dropping its mutation capability, similar to the freeze operation of Pony [23] and Project Verona [24]:

A Buffer is a mutable data structure; freezing returns it as a pure one. The result type Buffer^{} carries the empty capture set, so the frozen buffer is untracked and, like any immutable value, may be shared freely. This is safe for two reasons: the parameter is marked consume, so no other reference can reach the buffer after the call; and mode inference makes the result read-only, since the empty capture set is in read-only mode. Nothing can write to the frozen buffer through the old references or the new one, so it is effectively immutable.

6.3 Fearless Concurrency↩︎

6.3.1 Structured Parallelism↩︎

The library combinator runParallel of 2.2 provides data-race-free structured parallelism: it runs its two argument functions on separate threads, requires their capture sets to be separate, and suspends the caller until both return, so the concurrent computations join before it does.

As an example, a parallel quicksort uses a primitive that splits a Mutable array into two halves:

splitAt passes the two halves of the receiver to f as two array views. Their types carry distinct anys, so f may treat the halves as separate.

A parallel quicksort runs its two recursive calls concurrently:

The closures capture left and right read-write. They share ord, whose capture set {any.rd} contains only read-only capabilities, so it can safely run in parallel with itself.

6.3.2 Fork-Join Parallelism↩︎

Fork-join concurrency spawns a computation that outlives the expression starting it: the new thread runs until it is joined, possibly never. Conceptually, spawning f runs runParallel(f, rest) against the rest of the program; since rest is unbounded, nothing the spawned closure captures may ever be used again, so the parameter is marked consume:

A common use case is concurrent request handling in a server:

Each request is handled on a thread of its own. The onRequest callback takes ownership of its request (consume req), and spawn consumes the handler closure together with the request it captures.

7 Discussion↩︎

Semantic soundness for CoreCapybara establishes type safety, memory safety, immutability, and separation; confluence establishes data-race freedom. The type-preserving translation maps well-typed Capybara programs into the core. We do not define a separate semantics for the surface calculus or prove semantic preservation. The calculi omit Scala features such as classes, variance, exceptions, and concrete array layouts. The Scala 3 implementation handles them through its integration with the existing capture checker (6.1). We do not relate the compiler implementation formally to the declarative calculi, nor prove checker completeness or rule decidability. For concurrency, the calculi model structured parallelism, in which both branches join before evaluation continues. In Scala, APIs such as spawn consume a closure whose thread may outlive the call. The checker enforces consumption, but the thread’s behavior and synchronization primitives are outside the formal model.

A capability may be consumed only through a fresh, dominating reference, as in external uniqueness [25]. A component of a shared structure therefore cannot be consumed directly. APIs for such structures must expose operations such as builders, freezing, or disjoint splitting (6). Most permissions are inferred; Mutable classes, receiver modes, consume parameters, and fresh results mark the contracts that restrict aliasing. We have not measured the annotation cost of adding these contracts to existing capture-checked code. Synchronized sharing still requires specialized or trusted APIs.

Our main properties concern executions: separated terms have non-interfering footprints, read-only runs preserve every initial cell, and well-typed programs cannot use or free a dead cell. A syntactic proof would need corresponding heap and liveness invariants at every reduction step. Consumption makes these invariants nontrivial: types its continuation in the rewritten context \(\G\ominus C_1\), so contexts do not evolve monotonically, and deallocated cells remain in the heap, so attempts to access or deallocate them again are stuck. The logical relation instead includes footprints, liveness, and killing in the interpretation of types; the fundamental theorem establishes these invariants rule by rule. Semantic typing is also more expressive than the syntactic rules. Suppose a primitive ne that tests two references for identity. The following program is not syntactically well-typed, since nothing in scope separates a from b:

It can nevertheless be proved semantically well-typed: when the test succeeds, a and b are distinct cells, their footprints do not interfere, and the parallel composition runs without getting stuck (4).

The calculus supports higher-order store: references may contain closures and other references. Given \(x: T\), the program \(\LET a = \ALLOC x \IN \LET b = \ALLOC a \IN \ldots\) binds \(b : \REF[\REF[T]\capt\set{a}]\capt\set{c_b}\) where \(c_b\) is a fresh root: the content type names the stored reference \(a\) in its capture set, and reading \(b\) returns \(a\) at that type. It does not express cyclic reference graphs. At allocation, a reference’s content type and capture set may mention only capabilities already in scope, so it may contain only references allocated earlier. Supporting cycles remains future work.

The calculi support limited path dependence: capture sets may mention term variables, and dependent function codomains may name their parameters (3), but path selection is absent. The Scala 3 checker treats capabilities as paths and resolves them by prefix coverage: a covers a.b, while siblings a.b and a.c are treated as separate. Extending CoreCapybara with path selection based on Dependent Object Types (DOT) [26], [27] is future work.

Scala APIs mix curried and uncurried functions. Separation should be invariant under currying: constraints between parameter lists must survive partial application. Capture checking already supplies unary capture information. We considered and rejected reachability types as a basis for separation and freshness in Scala [28]. That calculus reconstructs separation at each application, but formalizes only unary application, not uncurried functions or Scala’s multiple parameter lists. A later logical-relations model revises the abstraction rule [29], suggesting that this subtle design point remains unsettled. Neither account treats Scala’s curried and uncurried calls uniformly. Capybara instead models separation constraints, for curried and uncurried functions alike, as relational modalities [20]. The encoding is stable and sound: constraints survive partial application by construction, and the logical model interprets the modality directly (5). The surface stays modality-free: the translation computes every lock and unlock. Both the calculus and the Scala checker handle the full application spine, so f(a, b) and f(a)(b) enforce the same separation.

8 Related Work↩︎

Capybara builds on capture checking and capturing types, which record the capabilities that a value may use [4], [5]. Capture checking is implemented in Scala 3 [30] and was first proposed as a foundation for exception safety [31]. Its boxing discipline draws on contextual modal type theory [20], and spores anticipated restrictions on closure capture in Scala [32]. Degrees of separation added relative, per-binding constraints to capture checking, obtaining confluence for fork-join parallelism [33], [34]. Capybara defines separation through roots: distinct roots are separate by construction, and capture sets are separate when they resolve to non-interfering roots, without per-binding declarations. It also adds freshness, consume, read-only access, and a semantic account of CoreCapybara.

Rust is the standard example of ownership and borrowing in a practical language, supporting memory safety and fearless concurrency through a pervasive alias discipline [1], [2], [35]–[37]. Swift and Mojo also support ownership and borrowing [11]–[13]. Classic ownership and uniqueness systems enforce a distinguished owner, confinement, unique access, or external uniqueness [8], [25], [38]–[42]; Mezzo makes permissions the basis of the language [43]. Adoption and focus recover temporary exclusive access to an aliased value by setting its adopter aside [44]. Tempered domination later applies this mechanism to fearless concurrency [45]. Previous Scala work used capabilities for unique references and actor isolation [46], [47]. Capybara permits ordinary sharing and uses tracked capture sets to establish the exclusivity required for separation or consumption, without a lexical focus construct.

Linear and affine types constrain use of values [7], [48], graded modal types generalize these restrictions [49], and recent work connects linearity, uniqueness, and borrowing [9], [50]. Linear Haskell supports ordinary and linear functions side by side [10]. Capybara retrofits substructural reasoning by constraining access through tracked capabilities rather than value use. CoreCapybara’s modality \([\Psi,\Phi]E\) records separation constraints between program-specific capture sets and read-only capability bounds. OxCaml modes instead qualify individual values along fixed axes such as locality, uniqueness, and contention [14], [15]; modal effect types index computations by effect contexts [16], [51]. These indices qualify one value or computation at a time; they do not directly relate the footprints of two otherwise freely aliased values. Like modal effect types, CoreCapybara uses Fitch-style locks; its unlocks discharge program-specific constraints rather than compare modes in a fixed lattice, as OxCaml submoding does. The translation inserts lock and unlock forms; Capybara has no modal syntax. Whether these constraint-indexed modalities admit a standard multimodal account remains open.

Capability systems go back to unforgeable tokens for controlling authority [52]; object-capability languages make authority follow from holding object references [53]. Capabilities also induce an effect discipline: the effects of a computation are bounded by the capabilities it holds [6], [54]. Wyvern makes this idea explicit with object capabilities and path-dependent effects [55], [56]. Second-class values restrict capability scope, while effect handlers reflect capabilities in computation types [57]–[61]. Type-and-effect systems and row-polymorphic effect languages track effects directly [62]–[64]. Capybara builds on this capability-based account of effects, adding static control of exclusive and read-only access.

Separation logic and syntactic systems for interference control use disjointness and permissions to reason about memory access [19], [65]–[70]. In Capybara, separated capture sets denote non-interfering footprints and justify parallel composition. Reference immutability restricts mutation through read-only references [71]–[77]; Capybara applies the same restriction to capabilities; its separation judgment permits overlapping read-only footprints. Region systems and Cyclone provide static memory management through regions and region capabilities [78]–[80]. Typed memory-management calculi add static capabilities, alias types, and linear regions [81]–[83]. Capybara proves no-use-after-free and no double-free using liveness in the semantic model, without region handles or region inference.

Reference-capability systems such as Pony and Verona assign permissions that control aliasing and concurrency [23], [24], [84]. Other systems obtain fearless concurrency through uniqueness with immutability, branded permissions, affine regions with isolated fields, or capability-based actors [45], [74], [85], [86]. In Capybara, data-race freedom follows from separation and confluence: parallel computations have non-interfering footprints, and their scheduling is unobservable. Separation is checked per captured capability, rather than per object graph, actor heap, thread reservation, or region.

Logical relations and the logical approach to type soundness support semantic accounts of higher-order state, memory safety, and concurrency [17], [21], [22], [29], [36], [87], [88]. Our logical relation interprets types as predicates over worlds and capture sets as access-tagged footprints. Its fundamental theorem yields type safety, memory safety, and immutability; the same model validates separation. The core development is mechanized in Lean 4. Future work is to interpret Capybara types in a separation logic, possibly through implicit dynamic frames [89], and relate that interpretation to Iris [90].

9 Conclusion↩︎

We presented System Capybara, extending capturing types with selective substructural reasoning. Ordinary aliasing remains unrestricted; APIs require separation, read-only access, or consumption only where needed. Separation gives non-interfering footprints, while consumption prevents later use through aliases.

A type-preserving translation maps Capybara to CoreCapybara, whose semantic soundness proof we mechanize in Lean 4. It establishes type safety, memory safety, immutability, and data-race freedom. We implement Capybara as the new separation checker in the Scala 3 compiler, built on its existing capture checker. The implementation gives Scala itself Rust-style resource safety and fearless concurrency without global ownership invariants: pervasive sharing remains the default, and substructural constraints fit its generic and higher-order idioms.

10 Complete Definitions of System CoreCapybara↩︎

This appendix presents the full formal definitions of the core calculus CoreCapybara. The definitions follow the Lean mechanization; they depart from it only in notation and minor presentational simplifications, as stated in the conventions below.

10.1 Syntax↩︎

[fig:core-syntax] presents the abstract syntax of System CoreCapybara. CoreCapybara has memory primitives for allocating, reading, writing, and deallocating references, reader values \(\RO\,x\) that grant read-only access to a reference, modal values \(\LOCK[\Psi,\Phi]t\) with the eliminator \(\UNLOCK\,x\), parallel composition, and conditionals. An existential type \(\EXCAP{c_1,\ldots,c_n}T\) hides \(n\) capture variables; its introduction form is a pack \(\<C_1,\ldots,C_n,x\>\) that supplies the \(n\) witnesses, and its elimination forms are the unpack \(\LET\<c_1,\ldots,c_n,x\>=t\IN u\) and the consumer lambda \(\lambda(\<c,x\>:\EXCAP{c}T)t\), a first-class function that consumes a packed argument. Its application \(x\,t\) passes the term \(t\), which distinguishes it from an ordinary application \(x\,y\) of a variable to a variable. A capture bound \(B\) is a capture set or the trivial bound \(\top\). A capture binding \(\alpha\,c<:B\) carries a consume mode \(\alpha\): an access-only variable (\(\epsilon\)) may only be accessed, a consumable one (\(\CONSUME\)) may additionally be consumed, and a killed one (\(\KILLED\)) has been consumed and may be neither accessed nor consumed. The mode \(\KILLED\) does not occur in source programs; it arises in the contexts of typing derivations through the kill operation defined below.

10.2 Static Semantics↩︎

The static semantics consists of nine judgments: subcapturing \(\subs{\G}{C_1}{C_2}\), capability kinding \(\typs{\G}{C}{m}\), subbounding \(\subs{\G}{B_1}{B_2}\), separation \(\sep{\G}{C_1}{C_2}\), disjointness \(\disj{\G}{C_1}{C_2}\), sequential composition \(\seqcomp{\G}{C_1}{C_2}\), satisfaction \(\sat{\G}{[\Psi,\Phi]}\), subtyping \(\subs{\G}{E_1}{E_2}\), and term typing \(\typ{C}{\G}{t}{E}\).

Two conventions apply throughout. First, all rules are stated up to \(\alpha\)-renaming, and every type and capture set is well-scoped in the context where it occurs; the mechanization enforces this with de Bruijn indices. In particular, in rule the capture set \(C\) cannot mention the bound variable \(x\), and in rules and neither \(C_2\) nor \(E\) can mention the variables bound by the continuation. Second, in the mechanization, abstractions, modal values, and parallel compositions carry the capture sets appearing in their typing rules as annotations; we omit these annotations, except the two capture sets on a parallel composition, which the reduction rules consult and which we display in 10. As in the surface language, we omit the default permission \(\epsilon\) of a capturing type \(m\,S\capt C\) and write \(S\capt C\). We identify a pure capturing type \(S\capt\set{}\) with the shape type \(S\).

10.2.1 Capture Set Operations and Predicates↩︎

Applying an access mode to a capture set acts on every element: \(\epsilon\,C = C\); \(\RO\,C\) replaces the mutability of every element of \(C\) by \(\RO\), leaving \(\CONSUME\)-marked elements unchanged; and \(\CONSUME\,C\) marks every element of \(C\) with \(\CONSUME\). Mutabilities are ordered by \(\RO\preceq\epsilon\).

The roots of a capture set resolve term variables through the context until only capture variables remain: \[\begin{align} \roots{\G}{\set{}} &= \set{} \\ \roots{\G}{C_1\cup C_2} &= \roots{\G}{C_1}\cup\roots{\G}{C_2} \\ \roots{\G}{\set{\mu\,c}} &= \set{\mu\,c} \\ \roots{\G}{\set{\mu\,x}} &= \mu\,\roots{\G}{C} \quad\text{where}\;x: m\,S\capt C\in\G \end{align}\] A capture set containing only capture variables is a root set, ranged over by \(P\). We write \(P\vert_{\CONSUME}\) for the restriction of \(P\) to its \(\CONSUME\)-marked elements. The mechanization names this function peaks.

The judgments on capture sets used by the rules are defined via roots:

• \(\accessonly{\G}{C}\) holds iff \(\roots{\G}{C}\) contains no \(\CONSUME\)-marked element. A bound is access-only if it is \(\top\) or an access-only capture set.

• \(\consumable{\G}{C}\) holds iff every capture variable occurring in \(\roots{\G}{C}\) is bound with mode \(\CONSUME\) in \(\G\).

• \(\accessible{\G}{C}\) holds iff no capture variable occurring in \(\roots{\G}{C}\) is bound with mode \(\KILLED\) in \(\G\).

The context \(\G\ominus C\) kills the capture variables consumed by \(C\): \[\G\ominus C \mathrel{\vcenter{:}}= \G\big[\;\alpha\,c<:B \;\mapsto\; \KILLED\,c<:B \;\big|\; \CONSUME\,c\in\roots{\G}{C}\;\big],\] replacing the binding of every capture variable that the roots of \(C\) mark consumed and leaving all other bindings unchanged.

10.2.2 Subcapturing, Capability Kinding, and Subbounding↩︎

None

Figure 6 defines subcapturing, capability kinding, and subbounding. Subcapturing extends the surface rules with , which resolves a capture variable to its declared bound and applies only to access-only bindings, , which forgets a read-only restriction upward, and the congruence rules and . Capability kinding assigns a mutability to a capture set: every set has kind \(\epsilon\) by , while kind \(\RO\) certifies that the set grants at most read-only access, either because the set is \(\RO\)-marked or because an enclosing lock asserts it . Subbounding lifts subcapturing to capture bounds, with \(\top\) above every bound.

10.2.3 Separation, Sequential Composition, and Satisfaction↩︎

None

Figure 7 defines the three judgments that govern aliasing and consumption. Separation \(\sep{\G}{C_1}{C_2}\) certifies that two capture sets do not interfere: two access-only sets of read-only kind are separated ; two distinct consumable capture variables are separated ; a lock in the context contributes the separation assumptions it records ; and separation is preserved when the left-hand set shrinks to a subcapture . Disjointness \(\disj{\G}{C_1}{C_2}\) is the fragment of separation obtained by dropping and . In particular, it admits no read-only sharing: two read-only views of the same capability are separate but not disjoint. Disjoint sets thus hold genuinely distinct capabilities, and uses the judgment to keep the witnesses of an existential pairwise apart. Sequential composition \(\seqcomp{\G}{C_1}{C_2}\) states that a computation using \(C_1\) may run before one using \(C_2\): either \(C_1\) consumes nothing or it is separated from \(C_2\) . Satisfaction \(\sat{\G}{[\Psi,\Phi]}\) discharges a modal context: each mode entry of \(\Phi\) is established by kinding and each pair of distinct entries of \(\Psi\) by separation.

10.2.4 Subtyping↩︎

None

Figure 8 defines subtyping. The judgment relates existential types, with capturing types included as the existential types that bind no capture variable. Rule combines shape subtyping with subcapturing; the remaining congruence rules relate shape types. The mechanization instead inlines the subcapturing premise of into each congruence rule. Only pure types are below \(\top\) . Rule replaces the modal context of a modal type by another one that suffices to satisfy it: the original context \([\Psi_1,\Phi_1]\) must be satisfied under a lock carrying the new context \([\Psi_2,\Phi_2]\). Rule relates two existentials of the same arity under their \(n\) freshly bound, access-only capture variables. Consumer types carry no congruence rule; they are related only by and . Reference and reader types are invariant in their content type.

10.2.5 Term Typing↩︎

None

Figure 9 presents the typing rules. The judgment \(\typ{C}{\G}{t}{E}\) carries a use set \(C\) bounding the capabilities that \(t\) accesses or consumes. A variable occurrence has an empty use set, and its type refines the declared capture set to \(\set{x}\) ; uses are charged at elimination forms, each of which requires the eliminated capability to be accessible. Type and capture application charge the empty use set: a type or capture lambda binds a value ([fig:core-syntax]), so applying it produces that value without running anything, and the value’s work is charged where it is later eliminated; the accessibility and access-only premises remain. The restriction to value bodies costs no expressiveness, since a computation is suspended by boxing it under a lock with an empty separation context, whose satisfaction is vacuous. Unlock, by contrast, charges its subject : opening a modal value releases the suspended computation inside, and the subject’s capture set, which carries the modal’s annotation, is what pays for it. Rule sequences the two use sets through \(\seqcomp{\G}{C_1}{C_2}\) and types the continuation in \(\G\ominus C_1\), so capture variables consumed by the bound term are killed and no longer accessible. Rule eliminates an \(n\)-ary existential. It additionally requires the consumed roots of \(C_1\) to be consumable, and binds \(n\) fresh consumable capture variables \(c_1,\ldots,c_n\) that the continuation may access and consume, as recorded by the extra use set \(\set{c_1,\ldots,c_n,\CONSUME\,c_1,\ldots,\CONSUME\,c_n}\). Between the witnesses and \(x\) it pushes the manufactured ownership lock \(\LOCK[\Psi_w,\Phi_w]\), recording that the witnesses are separate from the continuation charge \(C_2\); the sequencing premise pays for it in the footprint model, where every witness location is either confined to what \(C_1\) consumes, which \(\seqcomp{\G}{C_1}{C_2}\) keeps out of \(C_2\), or freshly allocated by the bound term (see 2). Dually, consumes the packed capture sets: writing \(D=\bigcup_i C_i\), each \(C_i\) must be access-only and consumable, the witnesses must be pairwise disjoint, and the pack charges \(D\cup\CONSUME\,D\). The consumer lambda is a first-class function that unpacks its argument: its body binds the consumable witness \(c\) and the term variable \(x\), and it kills every consumable capability of \(\G\) that its closure \(C\) does not capture, chosen as the root set \(X\). Its application sequences the argument’s use before the consumer’s own, mirroring . Allocation returns a reference under a fresh capture variable ; deallocation requires \(\set{x}\) to be consumable and charges \(\set{\CONSUME\,x}\) . Writing goes through the reference itself , whereas reading goes through a reader value , . Parallel composition requires the use sets of the two branches to be separated .

10.3 Dynamic Semantics↩︎

The dynamic semantics is store-based. Evaluation runs a term against a heap. At runtime, term variables additionally range over heap locations \(l\): evaluation substitutes locations for bound variables. A configuration \(\cfg{H}{t}\) pairs a heap \(H\) with the term \(t\) under evaluation. A heap is a finite map from locations to cells, \[H(l) \;::=\; v \;\mid\; \refcell{l'} \;\mid\; \deadcell{l'},\] a stored value \(v\), a live reference cell \(\refcell{l'}\) holding the location \(l'\), or a dead cell \(\deadcell{l'}\) left by a deallocation. We write \(H(l)\) for lookup, \(\dom H\) for the set of allocated locations, and \(H[l\mapsto c]\) for the heap that extends or updates \(H\) at \(l\). Each stored value also carries its footprint, the set of runtime capabilities it holds, which is the runtime image of its capture set; the parallel rules consult it and we leave it implicit.

Both relations emit a trace \(\tau\), a finite sequence of heap events recording every access the run performs. An event is an access \(\mu\,l\), a read when \(\mu=\RO\) and a write when \(\mu=\epsilon\), an allocation \(\ALLOC l\), or a deallocation \(\DEALLOC l\). Traces are the objects over which the standardization and confluence theorems are stated (11.8). We write \(\tau_1\,\tau_2\) for concatenation and omit the label on a step that emits the empty trace.

10.3.1 Small-step Reduction↩︎

None

Figure 10 defines the small-step relation \(\cfg{H}{t} \stepsto{\tau} \cfg{H'}{t'}\). An elimination form looks up its subject in the heap and reduces against the stored value. , , and apply a stored abstraction by substitution; type and capture arguments are computationally irrelevant, so these steps leave the heap and the trace untouched. applies a consumer by unpacking its argument, reducing to a redex, and opens a boxed value. The memory primitives are the only steps that touch the heap or the trace: follows a reader to its cell and returns the stored location, emitting a read; overwrites a live cell, emitting a write; installs a fresh live cell and returns a pack of its location; and marks a cell dead. A let evaluates its bound term under , then either lifts the resulting value to a fresh location or, when it is already a location, substitutes it ; substitutes the \(n\) witnesses and the location of a pack. and interleave the two branches of a parallel composition and returns unit once both are answers. A parallel node carries the footprints \(C_1\) and \(C_2\) of its two branches, the capture-set annotations of the typing rule resolved to the runtime capabilities they hold. A footprint is a finite set of elements \(\mu\,l\) tagging a location \(l\) with an access mode \(\mu\), and we order access modes by extending \(\RO\preceq\epsilon\) with \(\CONSUME\preceq\CONSUME\), leaving \(\CONSUME\) incomparable to the mutabilities. A left step is allowed on two conditions. First, the emitted trace is authorized by the stepping branch’s footprint. Say a location \(l\) is fresh at an event of \(\tau\) when an earlier \(\ALLOC l\) event precedes it in \(\tau\). Then \(\tauth{\tau}{C_1}\) holds when, for every event of \(\tau\) whose location is not fresh at it, an access \(\mu\,l\) has some \(\mu'\,l\in C_1\) with \(\mu\preceq\mu'\), and a deallocation of \(l\) has \(\CONSUME\,l\in C_1\). Second, the two footprints are non-interfering: \(\nintf{C_1}{C_2}\) holds when every \(\mu_1\,l_1\in C_1\) and \(\mu_2\,l_2\in C_2\) satisfy \(l_1\neq l_2\) or \(\mu_1=\mu_2=\RO\). The stepping branch’s footprint then grows to \(C_1'=C_1\cup\set{\epsilon\,l,\CONSUME\,l\mid \ALLOC l\;\text{occurs in}\;\tau}\), adding the cells \(t\) allocates so a later step may use them. is symmetric. These are exactly the obligations that the typing rule establishes on \(C_1\) and \(C_2\), so a well-typed program never blocks on them.

10.3.2 Big-step Evaluation↩︎

None

Figure 11 defines the big-step relation \(\cfg{H}{t} \evalsto{\tau} \cfg{H'}{a}\), evaluating \(t\) to an answer \(a\), a value or a location, while threading the heap and concatenating the traces of its subevaluations. It is the sequential counterpart of the small-step relation: values and locations evaluate to themselves , , the elimination forms evaluate the redex they expose, and runs the two branches left to right rather than interleaving them. and sequence a let by evaluating the bound term first and then the body, lifting an intermediate value to the heap or substituting an intermediate location, and does the same for an existential. The two relations agree up to the scheduling of parallel composition; the metatheory relates them by a standardization argument (12).

11 Metatheory of System CoreCapybara↩︎

This appendix presents the semantic model behind 5 and states the theorems in the form in which they are mechanized. The Lean development is the ground truth. The definitions below transcribe it in the notation of 10, omitting de Bruijn indices and well-scopedness side conditions. The model is a step-indexed Kripke logical relation over a higher-order store [17], [87]: types denote world-indexed predicates on heaps and terms, capture sets denote footprints, and the typing judgment asserts that the term evaluates to an answer satisfying its type’s predicate, with a trace authorized by its use set.

11.1 Footprints↩︎

A footprint is a capture set whose elements mention only heap locations (4). Each stored value in the heap carries its footprint, the runtime image of its capture-set annotation, and a location inherits the footprint of what it names: \[\fploc{H}{l} = \begin{cases} \set{\epsilon\,l} & \text{if}\;H(l)\;\text{is a reference cell,}\\ R_v & \text{if}\;H(l) = v\;\text{with footprint}\;R_v. \end{cases}\] A semantic environment \(\rho\) maps term variables to locations and capture variables to footprints; applying it to a capture set \(C\) yields a ground set, whose footprint \(\fdenot{C}_\rho^H\) expands each element to the footprint of its location: \[\fdenot{\set{}}_\rho^H = \set{}, \qquad \fdenot{C_1\cup C_2}_\rho^H = \fdenot{C_1}_\rho^H\cup\fdenot{C_2}_\rho^H, \qquad \fdenot{\set{\mu\,l}}_\rho^H = \mu\,\fploc{H}{l},\] with mode application as in 10. We drop the subscripts when the environment and heap are clear. A footprint \(C\) covers an access \(\mu\,l\) when \(\mu'\,l\in C\) for some \(\mu\preceq\mu'\). This is the reading used by trace authorization \(\tauth{\tau}{C}\) (4). Non-interference \(\nintf{C_1}{C_2}\) is as in 4, and two footprints are disjoint when they share no location at all.

11.2 Worlds↩︎

The denotations of the next subsection are Kripke: a type is interpreted relative to a world \((\Sigma, H)\), the heap \(H\) a program has reached together with a store typing \(\Sigma\) that assigns semantic contents to its reference cells. As a program allocates and writes, the world grows, and denotations are stable under this growth, so a value keeps its type in every future world.

The store typing is what breaks the circularity of the higher-order store: a cell typed \(\REF[T]\) should hold contents of type \(T\), but \(T\) may itself mention reference types, and through type variables a cell may even store values of an abstract type. \(\Sigma\) therefore assigns each cell a relation rather than a syntactic type, and the relations are stratified by a step index \(k\): \[\mathit{World}_k = \mathit{Loc}\rightharpoonup \mathit{Rel}_k, \qquad \mathit{Rel}_k = \textstyle\prod_{j<k} \left(\mathit{World}_j\to\mathit{Heap}\to\mathit{Term}\to\mathrm{Prop}\right).\] A stored relation at index \(k\) is a family, over every lower index \(j<k\), of predicates on a world at index \(j\), a heap, and a term. The space of relations recurses on the index, so the store is inherently step-indexed. This shape is forced: a stored relation must be stable under world extension, and must agree with the content type in both directions so that writes can re-establish it. We write \(\lfloor\Sigma\rfloor_j\) for the truncation of \(\Sigma\) to a lower index \(j\), which restricts each stored family to indices below \(j\).

World extension \(\wext{\Sigma'}{H'}{\Sigma}{H}\) holds when \(H'\) evolves from \(H\), meaning every allocated location keeps its cell, where a stored value is unchanged and a reference cell may change its content and may die but not revive, and when \(\Sigma'\) agrees with \(\Sigma\) on \(\dom\Sigma\). A world is well-typed, written \(\memtyped{k}{\Sigma}{H}\), when

1. every \(l\in\dom\Sigma\) is a reference cell of \(H\);

2. every stored relation of \(\Sigma\) is stable under world extension, at every index below \(k\); and

3. for every live cell \(l\in\dom\Sigma\) with \(H(l)=\refcell{l'}\), the content satisfies its stored relation at every lower index: \(\Sigma(l)_j\,(\lfloor\Sigma\rfloor_j, H, l')\) for all \(j<k\).

Condition (3) exposes cell contents only at indices strictly below \(k\), so a read consumes one unit of the index. The model accordingly treats \(k\) as a read budget: it bounds the number of read events of the runs about which the model makes claims.

11.3 Interpretation of Types↩︎

Types are interpreted relative to a semantic environment \(\rho\), which assigns to each variable of the context a semantic object of the matching kind: a heap location to a term variable, a footprint to a capture variable (11.1), and a denotation, a world-indexed predicate on answers, to a type variable. It is defined in 11.5. The value denotation \(\vdenot{T}_\rho\) is then a world-indexed predicate on answers, defined by recursion on the type, mutually with the expression denotation of the next subsection. We write \(a\in\vdenot{T}_\rho(k,\Sigma,H)\) when it holds of \(a\) at the world. Because evaluation lifts values to the heap, an answer names a value either directly or through a location. The partial function \(\resolve\) recovers it: \[\resolve(H,v) = v, \qquad \resolve(H,l) = v\;\;\text{if}\;H(l)=v,\] and \(\resolve(H,l)\) is undefined when \(l\) is unallocated or holds a reference cell. For a stored relation \(R\) at index \(k\), write \(R\approx_k\vdenot{T}_\rho\) when \(R\) agrees with the denotation of \(T\) at every lower world: \(R_j\,(\Sigma',H',a') \iff a'\in\vdenot{T}_\rho(j,\Sigma',H')\) for all \(j<k\), \(\Sigma'\), \(H'\), \(a'\). The first-order clauses are: \[\begin{array}{lcl} \vdenot{\TUNIT}_\rho(k,\Sigma,H) &=& \set{a\mid \resolve(H,a) = ()}\\[2pt] \vdenot{\TBOOL}_\rho(k,\Sigma,H) &=& \set{a\mid \resolve(H,a)\in\set{\TTRUE,\TFALSE}}\\[2pt] \vdenot{\top}_\rho(k,\Sigma,H) &=& \set{a\mid \resolve(H,a)\;\text{is a value with empty footprint}}\\[2pt] \vdenot{X}_\rho(k,\Sigma,H) &=& \rho(X)\,(k,\Sigma,H)\\[2pt] \vdenot{\REF[T]\capt C}_\rho(k,\Sigma,H) &=& \set{l\mid H(l)\;\text{a cell},\;\fdenot{C}\;\text{covers}\;\epsilon\,l,\; \Sigma(l)\approx_k\vdenot{T}_\rho}\\[2pt] \vdenot{\RO\,\REF[T]\capt C}_\rho(k,\Sigma,H) &=& \set{a\mid \resolve(H,a)=\RO\,l,\;\fdenot{C}\;\text{covers}\;\RO\,l,\; \Sigma(l)\approx_k\vdenot{T}_\rho} \end{array}\] Only pure values are below \(\top\). In the two cell clauses, the forward direction of the agreement \(\approx_k\) types the result of a read, and the backward direction lets a write re-establish condition (3) of \(\memtyped{k}{\Sigma}{H}\).

A function type denotes the abstractions whose bodies meet their specification in every future world. The four abstraction clauses share this quantification, so we abbreviate it: for \(j\leq k\), let \(\fworlds{j}{R}\) be the set of well-typed future worlds at index \(j\) in which \(R\) is live, that is, the pairs \((\Sigma',H')\) with \(\wext{\Sigma'}{H'}{\lfloor\Sigma\rfloor_j}{H}\), \(\memtyped{j}{\Sigma'}{H'}\), and every cell of \(R\) live in \(H'\). In each clause, the closure footprint \(R_0\) is the footprint of the stored abstraction’s capture annotation, and the footprints of the quantified ground capture sets are taken in \(H'\). The function clause is: \[\begin{array}{l} \vdenot{(\forall(x:T_1)E)\capt C}_\rho(k,\Sigma,H) =\\ \quad\{\,a\mid \resolve(H,a)=\lambda(x:T_1')\,t\;\text{with}\; R_0\subseteq\fdenot{C},\;\text{and}\\ \qquad [x:=l]\,t\in\edenot{E}^{R_0}_{\rho[x\mapsto l]}(j,\Sigma',H')\\ \qquad\quad \text{for all}\;j\leq k,\; (\Sigma',H')\in\fworlds{j}{R_0},\; \text{and}\;l\in\vdenot{T_1}_\rho(j,\Sigma',H')\,\} \end{array}\] The body’s budget is \(R_0\), not the annotation \(C\): a function may touch exactly what it captures. A type abstraction takes a denotation as its argument: \[\begin{array}{l} \vdenot{(\forall[X<:S]E)\capt C}_\rho(k,\Sigma,H) =\\ \quad\{\,a\mid \resolve(H,a)=\lambda[X<:S']\,t\;\text{with}\; R_0\subseteq\fdenot{C},\;\text{and}\\ \qquad [X:=\top]\,t\in\edenot{E}^{R_0}_{\rho[X\mapsto\delta]}(j,\Sigma',H')\\ \qquad\quad \text{for all}\;j\leq k,\; (\Sigma',H')\in\fworlds{j}{R_0},\; \text{and all proper}\;\delta\; \text{bounded by}\;\vdenot{S}_\rho\,\} \end{array}\] A denotation \(\delta\) is proper when it satisfies the closure properties the model demands of every type’s interpretation, chiefly stability under heap growth, world extension, and index decrease. As an argument here it must moreover contain only pure answers. Bounded means that \(\delta\) implies \(\vdenot{S}_\rho\) at every world extending \((\Sigma',H')\), at every index at most \(j\). The type substituted into the body is irrelevant to evaluation. The mechanization fixes \(\top\). A capture abstraction takes a ground capture set: \[\begin{array}{l} \vdenot{(\forall[c<:B]E)\capt C}_\rho(k,\Sigma,H) =\\ \quad\{\,a\mid \resolve(H,a)=\lambda[c<:B']\,t\;\text{with}\; R_0\subseteq\fdenot{C},\;\text{and}\\ \qquad [c:=W]\,t\in\edenot{E}^{R_0}_{\rho[c\mapsto W]}(j,\Sigma',H')\\ \qquad\quad \text{for all}\;j\leq k,\; (\Sigma',H')\in\fworlds{j}{R_0},\\ \qquad\quad \text{and all ground}\;W\;\text{with}\;\fdenot{W}\; \CONSUME\text{-free and}\;\fdenot{W}\subseteq\fdenot{B}\,\} \end{array}\] The bound imposes no constraint when \(B=\top\). A consumer takes a packed argument, a ground witness \(W\) together with a location: \[\begin{array}{l} \vdenot{(\forall(\<c,x\>:\EXCAP{c}T_1)E)\capt C}_\rho(k,\Sigma,H) =\\ \quad\{\,a\mid \resolve(H,a)=\lambda(\<c,x\>:\EXCAP{c}T_1')\,t\; \text{with}\;R_0\subseteq\fdenot{C},\;\text{and}\\ \qquad [c:=W,\,x:=l]\,t\in \edenot{E}^{\,R_0\cup\fdenot{W}\cup\CONSUME\,\fdenot{W}}_{\rho}(j,\Sigma',H')\\ \qquad\quad \text{for all}\;j\leq k,\; (\Sigma',H')\in\fworlds{j}{R_0},\; \text{all ground}\;W\;\text{with}\;\fdenot{W}\; \CONSUME\text{-free,}\\ \qquad\quad \text{live in}\;H'\text{, and disjoint from}\;R_0,\; \text{and all}\;l\in\vdenot{T_1}_{\rho[c\mapsto W]}(j,\Sigma',H')\,\} \end{array}\] The witness binding \(\rho[c\mapsto W]\) carries consumable authority, and the body’s budget widens to \(R_0\cup\fdenot{W}\cup\CONSUME\,\fdenot{W}\): the consumer receives full rights to the witness, including its consumption. The result type \(E\) mentions neither \(c\) nor \(x\), so it is interpreted under \(\rho\) itself. A modal type \(([\Psi,\Phi]E)\capt C\) denotes the boxed values whose recorded separation context is discharged by the semantic satisfaction of \([\Psi,\Phi]\) and whose bodies inhabit \(\edenot{E}\) in every future world in which \(\rho\) satisfies \([\Psi,\Phi]\), meaning each kind entry of \(\Phi\) holds of the corresponding footprint and each separation pair of \(\Psi\) denotes non-interfering footprints. Finally, an existential type denotes the packs whose witnesses are separate: \[\begin{array}{l} \vdenot{\EXCAP{c_1,\ldots,c_n}T}_\rho(k,\Sigma,H) =\\ \quad\{\,a\mid \resolve(H,a)=\<C_1,\ldots,C_n,x\>,\\ \qquad \fdenot{C_1},\ldots,\fdenot{C_n}\;\text{are}\; \CONSUME\text{-free and pairwise disjoint},\\ \qquad x\in\vdenot{T}_{\rho[c_1\mapsto C_1,\ldots,c_n\mapsto C_n]}(k,\Sigma,H)\,\} \end{array}\] where the witnesses \(c_i\) are bound at consumable authority.

11.4 The Expression Relation↩︎

The expression denotation lifts a predicate on answers to a predicate on expressions: an expression inhabits it when it evaluates, by the big-step relation of 11, to an answer in the value denotation while accessing only the locations in its budget. The read budget guards every clause. Write \(\readsof{\tau}\) for the number of read events of a trace \(\tau\). Call a run of the small-step relation sequential when it follows the left-first schedule: fires only when the left branch is already an answer, so the right branch of a parallel node steps only after the left has finished. This is the order in which evaluates a parallel composition, so sequential runs are the small-step reading of the big-step relation. We write \(\cfg{H}{t}\redsto{\tau}\cfg{H'}{t'}\) for the reflexive-transitive closure of the small-step relation, concatenating traces, and \(\seqredsto{\tau}\) for its restriction to sequential runs. Then \(t\in\edenot{E}^{R}_\rho(k,\Sigma,H)\) iff \(\memtyped{k}{\Sigma}{H}\) implies all of:

1. Safety: every configuration reachable from \(\cfg{H}{t}\) by a sequential run performing fewer than \(k\) reads is an answer or can step.

2. Postcondition: for every evaluation \(\cfg{H}{t}\evalsto{\tau}\cfg{H'}{a}\) with \(\readsof{\tau}<k\), the trace is authorized by the budget, \(\tauth{\tau}{R}\), and, where \(k' = k-\readsof{\tau}\), there is a store typing \(\Sigma'\) at index \(k'\) with \[\wext{\Sigma'}{H'}{\lfloor\Sigma\rfloor_{k'}}{H}, \qquad \memtyped{k'}{\Sigma'}{H'}, \qquad a\in\vdenot{E}_\rho(k',\Sigma',H').\]

3. Prefix safety: for every sequential run \(\cfg{H}{t}\seqredsto{\tau}\cfg{H''}{t''}\) with \(\readsof{\tau}<k\), complete or not, the trace is authorized by the budget, \(\tauth{\tau}{R}\).

Runs that exhaust the budget owe nothing. Adequacy below recovers unconditional claims by instantiating \(k\) above the read count of any given run. When \(E\) is an existential, the postcondition additionally requires the witnesses of the answer to be live in \(H'\) and confined: every capability a witness reaches is either consumable under the budget \(R\) or was freshly allocated by the run. This witness-confinement bound is what pays for the ownership lock of (2).

The safety clause is a budget-indexed progress predicate. At a parallel node it is a rely-guarantee invariant: it carries the two branch footprints, requires every branch run to be authorized by its footprint and the two footprints to be non-interfering, and requires each branch to remain safe under every heap that runs of the other branch can produce.

The postcondition constrains complete runs only, so prefix safety is what bounds the trace of a run still underway. In the mechanization, the sequential relation carries none of the guards of and , and prefix safety moreover realizes each within-budget run in guarded form, with the authorization and non-interference guards discharged at every parallel step. This realization is what embeds a run of the model into the full small-step relation, where the guards are checked at every step (11.7).

11.5 Semantic Typing↩︎

An environment \(\rho\) realizes a context \(\G\) at a world, written \(\rho\in\gdenot{\G}(k,\Sigma,H)\), when it interprets each binding as its denotation demands:

• for \(x: T\), the location \(\rho(x)\) is in \(\vdenot{T}_\rho(k,\Sigma,H)\);

• for \(X<:S\), the denotation \(\rho(X)\) is a proper, extension-stable predicate bounded by \(\vdenot{S}_\rho\);

• for \(\alpha\,c<:B\), the footprint of \(\rho(c)\) is \(\CONSUME\)-free and bounded by \(\fdenot{B}\), and \(\rho\) records the authority \(\alpha\) for \(c\);

• for a lock \(\LOCK[\Psi,\Phi]\), \(\rho\) satisfies \([\Psi,\Phi]\) semantically, as in the modal clause above.

Consumption rights are carried by the binding authority, not by the footprint itself. The budget of a term that consumes \(c\) acquires the \(\CONSUME\) capabilities through the rules that charge them. An environment is separation-well-formed when the footprints of distinct consumable capture variables are disjoint.

Semantic typing quantifies over all realizing worlds: \(\semtyp{C}{\G}{t}{E}\) holds iff for all \(\rho\), \(k\), \(\Sigma\), \(H\) with \(\rho\in\gdenot{\G}(k,\Sigma,H)\), \(\rho\) separation-well-formed, and every cell of \(\fdenot{C}_\rho^H\) live in \(H\), \[t\rho \in \edenot{E}^{\fdenot{C}_\rho^H}_{\rho}(k,\Sigma,H),\] where \(t\rho\) substitutes the environment into the term.

11.6 The Fundamental Theorem↩︎

The proof is by induction on the typing derivation, with one compatibility lemma per rule of 9. The auxiliary judgments of 10 have fundamental lemmas of their own, which the compatibility lemmas invoke. The two that carry the concurrency results are:

2 is 4: syntactic separation denotes non-interference of footprints. It is what lets the compatibility lemma for establish the rely–guarantee obligations of the safety predicate and the side conditions of and . Kinding has an analogous lemma: a capture set of kind \(\RO\) denotes a footprint that covers no write.

11.7 Adequacy↩︎

Adequacy extracts unconditional statements about closed programs. A closed program is run on a platform of \(N\) pre-allocated boolean cells: the context \(\G_N\) binds, per cell, a capture variable and a term variable of type \(\REF[\TBOOL]\); the heap \(H_N\) allocates the \(N\) live cells; and the environment \(\rho_N\) maps each variable to its cell. The platform realizes \(\G_N\) at every index by construction, is separation-well-formed because all its capture variables are access-only, and is compatible with every footprint because all its cells are live. A program is a source term: it mentions no heap locations, so the platform configuration \(\cfg{H_N}{t\rho_N}\) is well-formed in the sense of 11.8, as the substitution \(\rho_N\) introduces only the live platform cells.

Given a reachable configuration, instantiate the semantic typing at budget \(k = \readsof{\tau}+1\) for the trace \(\tau\) of the run that reaches it. The run is then strictly within budget and the safety clause applies. The schedule theorems of 11.8 lift the statement to arbitrary interleavings.

Let \(\cfg{H_N}{t\rho_N}\redsto{\tau_1}\cfg{H_1}{t_1}\) and instantiate the semantic typing at budget \(k = \readsof{\tau_1}+1\). The safety clause yields a maximal sequential run: one that reaches an answer within the budget, or one that performs at least \(k\) reads. Prefix safety realizes it in guarded form (11.4), so it is also a run of the unrestricted relation. Confluence (13) joins the two runs. If the joining run out of \(\cfg{H_1}{t_1}\) is nonempty, \(t_1\) can step. If it is empty, the joined endpoints coincide. Then either \(t_1\) is the sequential answer up to a renaming of locations, hence itself an answer, or the sequential run exhausted the budget, which condition (4) of confluence excludes: the joined traces have equal read counts, yet one performs fewer than \(k\) reads and the other at least \(k\).

2 is 10 composed with 8, and 1 follows because the stuck configurations that adequacy excludes include every use-after-free and double-free: a dead cell matches no reduction rule (10).

Adequacy also yields the guarantee behind the read-only mode: a computation whose budget is read-only cannot change the state it runs over.

The read-only kind rules out writes and deallocations, so both content and liveness are preserved. The schedule is arbitrary because standardization (12) converts an interleaved run to an answer into a sequential run with the same endpoints, to which the sequential argument applies. 3 is this theorem composed with 8.

11.8 Standardization and Confluence↩︎

The remaining theorems relate the schedules of the small-step relation (10). They are stated up to trace equivalence: two traces are equivalent when, at every location, they perform the same sequence of external accesses and deallocations, where events on cells the trace itself allocated are internal and do not count. Formally, the external sequence of \(\tau\) at \(l\), relative to a set \(A\) of internal locations, is \[\begin{array}{lcll} \mathit{ext}^{A}_{l}(\cdot) &=& \cdot\\ \mathit{ext}^{A}_{l}((\ALLOC l')\,\tau) &=& \mathit{ext}^{A\cup\set{l'}}_{l}(\tau)\\ \mathit{ext}^{A}_{l}((\mu\,l)\,\tau) &=& \mu\;\mathit{ext}^{A}_{l}(\tau) &\text{if}\;l\notin A\\ \mathit{ext}^{A}_{l}((\DEALLOC l)\,\tau) &=& \CONSUME\;\mathit{ext}^{A}_{l}(\tau) &\text{if}\;l\notin A\\ \mathit{ext}^{A}_{l}(e\,\tau) &=& \mathit{ext}^{A}_{l}(\tau) &\text{otherwise,} \end{array}\] and \(\tau_1\treq\tau_2\) iff \(\mathit{ext}^{\set{}}_{l}(\tau_1) = \mathit{ext}^{\set{}}_{l}(\tau_2)\) for every \(l\). This is Mazurkiewicz trace equivalence: independent events may be reordered, conflicting events keep their order. A term is well-formed in \(H\) when every location it mentions is allocated in \(H\). The relations \(\redsto{\tau}\) and \(\seqredsto{\tau}\) are as in 11.4.

The final heap and answer are syntactically identical. Only the trace is reordered. The theorem carries no typing hypothesis: the authorization and non-interference guards of and already carry the separation content that makes the commutations sound, and typing is what guarantees the guards never block (4). It is the precise form of 5.

The renaming \(\pi\) accounts for the free choice of fresh locations at allocation. In the mechanization, condition (2) holds up to the capture annotations on parallel nodes: their growth depends on the order of interleaving, but the footprints they denote agree. Condition (4) does not follow from (3): trace equivalence discounts events on cells the runs themselves allocate, so it alone does not pin down read counts. It is what closes the budget-exhaustion case of 10.

The corollary is immediate from 13: answers do not reduce, so both closing runs are empty. It is the precise form of 6 and the operational content of data-race freedom: no observation of a well-typed program can depend on how its parallel compositions are scheduled.

11.9 Mechanization↩︎

The development is mechanized in Lean 4. All results are proved in full. The development contains no unproven obligations. The syntax, type system, and operational semantics are as in 10. The model of [app:meta:footprints,app:meta:worlds,app:meta:types,app:meta:exprel,app:meta:semtyping] lives in the Denotation module, the compatibility lemmas and 8 in Fundamental, the platform and adequacy theorems in Safety and SafetyReduce, and the schedule theorems in Semantics. The main theorems correspond to the following Lean declarations:

12 Translating Capybara to CoreCapybara↩︎

This appendix defines the type-preserving translation \(\embed{\cdot}\) from the surface calculus Capybara (3) to the core calculus CoreCapybara (10), states its correctness theorem, and proves it. The translation is the bridge that transfers CoreCapybara’s metatheory, soundness, memory safety, and data-race freedom, to Capybara.

12.1 Conventions↩︎

We fix the following conventions, which the surface presentation of 3 leaves implicit.

12.1.0.1 Root capabilities.

The two special capture variables \(\ANY\) and \(\FRESH\) are root capabilities. They dissolve into universal and existential capture quantification during translation. Recall from 3.2 that \(\mfree{C}\) removes every root capability from \(C\); call a capture set or type root-free when it mentions no root capability. All judgments of the translation are read over root-free sets: whenever a root capability would enter a capture position of a CoreCapybara type, the type translation has already consumed it into a bound capture variable.

12.1.0.2 Root-directedness.

A well-formed surface type is root-directed: occurrences of \(\ANY\) appear only as elements of the top-level capture set of a term-function domain, whose root-free part is access-only, and occurrences of \(\FRESH\) appear only in covariant (spine) positions, never in a function domain. The domain restriction on \(\ANY\) is what and already assume, read one arrow at a time: an \(\ANY\) nested deeper inside a domain sits in the domain of a nested arrow, and that arrow quantifies it itself. The codomain restriction on \(\FRESH\) is a stated convention, enforced by the surface well-formedness judgment \(\wf{\G}{T}\), which we assume. Under root-directedness each translated arrow binds a single capture variable \(\cstar\) for the (at most one) \(\ANY\) element of its domain’s top-level capture set, and a call instantiates \(\cstar\) with one capture set, exactly as and do with \(T[\ANY\leadsto\set{c}]\) and \(T[\ANY\leadsto D]\).

12.1.0.3 Domain honesty.

At every and instance, with domain top-level capture set \(C_T\) and argument \(y\) declared at capture set \(C_y\), we require the argument to resolve onto the domain’s root-free captures: every root of \(\mfree{C_T}\) is covered, at an equal or stronger mode, by a root of \(C_y\) (the covering order \(\sqsubseteq\) of 12.6). The domain’s root-free captures name capabilities the parameter actually holds, and the function body treats them as part of its footprint: it may assume them separate from what it captures, and the manufactured lock of 12.3 records that assumption, to be paid at every call from the caller’s own knowledge of the argument. An argument whose capture set under-runs the domain would make the assumption unpayable at the call while keeping it vacuously true of the actual argument; we exclude such applications. A domain whose only capture is \(\ANY\), the common case in 2, satisfies the requirement trivially.

12.1.0.4 Ambient contexts.

The translation is stated for derivations whose ambient context, the prefix of \(\G\) not introduced by a binder of the term under translation, declares term and type bindings only. Every capture variable of a translated context is then introduced by a translated binder and carries that binder’s lock or consume authority (12.4), which is what pays the fiat separations of (18). An ambient capture binding would arrive with neither, and a fiat separation between two such roots would have no translated image.

12.1.0.5 Context-indexed types.

The type translation resolves capture sets to their roots in the context where the type is read (12.3), so \(\embed{T}\) carries a context index that we leave implicit. The index is stable: a resolution consults only the bindings of the variables the resolved set mentions, so extending the context disturbs nothing, and a translated type weakens to any extension of its context unchanged.

12.1.0.6 Canonical derivations.

The translation is defined on typing derivations, and the theorem asserts that the judgment translates, so we may choose which derivation to translate. We choose a canonical one, which keeps two sources of slack out of the translated obligations: gratuitously wide witnesses and gratuitously widened subjects.

12.1.0.7 Translation on derivations.

The translation is defined on canonical typing derivations, and is compositional. The translated term inserts administrative forms, capture applications, locks and unlocks, packs and unpacks, that carry no source syntax but discharge the bookkeeping that CoreCapybara makes explicit. We write \(\embed{\cdot}\) for the translation of every syntactic class; context disambiguates.

12.2 Translating Capture Sets, Bounds, and Permissions↩︎

12.2.0.1 Capture sets.

\(\embed{C}\) acts elementwise, preserving variable names and access modes: \[\embed{\set{\mu_1\,\theta_1,\ldots,\mu_n\,\theta_n}} = \set{\mu_1\,\theta_1,\ldots,\mu_n\,\theta_n} \quad\text{for root-free}\;\theta_i.\] Root capabilities never occur in a translated capture position; they are removed by \(\mfree{\cdot}\) or turned into bound capture variables by the type translation.

12.2.0.2 Mode application.

Mode application commutes with translation.

12.2.0.3 Bounds.

A surface capture bound is a capture set or a mutability. Capture sets translate as above. Mutabilities translate to the trivial core bound: \[\embed{\epsilon} = \top,\qquad \embed{\RO} = \top.\] A mutability bound carries no separation content of its own in CoreCapybara, where the trivial bound is \(\top\). Its kinding force is recovered elsewhere: an \(\RO\) bound additionally contributes a mode-context entry \((\set{c}:\RO)\) to the lock manufactured at the binder that introduces \(c\) (12.3), which is what lets pay the source uses of and .

12.2.0.4 Permissions.

Both systems qualify capturing types with a permission \(m\), and the translation carries it over verbatim: \[\embed{m\,S\capt C} = m\,\embed{S}\capt \embed{C}, \qquad \embed{S} = \embed{S}\;\text{(pure case)}.\] The permission is a qualifier on the capturing type, not an operation on its capture set: \(\embed{C}\) is translated element-wise and \(m\) never touches it. Every rule that reads or writes a permission does so through the type former: preserves the binding’s qualifier on its refined singleton, keeps it rigid on both sides, introduces the read-only view of a reference at \(\RO\,\REF[T]\capt\set{\RO\,x}\), and demands an \(\RO\)-qualified subject. Because matches only the default qualifier, a reader-typed alias can never appear as the subject of a write: the qualifier plays exactly the role of the mechanization’s separate reader type constructor, which realizes the same distinction as a shape. Mode qualification of capture sets (\(\RO\,C\), \(\CONSUME\,C\)) is an independent, element-wise operation used by charges and subcapturing (, ) and is likewise translated unchanged.

12.3 Translating Types↩︎

Type translation comes in two variants. The plain translation \(\embed{T}\) is used in domains and other invariant or contravariant positions, where \(\FRESH\) never occurs (root-directedness). The result translation \(\eemb{T}\) is used in covariant result positions, let-bound terms and function codomains, where \(\FRESH\) may occur; it closes the \(\FRESH\) occurrences into an existential: \[\eemb{T} = \begin{cases} \EXCAP{c_1,\ldots,c_n}\,\embed{\freshinst{T}{\set{c_1},\ldots,\set{c_n}}} & \text{if T mentions \FRESH},\\ \embed{T} & \text{otherwise}, \end{cases}\] binding one capture variable per \(\FRESH\) occurrence, matching . For root-free \(T\) the two variants coincide.

12.3.0.1 Plain translation.

The base and capturing cases are homomorphic: \[\embed{\top} = \top, \qquad \embed{X} = X, \qquad \embed{m\,S\capt C} = m\,\embed{S}\capt \embed{C}.\] Every function former, term, consumer, capture, and type function alike, manufactures a lock at its capturing type; their clauses follow the next definition.

12.3.0.2 Root entries.

The manufactured locks are built from resolved roots. For a root set \(P\) (10), whose elements are moded capture variables \(\mu\,p\), write \(P\vert_p\) for the restriction of \(P\) to the atoms over the variable \(p\), and \[\langle P\rangle \;=\; P\vert_{p_1},\;\ldots,\;P\vert_{p_k}, \qquad p_1,\ldots,p_k\;\text{the distinct capture variables of}\;P,\] for the root entry list of \(P\): one separation-context entry per capture variable, each collecting every access mode at which its variable occurs in \(P\). No two entries share a variable, so a lock built from \(\langle P\rangle\) asserts pairwise separation of distinct roots and never demands a root’s separation from itself. For a function type \(A\) read in context \(\G\), define its root set \[R_A \;=\; \begin{cases} \roots{\G}{\mfree{C\cup C_T}} & A=m\,(\forall(\alpha\,x:T)U)\capt C,\;\text{with C_T the top-level captures of T},\\ \roots{\G}{\mfree{C}} & A=m\,(\forall[c<:B]U)\capt C\;\text{or}\;A=m\,(\forall[X<:S]U)\capt C. \end{cases}\] \(R_A\) resolves, once, at the type former, everything the arrow’s capture annotation and, for a term function, its domain’s root-free captures reach. It is the translated counterpart of the shallow part of the spine capture set \(|A|\): the deeper positions of \(|A|\) belong to the nested arrows of \(A\), each of which manufactures its own lock.

12.3.0.3 Term functions.

Let \(A=m\,(\forall(x:T)U)\capt C\) be an access-only term-function type, so its parameter carries consume mode \(\alpha=\epsilon\). The translation is \[\embed{A} = m\,\Big(\forall[\cstar<:\top]\;\forall\big(x:\embed{\anyinst{T}{\set{\cstar}}}\big)\; ([\Psi_A,\Phi_A]\,\eemb{U})\capt W_A\Big)\capt \embed{C},\] with the lock manufacture and the codomain annotation \[\Psi_A = \set{\cstar}\,,\;\langle \embed{R_A}\rangle, \qquad \Phi_A = \emptyset, \qquad W_A = \set{\cstar}\cup\embed{R_A}.\] The separation context \(\Psi_A\) has one entry for the parameter root \(\set{\cstar}\) and one entry per root of \(R_A\); through it records that the parameter is separated from every root the function’s annotation and domain reach, and that those roots are pairwise separated. These are exactly the separations the body may assume by fiat (): the body’s charge is \(C\cup\set{x}\), whose roots are \(R_A\cup\set{\cstar}\), the entry variables (18). The codomain annotation \(W_A\) is the same root set read as a capture set: the translated body charge subcaptures it by resolving each of its own atoms upward (8), which is what lets the translated abstraction carry the annotation its type states (12.8). The mode context of a term-function lock is empty; mode entries arise only at \(\RO\)-bounded capture binders below. The single bound variable \(\cstar\) instantiates the (at most one) \(\ANY\) of the domain, and \(\anyinst{T}{\set{\cstar}}\) denotes \(T\) with it replaced by \(\set{\cstar}\).

12.3.0.4 Consume-mode term functions.

When the parameter carries \(\alpha=\CONSUME\), the arrow translates to a CoreCapybara consumer type, whose argument is packed with its own capture witness so that the body may consume the root: \[\begin{align} \embed{m\,(\forall(\CONSUME\,x:T)U)\capt C} = m\,\Big( &\forall\big(\langle\cstar,x\rangle:\EXCAP{\cstar}\embed{\anyinst{T}{\set{\cstar}}}\big)\\[-2pt] &\;([\Psi_A,\Phi_A]\,\eemb{U})\capt W_A\Big)\capt \embed{C}, \end{align}\] with \[\Psi_A = \set{\cstar,\CONSUME\,\cstar}\,,\;\langle \embed{R_A}\rangle, \qquad \Phi_A = \emptyset, \qquad W_A = \set{\cstar,\CONSUME\,\cstar}\cup\embed{R_A}.\] The consumer binds \(\CONSUME\,\cstar<:\top\) (), so its body may consume the root; accordingly the parameter entry and the codomain annotation carry both modes of \(\cstar\), the image of the body charge \(D=\set{c,\CONSUME\,c}\) of in the consume case.

12.3.0.5 Capture functions.

Let \(A=m\,(\forall[c<:B]U)\capt C\). The translation is \[\embed{A} = m\,\Big(\forall[c<:\embed{B}]\;([\Psi_A,\Phi_A]\,\eemb{U})\capt W_A\Big)\capt \embed{C}, \qquad \Psi_A = \set{c}\,,\;\langle \embed{R_A}\rangle, \qquad W_A = \set{c}\cup\embed{R_A},\] with one mode entry paying an \(\RO\) bound: \[\Phi_A = \begin{cases} (\set{c}:\RO) & \text{if } B = \RO,\\ \emptyset & \text{otherwise.} \end{cases}\] When \(B=\RO\) the parameter is bounded by \(\top\) in the translated type (\(\embed{\RO}=\top\)), and the mode entry restores that \(\set{c}\) has kind \(\RO\) inside the codomain through ; a capture-set bound translates to the capture set itself and contributes no mode entry. The parameter entry \(\set{c}\) is not redundant: charges the body at \(C\cup\set{c}\), so the body may pair \(c\) against the roots of \(C\) in its own separation premises, and the entry is what pays those pairs. The bound \(B\) contributes nothing to \(\Psi_A\): locks record what the body assumes, and the body’s charge reaches \(B\) only through \(c\) itself.

12.3.0.6 Type functions.

Let \(A=m\,(\forall[X<:S]U)\capt C\). The translation is \[\embed{A} = m\,\Big(\forall[X<:\embed{S}]\;([\Psi_A,\Phi_A]\,\eemb{U})\capt W_A\Big)\capt \embed{C}, \qquad \Psi_A = \langle \embed{R_A}\rangle, \qquad \Phi_A = \emptyset, \qquad W_A = \embed{R_A}.\] A type binder introduces no root, so the lock has no parameter entry, only the pairwise entries of the annotation’s roots: a type-function body may still fire between two captured roots, and its lock is what pays for it. Correspondingly carries no separation premise, and the translated type application discharges its unlock from the ambient pairwise separations alone (12.8): the surface rule and the manufactured lock ask for the same thing.

12.4 Translating Contexts↩︎

Contexts translate pointwise: \[\embed{\emptyset}=\emptyset,\quad \embed{\G,x:T}=\embed{\G},x:\embed{T},\quad \embed{\G,X<:S}=\embed{\G},X<:\embed{S},\quad \embed{\G,\alpha\,c<:B}=\embed{\G},\alpha\,c<:\embed{B},\] where the source consume mode \(\alpha\in\set{\epsilon,\CONSUME}\) maps to itself and \(\embed{\epsilon}=\embed{\RO}=\top\) on bounds.

The manufactured locks do not live in \(\embed{\G}\) globally. They enter the context only where the translated term pushes a lock, at a , , or binder. We write \(\embed{\G}^{\LOCK}\) for the translated context interleaved with the frames pushed by the enclosing translated binders, and define it alongside the term translation. A source context extension contributes one frame per binder passed on the way from the ambient context to the site:

• a term binder \(\lambda(\alpha\,x:T)\) with arrow \(A\) contributes \(\alpha\,\cstar<:\top,\;x:\embed{\anyinst{T}{\set{\cstar}}},\; \LOCK[\Psi_A,\Phi_A]\), where in the consume case the pair \(\cstar,x\) is bound by a single frame;

• a capture binder \(\lambda[c<:B]\) with arrow \(A\) contributes \(\epsilon\,c<:\embed{B},\;\LOCK[\Psi_A,\Phi_A]\);

• a type binder \(\lambda[X<:S]\) with arrow \(A\) contributes \(X<:\embed{S},\;\LOCK[\Psi_A,\Phi_A]\);

• a root-free contributes \(x:\embed{T}\), and a \(\FRESH\)-carrying contributes the frame \(\CONSUME\,c_1<:\top,\ldots,\CONSUME\,c_n<:\top,\; \LOCK[\Psi_w,\Phi_w],\;x:\embed{\freshinst{T}{\set{c_1},\ldots,\set{c_n}}}\) with the ownership lock of .

The lock of each frame is available to every subderivation nested inside its binder, which is what makes the manufactured separations of 12.3 usable in the body. The kill operators \(\ominus\) that core and apply to their continuations are not part of \(\embed{\G}^{\LOCK}\): the main induction produces continuation derivations in the unkilled context and places them under the kill by 19.

12.5 Translating Terms↩︎

Term translation is directed by the typing derivation: the translated term depends on which typing rule concludes the source derivation, since a bare surface variable may be typed by , , or . The homomorphic and short cases are collected in the table below; the cases that insert nontrivial administrative structure are described in the paragraphs that follow.

Here \([\Psi_A,\Phi_A]\) is the lock manufactured at the binder’s arrow type (12.3); all three abstraction forms push it, and all three application forms open it with an . The two rows are distinguished by whether the bound term’s declared type \(T\) carries \(\FRESH\): a root-free \(T\) translates to a , whereas a \(T\) with \(\FRESH\) translates to a , whose \(n\) freshly bound witnesses are exactly the roots \(c_1,\ldots,c_n\) that \(\eemb{T}\) packages. The charge match is exact: the extra use set \(\set{c_1,\ldots,c_n,\CONSUME\,c_1,\ldots,\CONSUME\,c_n}\) that adds to the continuation is the image of the body charge \(D\cup\CONSUME\,D\) of the source .

12.5.0.1 Abstraction.

An access-only abstraction translates to a capture lambda, a term lambda, and a lock, in that order, so that its body runs under the manufactured lock: \[\embed{\lambda(x:T)t} = \lambda[\cstar<:\top]\;\lambda\big(x:\embed{\anyinst{T}{\set{\cstar}}}\big)\; \LOCK[\Psi_A,\Phi_A]\;\embed{t}, \qquad A=(\forall(x:T)U)\capt C.\] A consume abstraction translates to a consumer lambda, whose bound pair \(\langle\cstar,x\rangle\) supplies the consumable root: \[\embed{\lambda(\CONSUME\,x:T)t} = \lambda\big(\langle\cstar,x\rangle:\EXCAP{\cstar}\embed{\anyinst{T}{\set{\cstar}}}\big)\; \LOCK[\Psi_A,\Phi_A]\;\embed{t}.\] In both cases the translated context at \(\embed{t}\) is \(\embed{\G}^{\LOCK}\) extended with the binder’s frame, as in 12.4.

12.5.0.2 Application.

An application instantiates the callee’s capture parameter with the argument’s \(\ANY\)-witness, applies, then unlocks: \[\embed{x\,y} = \LET x_1 = x[\embed{D}]\IN \LET x_2 = x_1\,y\IN \UNLOCK\,x_2,\] where \(D\) is the canonical witness of 1. The capture application \(x[\embed{D}]\) instantiates \(\cstar:=\embed{D}\): the callee’s translated type binds \(\cstar<:\top\), and with narrows \(\top\) to \(\embed{D}\) before . The term application then produces a value of the modal codomain \([\Psi_A,\Phi_A]\eemb{U}\) instantiated at the call, and \(\UNLOCK\,x_2\) opens it, discharging the satisfaction obligation of . The obligation asks for pairwise separation of the instantiated entries: \(\embed{D}\) against each root entry, the image of the source premise \(\sep{\G}{D}{|(\forall(z:T)U)\capt C|}\) at the shallow part of the spine, and the root entries pairwise, which the ambient locks supply (5). The access-only requirement of core on \(\embed{D}\) is the image of the premise \(\accessonly{\G}{D}\) through 11.

12.5.0.3 Consume application.

A consume application packs the argument with its witness and applies the consumer, then unlocks: \[\embed{x\,y} = \LET x_2 = x\,\langle\embed{D},y\rangle\IN \UNLOCK\,x_2.\] The synthesized pack \(\langle\embed{D},y\rangle\) has type \(\EXCAP{\cstar}\embed{\anyinst{T}{\set{\cstar}}}\) by : with \(n=1\) the pairwise disjointness is vacuous, \(\embed{D}\) is access-only and consumable (the source premise \(\consumable{\G}{D}\)), and the pack charges \(\embed{D}\cup\CONSUME\,\embed{D}\). then sequences this charge before \(\set{x}\), which splits into an access leg \(\seqcomp{}{\embed{D}}{\set{x}}\), free by from the access-only premise, and a consume leg \(\seqcomp{}{\CONSUME\,\embed{D}}{\set{x}}\), the translated image (4, 17) of the source premise \(\seqcomp{\G}{\CONSUME\,D}{\set{x}}\): the consumption of the argument’s witness sequences before the consumer runs.

12.5.0.4 Type and capture application.

\(\embed{x[S']}=\LET x_1=x[\embed{S'}]\IN\UNLOCK\,x_1\) and \(\embed{x[D]}=\LET x_1=x[\embed{D}]\IN\UNLOCK\,x_1\) open the manufactured lock exactly as an application does. For a type application the instantiated entries are the root entries alone, so the unlock carries no image of a source premise, matching , which has none: the ambient locks pay everything (5). For a capture application the entries are \(\embed{D}\) and the root entries, the image of the premise \(\sep{\G}{D}{|A|}\) at the shallow spine; the witness \(D\) is part of the source term and, by the revised , part of the source charge, which is what keeps its roots inside the ambient invariant’s reach (18).

12.5.0.5 Read-only occurrence.

A source occurrence typed by translates to the core reader value: for a reference-shaped subject \(x\), \(\embed{x}=\RO\,x\), and produces \(\RO\,\REF[\embed{T}]\capt\set{\RO\,x} =\eemb{\RO\,\REF[T]\capt\set{\RO\,x}}\) together with the charge \(\set{}\) primitively, with no coercion. This matches the mechanization, whose is specific to reference types and translates to its reader value; the \(\RO\) type qualifier is the flattened image of its reader shape. Following the mechanization, we read as specific to reference-shaped subjects (12.2). A occurrence at an \(\RO\)-qualified \(x\) needs no coercion at all: the qualifier rides on the type, which preserves.

12.5.0.6 Fresh occurrence.

A source occurrence typed by , retyping \(x\) from \(T[\FRESH\leadsto D_1,\ldots,D_n]\) to \(T\), translates to a pack at the translated existential \(\eemb{T}\): \[\embed{x} = \big\langle\;\embed{D_1},\ldots,\embed{D_n}\;,\;x\;\big\rangle,\] one witness per bound root of \(\eemb{T}=\EXCAP{c_1,\ldots,c_n}\embed{\freshinst{T}{\set{c_1},\ldots,\set{c_n}}}\) (one root per \(\FRESH\) occurrence, matching ). The pack charges \(\bigcup_i\embed{D_i}\cup\CONSUME\bigcup_i\embed{D_i}\), exactly the translated image of the source charge \(D\cup\CONSUME\,D\).

12.5.0.7 Subsumption.

A source step translates by 14 (subtyping preservation) and 10 (subcapturing preservation), followed by core .

12.5.0.8 State, parallelism, and conditionals.

The memory primitives, parallel composition, and conditionals (3.4) translate homomorphically, with two points of interest. An allocation keeps its form, and its types line up by the result translation: \(\eemb{\REF[T]\capt\set{\FRESH}} = \EXCAP{c}\REF[\embed{T}]\capt\set{c}\), the type of core . A read inserts the reader that core demands: \[\embed{\READ x} = \LET r = \RO\,x \IN \READ r,\] where types \(\RO\,x\) at \(\RO\,\REF[\embed{T}]\capt\set{\RO\,x}\) and the let charges the translated image \(\set{\RO\,x}\) of the source charge. Writes, deallocations, parallel compositions, and conditionals map to their core counterparts unchanged; their premises are the translated images of the source premises, using 16 for the separation premise of , whose payability hypothesis 18 discharges at the site, and 11 for the consumable premise of .

12.6 The Translation Theorem↩︎

The consuming forms of the surface calculus charge the access of what they consume alongside its consumption, and charging \(D\cup\CONSUME\,D\) and and binding \(\set{c,\CONSUME\,c}\), exactly as their translated images , , , and do. The translated use set is therefore bounded by \(\embed{C}\) itself.

The side condition is stated at the level of roots. Write \(P\sqsubseteq P'\) when every \(\mu\,\theta\in P\) has some \(\mu'\,\theta\in P'\) with \(\mu\preceq\mu'\), extending the mutability order with \(\CONSUME\preceq\CONSUME\). This is a statement-level device only: it never appears as the premise of a separation rule (a variable’s runtime footprint can strictly under-run its root, so root covering does not transport separation). Eager surface charging and lazy core charging differ exactly below variable resolution: the surface charges a variable occurrence \(\set{x}\) eagerly, while the core charges its uses at eliminations, but \(\set{x}\) and the declared capture set it resolves to have the same roots, so the two agree once resolved. The consumers of the theorem, the core access-only, consumable, and accessible predicates and the kill operation, are themselves root-based, so the root-level bound is exactly what they need.

The proof is in 12.8, by induction on the canonical source derivation, one case per rule, using the lemma stack of 12.7. Because the translated term is typed against \(\embed{T}\) and its uses are root-covered by \(\embed{C}\), and CoreCapybara’s dynamic semantics preserves both, the metatheory of 5 transfers to Capybara.

12.7 Lemma Stack↩︎

The proof of 14 rests on the following lemmas. Except where noted, each is by induction on the indicated derivation.

12.7.0.1 L1: Mode monotonicity.

4 already records \(\embed{\mu\,C}=\mu\,\embed{C}\). We add monotonicity of qualification.

12.7.0.2 L2: Roots.

Root resolution (10) underlies the lock manufacture, and four of its properties recur. Throughout, \(\sqsubseteq\) is the covering order of 12.6, and we use silently that resolution is multiplicative, \(\roots{\G}{\mu\,C}=\mu\,\roots{\G}{C}\), and distributes over union, both immediate from its definition, and that it commutes with the translation, \(\roots{\embed{\G}^{\LOCK}}{\embed{C}} = \embed{\roots{\G}{C}}\) for root-free \(C\), since the translation preserves every binding’s capture set elementwise and the interleaved frames bind no term variables that \(C\) mentions.

12.7.0.3 L3: Subcapturing preservation.

12.7.0.4 L4: Capability kinding, access-only, consumable, accessible.

12.7.0.5 L5: Substitution and instantiation.

The translated eliminations substitute a term variable, a type, or a capture set into a translated type. Away from the manufactured locks and codomain annotations, translation and substitution commute on the nose; at the locks, substitution replaces the resolved entries by written-level sets, and one subtyping cast re-relates the two.

12.7.0.6 L6: Subtyping preservation.

12.7.0.7 L7: Separation.

The surface leaf separates any two distinct roots by fiat; the core has no fiat, and the translation pays every pair from a lock, from consume authority, or from read-only kinding. The next lemma extracts from a surface separation everything the payment needs, the following definition names the payments, and the preservation lemma reconstructs the core derivation; which payments are available at a site is the business of 18.

12.7.0.8 L8: Sequential composition.

12.7.0.9 L9: The ambient invariant.

The payability hypotheses of [lem:tr:sep,lem:tr:seq] are discharged uniformly: at every site of the main induction, the roots of the site’s own charge and witnesses are pairwise payable. This is the translated image of ’s fiat, cut down from all pairs of roots in scope to the pairs the site can actually mention.

A site of a canonical derivation is a subderivation occurrence; its site root set \(\rho(s)\) is \(\roots{\G_s}{C_s}\) for its context \(\G_s\) and use set \(C_s\), together with \(\roots{\G_s}{D}\) for the witnesses \(D\) of its own and premises ( witnesses are already charged).

12.7.0.10 L10: Kill transport.

The core and type their continuation in the killed context \(\G\ominus C_1\), whereas the induction produces the translated continuation in the unkilled \(\embed{\G}^{\LOCK}\). The bridge is that translated derivations consult consume authority only at charged roots, which sequencing keeps live.

The main induction produces derivations that are authority-robust for \(X_s=\embed{\rho(s)}\), the translated site root set: every elimination’s subject is charged by the source (surface charges occurrences eagerly), every consumable premise concerns a charged or witness set, and every instance introduced by [lem:tr:sep,lem:tr:seq,lem:tr:disj,lem:tr:invariant] pairs atoms of \(\rho(s)\). The let case of 12.8 verifies that the killed roots avoid exactly this set.

12.8 Proof of the Translation Theorem↩︎

We prove 14 by induction on the canonical source derivation, one case per rule. Throughout, \(C'\) denotes the translated use set, verified root-covered by \(\embed{C}\); unless stated, the translated result type is \(\eemb{T}\) by construction. Three recurring facts are used without further comment. Stamping: whenever \(\roots{\embed{\G}^{\LOCK}}{C'}\sqsubseteq W\) for a root-level capture set \(W\), also \(\subs{\embed{\G}^{\LOCK}}{C'}{W}\), by 8 followed by , , and on the covering; this is what matches a translated body charge against the stated annotation \(W_A\) and a translated use set against a root-closure slot. Robustness: each case’s derivation is authority-robust for \(\embed{\rho(s)}\) (3), by inspection of its leaves. Consumed charges: every \(\CONSUME\)-marked atom of a translated use set either belongs to a translated , , , or charge, each guarded by a consumable premise translated through 11, or resolves from an annotation stamped from such a charge, so its variable is \(\CONSUME\)-bound.

12.8.0.1 .

\(\embed{x}=x\). The translated binding is \(x:m\,\embed{S}\capt\embed{C}\), so gives \(\typ{\set{}}{\embed{\G}^{\LOCK}}{x}{m\,\embed{S}\capt\set{x}}\), which is \(\eemb{m\,S\capt\set{x}}\) for either \(m\): source and core preserve the binding’s qualifier on the same plain singleton. Uses: \(\set{}\), trivially below.

12.8.0.2 .

\(\embed{x}=\RO\,x\). By the convention of 12.5 the subject is reference-shaped, \(x:\REF[T]\capt C\in\G\), so gives \(\typ{\set{}}{\embed{\G}^{\LOCK}}{\RO\,x}{\RO\,\REF[\embed{T}]\capt\set{\RO\,x}} =\eemb{\RO\,\REF[T]\capt\set{\RO\,x}}\) primitively, with no coercion. Uses: \(\set{}\), trivially below the source charge \(\set{\RO\,x}\).

12.8.0.3 .

\(\embed{x}=\langle\embed{D_1},\ldots,\embed{D_n},x\rangle\). \(x\)’s declared type is \[[c_1:=\embed{D_1},\ldots,c_n:=\embed{D_n}]\,\embed{\freshinst{T}{\set{c_1},\ldots,\set{c_n}}}\] (12), so applies: each \(\embed{D_i}\) is access-only and consumable (11 on the rule’s premises), and the witnesses are pairwise disjoint, \(\disj{}{\embed{D_i}}{\embed{D_j}}\) for \(i\neq j\), by 4 on the rule’s disjointness premises, whose sides the rule’s other premises make consumable. The pack has type \(\eemb{T}=\EXCAP{c_1,\ldots,c_n}\embed{\freshinst{T}{\set{c_1},\ldots,\set{c_n}}}\) and charges \(\bigcup_i\embed{D_i}\cup\CONSUME\bigcup_i\embed{D_i} =\embed{D\cup\CONSUME\,D}\) (4), exactly the source charge.

12.8.0.4 .

By 14 on the type, 10 on the use set, and ; the side condition follows by 7.

12.8.0.5 .

For \(\alpha=\epsilon\), \[\embed{\lambda(x:T)t}=\lambda[\cstar<:\top]\lambda(x:\embed{\anyinst{T}{\set{\cstar}}})\LOCK[\Psi_A,\Phi_A]\embed{t}.\] The source premise types \(t\) at \(C\cup\set{x}\), so the IH types \(\embed{t}\) at a charge \(C'\) with \(\roots{}{C'}\sqsubseteq\embed{\roots{\G'}{C\cup\set{x}}} = \embed{R_A}\cup\set{\cstar}\), the atoms of \(W_A\), under the binder’s frame (12.4). stamps that charge onto the codomain modal as \(([\Psi_A,\Phi_A]\eemb{U})\capt C'\), and with stamping widens \(C'\) to the stated annotation \(W_A\). abstracts \(x\) and abstracts \(\cstar\) (premise: \(\top\) is access-only); the value’s outer capture \(\set{}\) is widened to \(\embed{C}\) by , giving \(\eemb{(\forall(x:T)U)\capt C}\). For \(\alpha=\CONSUME\) a frame replaces +; its body charge additionally carries \(\set{\cstar,\CONSUME\,\cstar}\), the image of the source \(D=\set{c,\CONSUME\,c}\), and the stamping target is \(W_A=\set{\cstar,\CONSUME\,\cstar}\cup\embed{R_A}\). Uses: \(\set{}\).

12.8.0.6 , .

As for with one binder fewer: \(\embed{\lambda[X<:S]t}=\lambda[X<:\embed{S}]\LOCK[\Psi_A,\Phi_A]\embed{t}\) types by around , and \(\embed{\lambda[c<:B]t}=\lambda[c<:\embed{B}]\LOCK[\Psi_A,\Phi_A]\embed{t}\) by (its premise \(\accessonly{\G}{\embed{B}}\) by 11, with \(\top\) access-only by definition) around . The body charges resolve into \(\embed{R_A}\cup\set{c}\) resp.\(\embed{R_A}\), and stamping widens them to \(W_A\). Both charge \(\set{}\) at the conclusion, as their source rules do.

12.8.0.7 .

\(\embed{x\,y}=\LET x_1=x[\embed{D}]\IN\LET x_2=x_1\,y\IN\UNLOCK\,x_2\), with \(D\) the canonical witness. By canonicity the callee premise concludes at the declared type, translated \[m\big(\forall[\cstar<:\top]\forall(z:\embed{\anyinst{T}{\set{\cstar}}})\,([\Psi_A,\Phi_A]\eemb{U})\capt W_A\big)\capt\embed{C}.\] with and narrows the bound \(\top\) to \(\embed{D}\), and instantiates \(\cstar:=\embed{D}\); its premise \(\accessonly{\G}{\embed{D}}\) is the image of the source premise through 11, and it charges \(\set{}\). The domain of the instantiated arrow is \([\cstar:=\embed{D}]\,\embed{\anyinst{T}{\set{\cstar}}} =\embed{\anyinst{T}{D}}\) on the nose: by root-directedness the sole \(\ANY\) sits in the domain’s top-level capture set, which is translated elementwise (12). The IH on the argument premise types \(y\) at exactly this type, so applies, charging \(\set{x_1}\) and producing \([z:=y][\cstar:=\embed{D}]\big(([\Psi_A,\Phi_A]\eemb{U})\capt W_A\big)\), which 13 casts to the translation of the instantiated source codomain. \(\UNLOCK\,x_2\) (charge \(\set{}\)) opens the modal, discharging its satisfaction by 5, and returns \(\eemb{[z:=y]U}\). The administrative lets sequence trivially: -style inert charges make the first head \(\set{}\) () and the unlock continuation \(\set{}\) ( via and ). Uses: \(\set{x_1}\), whose roots are the atoms of the instantiated \(W_A\), covered by \(\embed{\roots{\G}{\set{x,y}}}\): the \(R_A\)-part equals \(\roots{\G}{\set{x}}\) (declared annotation) and the witness part satisfies \(\roots{\G}{D}\sqsubseteq\roots{\G}{\set{y}}\) (tightness).

12.8.0.8 .

\(\embed{x\,y}=\LET x_2=x\,\langle\embed{D},y\rangle\IN\UNLOCK\,x_2\). The callee translates to a consumer type. forms \(\langle\embed{D},y\rangle:\EXCAP{\cstar}\embed{\anyinst{T}{\set{\cstar}}}\) (charge \(\embed{D}\cup\CONSUME\,\embed{D}\); access-onliness and consumability from the source premises through 11). applies \(x\), requiring \(\seqcomp{\G}{\embed{D}\cup\CONSUME\,\embed{D}}{\set{x}}\): splits it into the access leg, free by , and the consume leg \(\seqcomp{}{\CONSUME\,\embed{D}}{\set{x}}\), given by 17 on the source premise \(\seqcomp{\G}{\CONSUME\,D}{\set{x}}\) with payability from 18 (\(D\) is charged at this site). opens the codomain by 5, after 13 casts the substituted codomain. The charge \(\embed{D}\cup\CONSUME\,\embed{D}\cup\set{x}\) lies below the source charge \(\embed{\set{x,y}\cup D\cup\CONSUME\,D}\) by .

12.8.0.9 , .

\(\embed{x[S']}=\LET x_1=x[\embed{S'}]\IN\UNLOCK\,x_1\): with narrows the bound from \(\embed{S}\) to \(\embed{S'}\) (using \(\subs{\G}{S'}{S}\) through 14), instantiates, and opens the lock, whose entries the type substitution does not touch (12); 5 discharges the satisfaction from the ambient invariant alone, and the result is \([X:=\embed{S'}]\eemb{U}=\eemb{[X:=S']U}\). \(\embed{x[D]}=\LET x_1=x[\embed{D}]\IN\UNLOCK\,x_1\): narrows the translated bound to \(\embed{D}\) (10 for a capture-set bound, for a translated mutability bound), instantiates \(c:=\embed{D}\) (access-only premise through 11), 13 casts the substituted codomain, and opens the lock by 5, whose witness pairs are payable because the revised charges \(D\); when \(B=\RO\) the mode leg is the image of the kinding (11). In both cases every translated charge is \(\set{x}\), directly corresponding to the source charge, and the administrative let sequences by .

12.8.0.10 .

Let \(C_1,C_2\) be the source charges and \(C_1',C_2'\) the translated ones from the IHs. Both forms instantiate their core rule with the head slot \(C_1'\) and the root-closure continuation slot \(\widehat{C_2}=\embed{\roots{\G}{C_2}}\) (plus, for , the witness uses the rule adds); the continuation’s typing is widened from \(C_2'\) to \(\widehat{C_2}\) by and stamping, and the closure adds no roots, so the side condition for the total \(C_1'\cup\widehat{C_2}\) still reads \(\sqsubseteq\embed{\roots{\G}{C_1\cup C_2}}\). The sequencing premise \(\seqcomp{}{C_1'}{\widehat{C_2}}\) is derived as in 17: traces \(C_1'\) to its roots, covered by \(\embed{\roots{\G}{C_1}}\); access-only atoms close by ; and a \(\CONSUME\)-marked atom is, by 15 on the source premise \(\seqcomp{\G}{C_1}{C_2}\), over a variable outside \(\roots{\G}{C_2}\), so its pairs are payable (18) and closes it.

The continuation’s IH derivation lives in the unkilled context, and 19 places it under the kill: it is authority-robust for \(X=\embed{\roots{\G}{C_2}}\) together with the continuation’s witnesses and locally bound roots, and the killed variables, the \(\CONSUME\)-marked roots of \(C_1'\), avoid \(X\): they avoid \(\roots{\G}{C_2}\) by 15 as above, they avoid the witnesses because a witness is tight or charged, hence inside \(\roots{\G}{C_2}\)-coverage, and local roots are bound after the kill.

When \(T\) is \(\FRESH\)-free the translated term is \(\LET x=\embed{t}\IN\embed{u}\), typed by ; the continuation’s result type \(\eemb{U}\) and every payload pass through the kill unchanged, since \(\ominus\) rewrites authorities only. When \(T\) carries \(\FRESH\), \(\embed{\LET x=t\IN u}=\LET\langle c_1,\ldots,c_n,x\rangle=\embed{t}\IN\embed{u}\), typed by . The match is exact: binds each \(\CONSUME\,c_i<:\top\) and adds \(\set{c_1,\ldots,c_n,\CONSUME\,c_1,\ldots,\CONSUME\,c_n}\) to the continuation’s use set, the images of the source ’s \(\CONSUME\,c_i\) bindings and its body charge \(D\cup\CONSUME\,D\); the consumed roots of \(C_1'\) are consumable by the consumed-charges fact. The rule pushes the ownership lock \(\Psi_w=\set{c_1,\ldots,c_n,\CONSUME\,c_1,\ldots,\CONSUME\,c_n}\,,\; \widehat{C_2}\), whose root-level continuation entry is exactly what the continuation case of 18 reads; the lock imposes no obligation on the continuation (it is read, not proved, at the binder).

12.8.0.11 State, parallelism, and conditionals.

, , , and map to their core namesakes with the premises translated by 11; inserts the reader as in 12.5, its administrative let sequencing by (a reader value charges nothing). maps to , whose separation premise is 16 on the source premise, with payability from 18: both branch charges are part of the site’s charge. Charges are the translated images of the source charges throughout.

This completes the induction, establishing 14.0◻

12.9 Example: runParallel↩︎

We trace the runParallel pattern of 2 through the translation, exercising the lock manufacture of 12.3 and the satisfaction discharge of 5. Use a type variable \(X\) (declared \(X<:\top\)) for the resource shape, take \(\TUNIT\) and \(()\) as a base type and its value as in the core calculus, and abbreviate \(T_a=X\capt\set{\ANY}\), a resource whose capture is a fresh \(\ANY\). Take \[T_{\textsf{rp}}=\forall(op_1:T_a)\,\big((\forall(op_2:T_a)\TUNIT)\capt\set{op_1}\big),\] the curried type of runParallel: applied to \(op_1\) it returns a closure that has captured \(op_1\) and awaits \(op_2\), and running the two together requires \(op_2\) separate from \(op_1\). The context declares \(\textsf{rp}:T_{\textsf{rp}}\) and a primitive \(\textsf{alloc}:\forall(y:\TUNIT)(X\capt\set{\FRESH})\) producing fresh resources. The source program is \[\LET f_1=\textsf{alloc}\,()\IN \LET f_2=\textsf{alloc}\,()\IN \textsf{rp}\,f_1\,f_2.\] Each \(\LET\) binds a fresh consumable root; write \(c_1,c_2\) for them, so \(f_1:X\capt\set{c_1}\), \(f_2:X\capt\set{c_2}\) with \(c_1\neq c_2\). The first application \(\textsf{rp}\,f_1\) carries the trivial separation \(\sep{\G}{\set{f_1}}{|T_{\textsf{rp}}|}=\sep{\G}{\set{f_1}}{\set{}}\); the second, \((\textsf{rp}\,f_1)\,f_2\), carries the real one \(\sep{\G}{\set{f_2}}{\set{f_1}}\), since the residual callee \((\forall(op_2:T_a)\TUNIT)\capt\set{f_1}\) has footprint \(\set{f_1}\). discharges it, \(c_1\neq c_2\).

12.9.0.1 Translated type.

By 12.3, \(\embed{T_{\textsf{rp}}}\) manufactures one lock per arrow: \[\begin{align} \embed{T_{\textsf{rp}}}= \forall[c_{\star1}{<:}\top]\,\forall(op_1{:}X\capt\set{c_{\star1}})\,\Big( &[\Psi_1,\emptyset]\,\big(\forall[c_{\star2}{<:}\top]\,\forall(op_2{:}X\capt\set{c_{\star2}})\\[-2pt] &\quad([\Psi_2,\emptyset]\,\TUNIT)\capt\set{c_{\star2},c_{\star1}}\big)\capt\set{op_1}\Big)\capt\set{c_{\star1}}, \end{align}\] \[\text{with}\quad \Psi_1=\set{c_{\star1}} \qquad\text{and}\qquad \Psi_2=\set{c_{\star2}},\;\set{c_{\star1}}.\] The outer lock \(\Psi_1\) has a single entry, the parameter root: the outer arrow’s annotation is empty, so \(R_{A_1}=\set{}\), and a one-entry lock demands no pairs; its satisfaction is vacuous. The inner arrow captures \(op_1\), so \(R_{A_2}=\roots{\G}{\set{op_1}}=\set{c_{\star1}}\), and \(\Psi_2\) records that \(op_2\)’s root \(c_{\star2}\) is separate from \(op_1\)’s root \(c_{\star1}\): the entries are individual roots, resolved once, at the type former, and a body-internal fiat pair is read off them by directly. This is the translated content of “supplying \(op_2\) requires it separate from \(op_1\)”. The codomain annotations are the same root sets read as capture sets, \(W_{A_1}=\set{c_{\star1}}\) and \(W_{A_2}=\set{c_{\star2},c_{\star1}}\); a user-written runParallel, whose inner body applies \(op_2\) and charges \(\set{op_1,op_2}\), stamps that charge onto them by resolution (12.8), so the manufactured arrow is inhabited by an actual abstraction and not only by the context primitive \(\textsf{rp}\).

12.9.0.2 Translated term.

The nested application is administratively normalized, each \(\embed{x\,y}\) expanding as in 12.5: \[\begin{align} &\LET\langle c_1,f_1\rangle=\embed{\textsf{alloc}\,()}\IN \LET\langle c_2,f_2\rangle=\embed{\textsf{alloc}\,()}\IN{}\\ &\quad\LET g=\big(\LET a_1{=}\textsf{rp}[\set{f_1}]\IN\LET a_2{=}a_1\,f_1\IN\UNLOCK\,a_2\big)\IN{}\\ &\quad\LET b_1{=}g[\set{f_2}]\IN\LET b_2{=}b_1\,f_2\IN\UNLOCK\,b_2. \end{align}\] The two \(\LET\langle c_i,f_i\rangle\) are s of the fresh results, binding \(\CONSUME\,c_i<:\top\). The capture applications instantiate \(c_{\star1}:=\set{f_1}\) and \(c_{\star2}:=\set{f_2}\), narrowing \(\top\) by first; the witnesses are the canonical (tight) ones, the arguments’ declared capture sets.

12.9.0.3 Satisfaction discharge.

Each \(\UNLOCK\) discharges the satisfaction of the instantiated lock.

• \(\UNLOCK\,a_2\): the instantiated \(\Psi_1[c_{\star1}{:=}\set{f_1}] =(\set{f_1})\) has a single entry, so demands no pair. This is the image of the trivial source separation against the empty spine.

• \(\UNLOCK\,b_2\): the instantiated \(\Psi_2[c_{\star1}{:=}\set{f_1}][c_{\star2}{:=}\set{f_2}] =(\set{f_2},\set{f_1})\) requires \(\sep{\G}{\set{f_2}}{\set{f_1}}\). Both entries resolve upward to the distinct \(\top\)-bounded consumable roots \(c_2,c_1\) (8), gives \(\sep{\G}{\set{c_2}}{\set{c_1}}\), and descends to the entries. This is 5 at the site: the witness pair is distinct by the source premise \(\sep{\G}{\set{f_2}}{\set{f_1}}\) (15) and payable by the ambient invariant (18), here through the consume authority of the two unpacked roots.

Had the call instead passed two views of a single resource \(f\), both applications would instantiate the same \(\set{f}\), and the inner obligation would be \(\sep{\G}{\set{f}}{\set{f}}\), underivable because the two roots coincide. The manufactured lock thus rejects exactly the racy call, as 2 requires.

References↩︎

---

1. Capybaras are known for living peacefully alongside others. The name is a phonetic pun for “capabilities and borrowing”.↩︎

2. The Lean 4 mechanization was developed with AI assistance. It is used to do proof engineering work.↩︎