Typed Memory Management in a Calculus of Capabilities^{∗}

David Walker Cornell University

Karl Crary Carnegie Mellon University Greg Morrisett Cornell University

February 12, 2000

Abstract

Region-based memory management is an alternative to standard tracing garbage collection that makes potentially dangerous operations such as memory deallocation explicit but verifiably safe. In this article, we present a new compiler intermediate language, called the Capability Calculus, that supports region-based memory management and enjoys a provably safe type system. Unlike previous region-based type systems, region lifetimes need not be lexically scoped and yet the language may be checked for safety without complex analyses. Therefore, our type system may be deployed in settings such as extensible operating systems where both the performance and safety of untrusted code is important.

The central novelty of the language is the use of static capabilities to specify the permissibility of various operations, such as memory access and deallocation. In order to ensure capabilities are relinquished properly, the type system tracks aliasing information using a form of bounded quantification. Moreover, unlike previous work on region-based type systems, the proof of soundness of our type system is relatively simple, employing only standard syntactic techniques.

In order to show our language may be used in practice, we show how to translate a variant of Tofte and Talpin’s high-level type-and-effects system for region-based memory management into our language. When combined with known region inference algorithms, this translation provides a way to compile source-level languages to the Capability Calculus.

1 Motivation and Background

A current trend in systems software is to allow untrusted extensions to be installed in protected services, relying upon language technology to protect the integrity of the service instead of hardware-based protection mechanisms [24, 51, 4, 35, 33, 22, 19]. For example, the SPIN project [4] relies upon the Modula-3 type system to protect an operating system kernel from erroneous extensions. Similarly, web browsers rely upon the Java Virtual Machine byte-code verifier [24] to protect users from malicious applets. In both situations, the goal is to eliminate expensive communications or boundary crossings by allowing extensions to directly access the resources they require.

∗This research was performed while the first author was at Cornell University. This material is based on work supported in part by the AFOSR grant F49620-97-1-0013, ARPA/RADC grant F30602-96-1-0317 and NSF grant No. EIA 97-03470.

Any opinions, findings, and conclusions or recommendations expressed in this publication are those of the authors and do not reflect the views of these agencies.

Recently, Necula and Lee [36, 35] have proposed Proof-Carrying Code (PCC) and Morrisett et al. [34, 33] have suggested Typed Assembly Language (TAL) as language technologies that provide the security advantages of high-level languages, but without the overheads of interpretation or just-in-time compilation. In both systems, low-level machine code can be heavily optimized, by hand or by compiler, and yet be automatically verified through proof- or type-checking.

However, in all of these systems (SPIN, JVM, TAL, and Touchstone [37], a compiler that generates PCC), there is one aspect over which programmers and optimizing compilers have little or no control: memory management. In particular, their soundness depends on memory being reclaimed by a trusted garbage collector. Hence, applets or kernel extensions may not perform their own optimized memory management. Furthermore, as garbage collectors tend to be large, complicated pieces of unverified software, the degree of trust in language-based protection mechanisms is diminished.

The goal of this work is to provide a high degree of control over memory management for programmers and compilers, but as in the PCC and TAL frameworks, make verification of the safety of programs a straightforward task.

1.1 Regions

Tofte and Talpin [47, 48] suggest a type and effects system for verifying the soundness of region-based memory management. In later work, Tofte and others show how to infer region types and lifetimes and how to implement their theory [46, 5, 6]. There are several advantages to region-based memory management; from our point of view, the two most important are:

1. Region-based memory management can be implemented using relatively simple constant-time routines.

2. All memory operations explicit in the program text, but safety is guaranteed.

The first advantage has several implications. If regions are used in a secure system then the simplicity of the implementation leads to a smaller trusted computed base. Moreover, it may be possible to formally verify that the region operations are implemented correctly. In contrast, a standard tracing garbage collector is a large and extremely complicated piece of code; a formal analysis of a garbage collector would be a much more onerous task than an analysis of a region-based system. Second, because region operations are constant-time and do not trace the structure of the heap, programs do not suffer from the pauses that are associated with conventional garbage collectors. Consequently, region-based memory management systems may be a practical alternative to real-time garbage collectors [3, 53].

The second advantage gives programmers greater control over memory use. By using a regionprofiler [5], programmers can quickly identify the memory regions that are causing performance problems in their applications. Next, because allocation and deallocation operations are explicit in the program text, programmers can use the profiling data to accurately relate the run-time behaviour of programs to their static representation. In other words, given information about the ways regions are used at run time, it is often straight-forward to examine program code, identify memory-intensive routines, and reason about the lifetimes of the data structures allocated there. Once the trouble spots have been identified, programmers can concentrate their optimization efforts on a small portion of the code. Most importantly, throughout the programming process, a type checker guarantees that all memory operations are safe so programmers do not have to worry about programs crashing due to memory faults.

In order to ensure that regions are used safely, the Tofte-Talpin language includes a lexically-scoped expression (letregion r in e end) that delimits the lifetime of a region r. A region is allocated when control enters the scope of the letregion construct and is deallocated when control leaves the scope. Programs may allocate values into live regions using the notation v at r. These values may be used until the region is deallocated. For example,

⋮

      Region lifetime \{ \begin{matrix}letregion r in & % Allocate region r \\ let x = v at r in & % Allocate value v in region r \\ f (x) \\ end & % Deallocate region r (and v) \end{matrix}

⋮

Tofte and Talpin ensure that deallocated values are not accessed unsafely using a type and effects system. Informally, whenever an expression uses a value in region r, the type system expresses this fact using the effect access(r). However, effects occuring within the scope of the letregion construct are masked. More specifically, if the expression e has effects access(r) ∪ ψ (for some set of effects ψ) then the overall effect of the expression letregion r in e end is simply ψ. Hence, if there is no overall effect for an entire program then every region access must have occured within the scope of the corresponding letregion construct. In other words, values in region r are used only during the lifetime of r and not before or after. If this condition holds, we can conclude the program is safe.

The Tofte-Talpin language makes efficient use of memory provided that the lifetimes of values coincide with the lexical structure of the program. However, if lifetimes deviate from program structure then this style of region-based memory management may force programs to use considerably more memory than necessary. Consider the following program fragments.

             % Scope 1:  The Call Site
             let x = v at r in

⋮

             let y = f (x) in

⋮

             y is dead

                                                 % Scope 2:  The Function
                                                 fun f (x) =

⋮

                                                    x is dead

⋮

                                                    let y = v′ at r′ in

⋮

                                                    return y

The value v is an argument to the function f and must be allocated in the scope of the function call. However, when f is executed, v dies quickly. The value v′ exhibits the inverse behaviour. It is allocated inside f but is returned as the function result. Both v and v′ have lifetimes that span two lexical scopes, but neither is live for very long in either scope. Consequently, vanilla region inference does not perform well in this setting. The best it can do is wrap the function call in a pair of letregion commands.

% Scope 1:  The Call Site
letregion r in
let x = v at r in

⋮

letregion r′ in
let y = f (x) in

⋮

y is dead
end (r′)
end (r)

⋮

% Scope 2:  The Function
fun f (x) =

⋮

x is dead

⋮

let y = v′ at r′ in

⋮

return y

Here, the regions r and r′ are live much longer than they need to be due to the inflexibility of the letregion construct. Both regions must be allocated and outside the function call. Notice also that even though v is dead when the function call returns, the outer region r cannot be deallocated until after the inner region r′ has been deallocated. Lexical scoping enforces a stack-like, last-allocated/first-deallocated memory management discipline.

In this example, a much better solution to this memory management problem is to separate region allocation (newregion) from deallocation (freeregion). The following program takes this approach. In principle, since the lifetimes of regions r and r′ do not overlap, the memory for these regions could be reused.

% Scope 1:  The Call Site
let newregion r in
let x = v at r in

⋮

let y = f (x) in

⋮

y is dead
let freeregion r′ in

⋮

% Scope 2:  The Function
fun f (x) =

⋮

x is dead
let freeregion r in

⋮

let newregion r′ in
let y = v′ at r′ in

⋮

return y

Unfortunately, we cannot write this program in the Tofte-Talpin language because it is based on the idea of lexical scoping. Another consequence of this language design is that any program transformation that alters program structure can affect memory management. One of the most devastating transformations for the Tofte-Talpin type system is the continuation-passing style (CPS) transformation; each successive computation is placed in the scope of all previous computations, with the result that no regions can be deallocated until the entire computation has been completed. In the following example, the CPS transformation prevents the region r from being deallocated until after code has been executed when it could be deallocated as soon as f has completed its computation.

                       letregion r in
                           f (v)
                       end;
                       code

⇒

                                             letregion r in
                                                 f (v, λ.code)
                                             end

The observation that the Tofte-Talpin type system will make poor use of memory in such cases has been made before. Both Birkedal et al. [6] and Aiken et al. [1] have proposed optimizations that allow regions to be freed early. However, although their optimizations are safe, there is no simple proof- or type-checker that an untrusting client can use to check the output code. Therefore, in order to construct a verifyably safe, efficient region-based language, we must re-examine the fundamental question: “When can a program access a value v?”

1.2 Contributions

Our solution to the problem of provably safe yet efficient region-based memory management takes its inspiration from operating systems such as Hydra [55]. Hydra solves the access control problem by associating an unforgeable key or capability with every object and requiring that the user present this capability to gain access to the object. Furthermore, when the need arises, Hydra revokes capabilities, thereby preventing future access to the protected objects.

We define a new strongly-typed compiler intermediate language for region-based memory management that uses a compile-time notion of capability to ensure that region operations are performed safely. Unlike Tofte and Talpin’s language, lexical scoping plays no part in the verification process. Instead, the type system threads static information in the form of capabilities along the control-flow path of a program. In order to use a value in region r at a particular control-flow point, the program must present the capability for that region. As in traditional capability systems, our type system keeps track of capability copies carefully so that it can determine when a capability has truly been revoked. Unlike traditional capability systems, our calculus supports only voluntary revocation. However, the capabilities in our calculus are a purely static concept and thus their implementation requires no run-time overhead. This mechanism provides an efficient way to check the safety of explicit, arbitrarily ordered region allocation and deallocation instructions.

We have a purely syntactic argument, based on Subject Reduction and Progress lemmas in the style of Felleisen and Wright [54], that the type system of the Capability Calculus is sound. In contrast, Tofte and Talpin formulate the soundness of their system using a more complicated greatest fixed point argument [48], and the soundness of Aiken et al.’s optimizations [1] depend upon this argument. Part of the reason for the extra complexity is that Tofte and Talpin simultaneously show that region inference translates lambda calculus terms into operationally equivalent region calculus terms, a stronger property than we prove. However, when system security is the main concern, soundness is the critical property.

The simplicity of our argument demonstrates the benefits of separating type soundness from type inference or optimization correctness.

We also have a formal translation of a variant of the Tofte-Talpin language into our calculus. Given a type-safe Tofte-Talpin program, the translation always produces a type-safe Capability Calculus program. Therefore, when the translation is combined with a region inference algorithm [46], it provides a way to compile source language programs into type-safe low-level code that can be used in secure extensible systems or mobile code.

The remaining sections of this article describe the Capability Calculus in greater detail. Section 2 presents the syntax and semantics of the language formally and motivates the design decisions that we made. At the end of this section, we present the type soundness theorem and discuss the most interesting parts of our proof. The complete proof may be found in Appendix A. Section 3 demonstrates that the Capability Calculus is at least as expressive as the Tofte-Talpin language. We define the semantics of a variant of the latter language and give a translation into the Capability Calculus. The translation preserves the type safety property and Appendix B proves this fact. We further demonstrate the expressiveness of the Capability Calculus by sketching a couple of optimizations that are not possible in the more restrictive language. Section 4 describes how to compile the relatively high-level Capability Calculus into a capability-based Typed Assembly Language. Most elements of this translation are orthogonal to the capability mechanism and therefore this section is mostly informal, although the capability-based Typed Assembly Language has been fully defined. We claim without proof that this target language is type-safe. We believe we could prove a type safety result, but the proof would be long and tedious and we doubt it would reveal any new insights. Finally, we believe that our notion of static capability is generally useful concept. Section 5 informally explores several other applications of capabilities. This section also explains further connections with related work. Finally, Section 6 concludes.

2 The Capability Calculus

The central technical contribution of this article is the Capability Calculus, a statically-typed intermediate language that supports the explicit allocation, freeing and accessing of memory regions.

As mentioned in the introduction, the type system for the language propagates static information (capabilities) along the control-flow path of a program. Therefore, the most elegant and natural form for the language is continuation-passing style (CPS) [40]. That is, functions in the Capability Calculus do not return values; instead, functions finish by calling a continuation function that is typically provided as an argument. The fact that there is only one means of transferring control in CPS—rather than the two means (call and return) in direct style—simplifies the tracking of capabilities. A direct style formulation is possible, but the complications involved obscure the central issues. In the remainder of this paper, we assume familiarity with CPS.

The syntax of the Capability Calculus appears in Figure 1. In the following sections, we explain and motivate the main constructs and typing rules of the language one by one.

kinds  κ ::= Type | Rgn | Cap
constructor vars  α, ρ, ϵ
constructors  c ::= α | τ | r | C
types  τ ::= α | int | r handle | ∀[Δ].(C, τ_{1}, …, τ_{n}) → 0at r | ⟨τ_{1}, …, τ_{n}⟩ at r
regions  r ::= ρ | ν
capabilities  C ::= ϵ | ∅ | \{r^{φ}\} | C_{1} ⊕ C_{2} | \overline{C}
multiplicities  φ ::= 1 | +
constructor contexts  Δ ::= · | Δ, α:κ | Δ, ϵ ≤ C
value contexts  Γ ::= · | Γ, x:τ
region types  Υ ::= {ℓ_{1} : τ_{1}, …, ℓ_{n} : τ_{n}}
memory types  Ψ ::= {ν_{1} : Υ_{1}, …, ν_{n} : Υ_{n}}
word values  v ::= x | i | ν.ℓ | handle(ν) | v[c]
heap values  h ::= fix f[Δ](C, x_{1}:τ_{1}, …, x_{n}:τ_{n}).e | ⟨v_{1}, …, v_{n}⟩
arithmetic ops  p ::= + | − | ×
declarations  d ::= x = v | x = v_{1} p v_{2} | x = h at v | x = π_{i}v | newrgn ρ, x | freergn v
terms  e ::= let d in e | if0 v then e_{2} else e_{3} | v(v_{1}, …, v_{n}) | halt v
memory regions  R ::= {ℓ_{1} ↦ h_{1}, …, ℓ_{n} ↦ h_{n}}
memories  M ::= {ν_{1} ↦ R_{1}, …, ν_{n} ↦ R_{n}}
machine states  P ::= (M, e)

Figure 1: Capability Syntax

2.1 Preliminaries

We specify the operational behavior of the Capability Calculus using an allocation semantics [30, 31, 33], which makes the allocation of data in memory explicit. The semantics, which is specified in Figure 2, is given by a deterministic rewriting system P ⟼ P′ mapping machine states to new machine states. A machine state consists of a pair (M, e) of a memory and a term being executed. A memory is a finite mapping of region names (ν) to regions where a region is a block of memory that holds a collection of heap-allocated objects. Regions are created at run time by the declaration newrgn ρ, x, which allocates a new region in the heap, binds ρ to the name of that region, and binds x to the handle (handle(ν)) for that region.

Region names and handles are distinguished in order to maintain a phase distinction between compile-time and run-time expressions. Region names are significant at compile time: The type-checker identifies which region an object inhabits via a region name (see below). However, region names, like other type constructors, have no run-time significance and may be erased from executable code. In contrast, region handles hold the run-time data necessary to manipulate regions. In addition to accounting for a phase distinction, the separation of region names and handles also allows us to refine the contexts in which region handles are needed. Handles are needed when allocating objects within a region and when freeing a region, but are not needed when reading data from a region.

Regions are freed by the declaration freergn v, where v is the handle for the region to be freed. Objects h large enough to require heap allocation (i.e., functions and tuples), called heap values, are allocated by the declaration x = hatv, where v is the handle for the region in which h is to be allocated. Data is read from a region in two ways: functions are read by a function call, and tuples are read by the declaration x = π_{i}(v), which binds x to the data residing in the ith field of the object at address v. Each of these operations may be performed only when the region in question has not already been freed. Enforcing this restriction is the purpose of the capability mechanism discussed in Section 2.2.

A region maps locations (ℓ) to heap values. Thus, an address is given by a pair ν.ℓ of a region name and a location. In the course of execution, word-sized values (v) will be substituted for value variables and type constructors for constructor variables, but heap values (h) are always allocated in memory and referred to indirectly by an address. Thus, when executing the declaration x = h at r (where r is handle(ν), the handle for region ν), h is allocated in region ν (say at ℓ) and the address ν.ℓ is substituted for x in the following code.

A term in the Capability Calculus consists of a series of declarations ending in either a branch or a function call (or a halt). The class of declarations includes those constructs discussed above, plus two standard constructs, x = v for binding variables to values and x = v_{1} p v_{2} (where p ranges over +, − and ×) for arithmetic.

Types The types of the Capability Calculus include type constructor variables and integers, a type of region handles, as well as tuple and function types. If r is a region, then r handle is the type of r’s region handle. The tuple type ⟨τ_{1}, …, τ_{n}⟩ at r contains the usual n field tuples, but also specifies that such tuples are allocated in region r, where r is either a region name ν or, more frequently, a region variable ρ.

The function type ∀[ ].(C, τ_{1}, …, τ_{n}) → 0at r contains functions taking n arguments (with types τ_{1} through τ_{n}) that may be called when capability C is satisfied (see the next section). The 0 return type is intended to suggest the fact that CPS functions invoke their continuations rather than returning as

(M, e) ⟼ P
If e = then P =
let x = v in e′  (M, e′[v/x])
let x = i p j in e′  (M, e′[(i p j)/x])
let x = h at (handle(ν)) in e′  (M{ν.ℓ ↦ h}, e′[ν.ℓ/x])
and ν ∈ Dom(M)  where ℓ ∉ Dom(M(ν))
let x = π_{i}(ν.ℓ) in e′  (M, e′[v_{i}/x])
and ν ∈ Dom(M) and ℓ ∈ Dom(M(ν)) where M(ν.ℓ) = ⟨v_{0}, …, v_{n−1}⟩ (0 ≤ i < n)
letnewrgn ρ, x in e′  (M{ν ↦ {}}, e′[ν, handle(ν)/ρ, x])
where ν ∉ M and ν ∉ e′

letfreergn (handle(ν)) in e′  (M\ν, e′)

and ν ∈ Dom(M)

if0 0 then e_{2} else e_{3}  (M, e_{2})
if0 i then e_{2} else e_{3}  (M, e_{3})

and i ≠ 0

v(v_{1}, …, v_{n})  (M, e[c_{1}, …, c_{m}, ν.ℓ, v_{1}, …, v_{n}/α_{1}, …, α_{m}, f, x_{1}, …, x_{n}])
where v = ν.ℓ[c_{1}, …, c_{m}]
and M(ν.ℓ) = fix f[Δ](C, x_{1}:τ_{1}, …, x_{n}:τ_{n}).e
and Dom(Δ) = α_{1}, …, α_{m}

Figure 2: Capability Operational Semantics a direct-style function does. The suffix “at r”, like the corresponding suffix for tuple types, indicates the region in which the function is allocated.

Functions may be made polymorphic over types, regions or capabilities by adding a constructor context Δ to the function type. For convenience, types, regions and capabilities are combined into a single syntactic class of “constructors” and are distinguished by kinds. Thus, a type is a constructor with kind Type, a region is a constructor with kind Rgn, and a capability is a constructor with kind Cap. We use the metavariable c to range over constructors, but use the metavariables τ, r and C when those constructors are types, regions and capabilities, respectively. We also use the metavariables ρ and ϵ for constructor variables of kind Rgn and Cap, and use the metavariable α for type variables and generic constructor variables. When Δ is empty, we abbreviate the function type ∀[Δ].(C, τ⃗) → 0at r by (C, τ⃗) → 0at r.

For example, a polymorphic identity function that is allocated in region r, but whose continuation function may be in any region, may be given type

∀[α:Type, ρ:Rgn].(C, α, (C, α) → 0at ρ) → 0at r

for some appropriate C. Let f be such a function, let v be its argument with type τ, and let g be its continuation with type (C, τ) → 0at r. Then f is called by f[τ][r](v, g).

Figure 3 specifies all well-formed constructors and constructor contexts. The two main judgments Δ ⊢ Δ′ and Δ ⊢ c : κ assume that the constructor context Δ is well-formed. The first judgement states that Δ′ is a well-formed constructor context and the second judgement states c is a well-formed constructor with kind κ.

The typing rules also use region types (Υ), which assign a type to every location allocated in a region, and memory types (Ψ), which assign a region type to every region allocated in memory. However, it is not necessary to understand these constructs in the preliminary development, and therefore we will defer discussing them until we describe the static semantics of the abstract machine in formal detail (see Section 2.4).

2.2 Capabilities

The central problem is how to ensure statically that no region is used after it is freed. The typing rules enforce this with a system of capabilities that specify what operations are permitted. The main typing judgement is

Ψ; Δ; Γ; C ⊢ e

which states that (when memory has type Ψ, free constructor variables have kinds given by Δ and free value variables have types given by Γ) it is legal to execute the term e, provided that the capability C is held. A related typing judgement is

Ψ; Δ; Γ; C ⊢ d ⇒ Δ′; Γ′; C′

which states that if the capability C is held, it is legal to execute the declaration d, which results in new constructor context Δ′, new value context Γ′ and new capability C′.

Capabilities indicate the set of regions that are presently valid to access, that is, those regions that have not been freed. Capabilities are formed by joining together a collection of singleton capabilities {r}

Δ ⊢ Δ′

Δ ⊢ · (ctxt-empty)  {Δ ⊢ Δ′ \atop Δ ⊢ Δ′, α:κ} (α ∉ Dom(ΔΔ′)) (ctxt-var)
Δ ⊢ Δ′ ΔΔ′ ⊢ C : Cap
Δ ⊢ Δ′, ϵ ≤ C

(ϵ ∉ Dom(ΔΔ′)) (ctxt-sub)

Δ ⊢ c : κ

Δ ⊢ α : κ (Δ(α) = κ) (type-var)  Δ ⊢ ϵ : Cap ((ϵ ≤ C) ∈ Δ) (type-sub)
Δ ⊢ int : Type (type-int) Δ ⊢ r : Rgn Δ ⊢ r handle : Type (type-handle)
Δ ⊢ τ_{i} : Type (for 1 ≤ i ≤ n) Δ ⊢ r : Rgn
Δ ⊢ ⟨τ_{1}, …, τ_{n}⟩ at r : Type

(type-tuple)

Δ ⊢ Δ′ ΔΔ′ ⊢ τ_{i} : Type (for 1 ≤ i ≤ n)

ΔΔ′ ⊢ C : Cap Δ ⊢ r : Rgn
Δ ⊢ ∀[Δ′].(C, τ_{1}, …, τ_{n}) → 0at r : Type

(type-arrow)

Δ ⊢ ν : Rgn (type-name)  Δ ⊢ ∅ : Cap (type-∅)  Δ ⊢ r : Rgn Δ ⊢ {r^{φ}} : Cap (type-single)
Δ ⊢ C_{1} : Cap Δ ⊢ C_{2} : Cap Δ ⊢ C_{1} ⊕ C_{2} : Cap (type-plus)  Δ ⊢ C : Cap ; Δ ⊢ \overline{C} : Cap (type-bar)

Figure 3: Capability Static Semantics: Type and Context Formation that provide access to only one region, and capability variables ϵ that provide access to an unspecified set of regions. Capability joins, written C_{1} ⊕ C_{2}, are associative and commutative, but are not always idempotent; in Section 2.3 we will see examples where C ⊕ C is not equivalent to C. The empty capability, which provides access to no regions, is denoted by ∅. We will often abbreviate the capability {r_{1}} ⊕ ⋯ ⊕ {r_{n}} by {r_{1}, …, r_{n}}.

In order to read a field from a tuple in region r, it is necessary to hold the capability to access r, as in the rule:

Δ ⊢ C = C′ ⊕ {r} : Cap
Ψ; Δ; Γ ⊢ v : ⟨τ_{1}, …, τ_{n}⟩ at r
Ψ; Δ; Γ; C ⊢ x = π_{i}(v) ⇒ Δ; Γ{x:τ_{i}}; C

(x ∉ Dom(Γ))

The first subgoal indicates that the capability held (C) is equivalent to some capability that includes {r}.

A similar rule is used to allocate an object in a region. Since the type of a heap value reflects the region in which it is allocated, the heap value typing judgement (the second subgoal below) must be provided with that region.

Δ ⊢ C = C′ ⊕ {r} : Cap Ψ; Δ; Γ ⊢ h at r : τ Ψ; Δ; Γ ⊢ v : r handle Ψ; Δ; Γ; C ⊢ x = h at v ⇒ Δ; Γ{x:τ}; C

(x ∉ Dom(Γ))

Functions Functions are defined by the form fix f[Δ](C, x_{1}:τ_{1}, …, x_{n}:τ_{n}).e, where f stands for the function itself and may appear free in the body, Δ specifies the function’s constructor arguments, and C is the function’s capability precondition. When Δ is empty and f does not appear free in the function body we abbreviate the fix form by λ(C, x_{1}:τ_{1}, …, x_{n}:τ_{n}).e.

In order to call a function residing in region r, it is again necessary to hold the capability to access r, and also to hold a capability equivalent to the function’s capability precondition:

Δ ⊢ C = C′′ ⊕ {r} : Cap Δ ⊢ C = C′ : Cap
Ψ; Δ; Γ ⊢ v : (C′, τ_{1}, …, τ_{n}) → 0at r
Ψ; Δ; Γ ⊢ v_{i} : τ_{i}
Ψ; Δ; Γ; C ⊢ v(v_{1}, …, v_{n})

The body of a function may then assume the function’s capability precondition is satisfied, as indicated by the capability C in the premise of the rule:^{1}

Ψ; Δ; Γ{x_{1}:τ_{1}, …, x_{n}:τ_{n}}; C ⊢ e

Ψ; Δ; Γ ⊢ λ(C, x_{1}:τ_{1}, …, x_{n}:τ_{n}).e at r : τ_{f} (x_{i} ∉ Dom(Γ))

As might be expected, the annotation “at r” indicates that the closure value resides in region r. The resultant function type τ_{f} is (C, τ_{1}, …, τ_{n}) → 0at r.

Often, we will extend the required capability for a function with a quantified capability variable (similar to a row variable). This variable may be instantiated with whatever capabilities are leftover after satisfying the required capability. Consequently, the function may be used in a variety of contexts. For example, functions with type

1This rule specializes the full rule for fix to the case where the function is neither polymorphic nor recursive.

∀[ϵ:Cap].({r} ⊕ ϵ, …) → 0at r

may be called with any capability that extends {r}.

Allocation and Deallocation The most delicate issue is the typing of region allocation and deallocation. Intuitively, the typing rules for the newrgn and freergn declarations should add and remove capabilities for the appropriate region. Naive typing rules could be:

Ψ; Δ; Γ; C ⊢ newrgn ρ, x ⇒ Δ{ρ:Rgn}; Γ{x:ρ handle}; C ⊕ {ρ} (wrong)
Ψ; Δ; Γ ⊢ v : r handle C′ = C \ {r}

Ψ; Δ; Γ; C ⊢ freergn v ⇒ Δ; Γ; C′

(wrong)

We will be able to use something much like the first rule for allocation, but the naive rule for freeing regions is fundamentally flawed. For example, consider the following function:

fix f[ρ_{1}:Rgn, ρ_{2}:Rgn]({ρ_{1}, ρ_{2}}, x:ρ_{1} handle, y:⟨int⟩ at ρ_{2}).

                      let freergn x in

let z = π_{0}y in ⋯

This function is well-formed according to the naive typing rule: The function begins with the capability {ρ_{1}, ρ_{2}} and ρ_{1} is removed by the freergn declaration, leaving {ρ_{2}}. The tuple y is allocated in ρ_{2}, so the projection is legal. However, this code is operationally incorrect if ρ_{1} and ρ_{2} are instantiated by the same region r. In that case, the first declaration frees r and the second attempts to read from r.

This problem is a familiar one. To free a region safely it is necessary to delete all copies of the capability. However, instantiating region variables can create aliases, making it impossible to tell by inspection whether any copies exist.

2.3 Alias Control

We desire a system for alias control that can easily be enforced by the type system, without expensive and complex program analyses. One possibility is a linear type system [16, 49, 50]. In a linear type system, aliasing would be trivially controlled; any use of a region name would consume that name, ensuring that it could not be used elsewhere. Thus, in a linear type system, the naive rules for allocating and deallocating regions would be sound. Unfortunately, a linear type system is too restrictive to permit many useful programs. For example, suppose f has type

∀[ρ_{1}:Rgn, ρ_{2}:Rgn].({ρ_{1}, ρ_{2}}, ⟨int⟩ at ρ_{1}, ⟨int⟩ at ρ_{2}, …) → 0at r′

and v_{1} and v_{2} are integer tuples allocated in the same region r. Then f could not be called with v_{1} and v_{2} as arguments, because that would require instantiating ρ_{1} and ρ_{2} with the same region. More generally, one could not type any function that takes two arguments that might or might not be allocated in the same region.

Approaches based on syntactic control of interference [41, 42] are more permissive than a linear type system, but are still too restrictive for our purposes; it is still impossible to instantiate multiple arguments with the same region.

Uniqueness Our approach, instead of trying to prevent aliasing, is to use the type system to track aliasing. More precisely, we track non-aliasing, that is, uniqueness. We do this by tagging regions with one of two multiplicities when forming a capability. The first form, {r^{+}}, is the capability to access region r as it has been understood heretofore. The second form, {r^{1}}, also permits accessing region r, but adds the additional information that r is unique; that is, r represents a different region from any other region appearing in a capability formed using {r^{1}}. For example, the capability {r_{1}^{+}, r_{2}^{1}} not only indicates that it is permissible to access r_{1} and r_{2}, but also indicates that r_{1} and r_{2} represent distinct regions.

Since {r^{1}} guarantees that r does not appear anywhere else in a capability formed using it, it is the capability, not just to access r, but also to free r. Thus we may type region deallocation with the rule:

Δ; Γ ⊢ v : r handle Δ ⊢ C = C′ ⊕ {r^{1}} : Cap

Ψ; Δ; Γ; C ⊢ freergn v ⇒ Δ; Γ; C′

Allocation of a region accordingly adds the new capability as unique:

Ψ; Δ; Γ; C ⊢ newrgn ρ, x ⇒ Δ{ρ:Rgn}; Γ{x:ρ handle}; C ⊕ {ρ^{1}} (ρ ∉ Dom(Δ), x ∉ Dom(Γ))

Note that joining capabilities is only idempotent when the capabilities in question contain no unique multiplicities. For instance, the capabilities {r^{+}} and {r^{+}, r^{+}} are equivalent, but the capabilities {r^{1}} and {r^{1}, r^{1}} are not; the latter capability ({r^{1}, r^{1}}) asserts that r is distinct from itself and consequently that latter capability can never be satisfied.

When C is equivalent to C ⊕ C, we say that C is duplicatable. Note that capability variables are unduplicatable, since they can stand for any capability, including unduplicatable ones. Occasionally this prevents the typing of desired programs, so we provide a stripping operator \overline{C} that replaces all 1 multiplicities in C with + multiplicities. For example, \overline{\{r_{1}^{1}, r_{2}^{+}\}} = \{r_{1}^{+}, r_{2}^{+}\}. For any capability C, the capability \overline{C} is duplicatable. When programs need an unknown but duplicatable capability, they may use a stripped variable \overline{ϵ}. As you will see in section 3, the stripping operator is essential in the translation of Tofte and Talpin’s region-based language into the Capability Calculus.

The complete rules for equivalence of capabilities and other constructors appear in Figure 4. Notice that the single rule eq-flag equates the duplicatable capability \{r^{+}\} with the barred capability \overline{\{r^{1}\}}. Consequently, the form {r^{+}} is redundant given the presence of the bar operator. However, the + notation is a pleasing foil for the 1 notation and the two flags give us a convenient way to distinguish between regions that appear once and regions that potentially appear many times in a single capability.

Subcapabilities The capabilities {r^{1}} and {r^{+}} are not the same, but the former should provide all the privileges of the latter. We therefore say that the former is a subcapability of the latter and write {r^{1}} ≤ {r^{+}}. In the complete system, the various rules from Section 2.2 are modified to account for subcapabilities. For example, the function call rule becomes:

Ψ; Δ; Γ ⊢ v : (C′, τ_{1}, …, τ_{n}) → 0at r
Δ ⊢ C ≤ C′′ ⊕ {r^{+}} Δ ⊢ C ≤ C′
Ψ; Δ; Γ ⊢ v_{i} : τ_{i}
Ψ; Δ; Γ; C ⊢ v(v_{1}, …, v_{n})

Δ ⊢ Δ_{1} = Δ_{2}

Δ ⊢ · = · (ctxt-eq-empty)  {Δ ⊢ Δ_{1} = Δ_{2} \atop Δ ⊢ Δ_{1}, α:κ = Δ_{2}, α:κ} (α ∉ ΔΔ_{1}) (ctxt-eq-kind)
Δ ⊢ Δ_{1} = Δ_{2} ΔΔ_{1} ⊢ C_{1} = C_{2} : Cap
Δ ⊢ Δ_{1}, ϵ ≤ C_{1} = Δ_{2}, ϵ ≤ C_{2}

(ϵ ∉ ΔΔ_{1}) (ctxt-eq-bound)

Δ ⊢ c_{1} = c_{2} : κ

{Δ ⊢ c : κ \atop Δ ⊢ c = c : κ} (eq-reflex)  {Δ ⊢ c_{2} = c_{1} : κ \atop Δ ⊢ c_{1} = c_{2} : κ} (eq-symm)
\begin{matrix}Δ ⊢ c_{1} = c_{2} : κ & Δ ⊢ c_{2} = c_{3} : κ \\ Δ ⊢ c_{1} = c_{3} : κ \end{matrix} (eq-trans)
Δ ⊢ C_{1} = C′_{1} : Cap Δ ⊢ C_{2} = C′_{2} : Cap Δ ⊢ C_{1} ⊕ C_{2} = C′_{1} ⊕ C′_{2} : Cap (eq-congruence-plus) Δ ⊢ C = C′ : Cap Δ ⊢ \overline{C} = \overline{C′} : Cap (eq-congruence-bar)
Δ ⊢ C : Cap Δ ⊢ ∅ ⊕ C = C : Cap (eq-∅)  Δ ⊢ C_{1} : Cap Δ ⊢ C_{2} : Cap Δ ⊢ C_{1} ⊕ C_{2} = C_{2} ⊕ C_{1} : Cap (eq-comm)
Δ ⊢ C_{i} : Cap (for 1 ≤ i ≤ 3) Δ ⊢ (C_{1} ⊕ C_{2}) ⊕ C_{3} = C_{1} ⊕ (C_{2} ⊕ C_{3}) : Cap (eq-assoc)  Δ ⊢ C : Cap Δ ⊢ \overline{C} = \overline{C} ⊕ \overline{C} : Cap (eq-dup)
Δ ⊢ \overline{∅} = ∅ : Cap (eq-bar-∅)  Δ ⊢ r : Rgn Δ ⊢ \overline{\{r^{1}\}} = \{r^{+}\} : Cap (eq-flag)
Δ ⊢ C : Cap Δ ⊢ \overline{\overline{C}} = \overline{C} : Cap (eq-bar-idem)  Δ ⊢ C_{1} : Cap Δ ⊢ C_{2} : Cap Δ ⊢ \overline{C_{1} ⊕ C_{2}} = \overline{C_{1}} ⊕ \overline{C_{2}} : Cap (eq-distrib)

Figure 4: Capability Static Semantics: Equality

Δ ⊢ C_{1} ≤ C_{2}

{Δ ⊢ C_{1} = C_{2} : Cap \atop Δ ⊢ C_{1} ≤ C_{2}} (sub-eq)  \begin{matrix}Δ ⊢ C_{1} ≤ C_{2} & Δ ⊢ C_{2} ≤ C_{3} \\ Δ ⊢ C_{1} ≤ C_{3} \end{matrix} (sub-trans)

\begin{matrix}Δ ⊢ C_{1} ≤ C′_{1} & Δ ⊢ C_{2} ≤ C′_{2} \\ Δ ⊢ C_{1} ⊕ C_{2} ≤ C′_{1} ⊕ C′_{2} \end{matrix} (sub-congruence-plus)  {Δ ⊢ C ≤ C′ \atop Δ ⊢ \overline{C} ≤ \overline{C′}} (sub-congruence-bar)

Δ ⊢ ϵ ≤ C ((ϵ ≤ C) ∈ Δ) (sub-var)  {Δ ⊢ C : Cap \atop Δ ⊢ C ≤ \overline{C}} (sub-bar)

Figure 5: Capability Static Semantics: Equality and Subcapability Relations

Suppose f has type ∀[ρ_{1}:Rgn, ρ_{2}:Rgn].({ρ_{1}^{+}, ρ_{2}^{+}}, …) → 0at r. If we hold capability {r^{+}}, we may call f by instantiating ρ_{1} and ρ_{2} with r, since {r^{+}} = {r^{+}, r^{+}}. Using the subcapability relation, we may also call f when we hold {r^{1}}, again by instantiating ρ_{1} and ρ_{2} with r, since {r^{1}} ≤ {r^{+}} = {r^{+}, r^{+}}.

Figure 5 contains the subcapability rules. When reading these rules, remember that Δ ⊢ \overline{\{r^{1}\}} = {r^{+}} : Cap. We use this fact to derive the judgement Δ ⊢ {r^{1}} ≤ {r^{+}} : Cap that we discussed informally above:

Δ ⊢ \{r^{1}\} ≤ \overline{\{r^{1}\}} : Cap (sub-bar)

Δ ⊢ \overline{\{r^{1}\}} = \{r^{+}\} : Cap (eq-flag)
Δ ⊢ \overline{\{r^{1}\}} ≤ \{r^{+}\} : Cap

(sub-eq)

Δ ⊢ {r^{1}} ≤ {r^{+}} : Cap

(sub-trans)

The subcapability relation accounts only for the forgetting of uniqueness information. Intuitively there could be a second source of subcapabilities, those generated by forgetting an entire capability. For example, {r_{1}^{+}, r_{2}^{+}} seems to provide all the privileges of {r_{1}^{+}}, so it is reasonable to suppose {r_{1}^{+}, r_{2}^{+}} to be subcapability of {r_{1}^{+}}. Indeed, one can construct a sound Capability Calculus incorporating this axiom, but we omit it because doing so allows us to specify memory management obligations and to prove a stronger property about space usage. Notice also, that by omitting this axiom, we do not give up any flexibility; one may always write a function that can be called with extra capabilities by using a capability variable, as discussed in Section 2.2.

By omitting the axiom C_{1} ⊕ C_{2} ≤ C_{1}, our type system may formally specify who has responsibility for freeing a region. Failure to follow informal conventions is a common source of bugs in languages (such as C) that use manual memory management. Our type system rules out such bugs. For example, consider the type:

∀[ρ:Rgn, ϵ:Cap].(ϵ ⊕ {r^{+}, ρ^{1}}, ρ handle, (ϵ ⊕ {r^{+}}) → 0at r) → 0at r

In our system ϵ ⊕ {r^{+}, ρ^{1}} ≰ ϵ ⊕ {r^{+}}. Consequently, before any function with this type can return (i.e., call the continuation of type (ϵ ⊕ {r^{+}}) → 0 at r), it must take action to satisfy the capability ϵ ⊕ {r^{+}}, that is, it must free ρ.

In general, our type system prevents “region leaks”: Programs must deallocate all memory regions before they terminate (Theorem 2.5). Therefore, the operating system does not have to clean up after a program halts. The typing rule for halt states that no capabilities may be held, and since capabilities may not be forgotten, this means that all regions must have been freed.

Ψ; Δ; Γ ⊢ v : int Δ ⊢ C = ∅ : Cap
Ψ; Δ; Γ; C ⊢ halt v

Bounded Quantification The system presented to this point is sound, but it is not yet sufficient for compiling real source languages. We need to be able to recover uniqueness after a region name is duplicated. To see why, suppose we hold the capability {r^{1}} and f has type:

∀[ρ_{1}:Rgn, ρ_{2}:Rgn].({ρ_{1}^{+}, ρ_{2}^{+}}, …, ({ρ_{1}^{+}, ρ_{2}^{+}}, …) → 0at ρ_{1}) → 0at r

We would like to be able to instantiate ρ_{1} and ρ_{2} with r (which we may do, since {r^{1}} ≤ {r^{+}, r^{+}}), and then free r when f calls the continuation in its final argument. Unfortunately, the continuation only possesses the capability {r^{+}, r^{+}} = {r^{+}}, not the capability {r^{1}} necessary to free r. It does not help to strengthen the capability of the continuation to (for example) {ρ_{1}^{1}}, because then f may not call it.

We may recover uniqueness information by quantifying a capability variable. Suppose we again hold capability {r^{1}} and g has type:

∀[ρ_{1}:Rgn, ρ_{2}:Rgn, ϵ:Cap].(ϵ, …, (ϵ, …) → 0at ρ_{1}) → 0at r

We may instantiate ϵ with {r^{1}} and then the continuation will possess that same capability, allowing it to free r. Unfortunately, the body of function g no longer has the capability to access ρ_{1} and ρ_{2}, since its type draws no connection between them and ϵ.

We solve this problem by using bounded quantification to relate ρ_{1}, ρ_{2} and ϵ. Suppose h has type:

∀[ρ_{1}:Rgn, ρ_{2}:Rgn, ϵ ≤ {ρ_{1}^{+}, ρ_{2}^{+}}].(ϵ, …, (ϵ, …) → 0at ρ_{1}) → 0at r

If we hold capability {r^{1}}, we may call h by instantiating ρ_{1} and ρ_{2} with r and instantiating ϵ with {r^{1}}. This instantiation is permissible because {r^{1}} ≤ {r^{+}, r^{+}}. As with g, the continuation will possess the capability {r^{1}}, allowing it to free r, but the body of h (like that of f) will have the capability to access ρ_{1} and ρ_{2}, since ϵ ≤ {ρ_{1}^{+}, ρ_{2}^{+}}.

Bounded quantification solves the problem by revealing some information about a capability ϵ, while still requiring the function to be parametric over ϵ. Hence, when the function calls its continuation we regain the stronger capability (to free r), although that capability was temporarily hidden in order to duplicate r. More generally, bounded quantification allows us to hide some privileges when calling a function, and regain those privileges in its continuation. Thus, we support statically checkable attenuation and amplification of capabilities.

Static Semantics So Far The combination of parametric polymorphism, bounded parametric polymorphism, and notions of uniqueness and aliasing provide a flexible language for expressing the lifetimes of regions. Figures 7 and 6 formally summarize the rules for type checking instructions and values that depend upon these concepts. We have already explained the majority of these rules in previous sections and the rules that we have not yet specified are the obvious ones (integers are given type int, etc.). Notice, however, that the form of the judgement for heap values h is slightly different from the judgements for instructions and small values v. The judgment Ψ; Δ; Γ ⊢ h at r : τ states that when memory has type Ψ, free constructor variables have kinds given by Δ and free value variables have types given by Γ, the heap value h resides in region r and has type τ.

2.4 The Static Semantics of the Abstract Machine

We have described the type constructor language of the Capability Calculus and the typing rules for the main term-level constructs. In fact, the previous section contains all of the information programmers or compilers require to write type-safe programs in the Capability Calculus. However, in order to prove a type soundness result in the style of Wright and Felleisen [54], we must be able to type check programs at every step during their evaluation. In this section, we give the static semantics of the run-time values that are not normally manipulated by programmers, but are nevertheless necessary to prove our soundness result.

At first, the formal definition of the semantics may appear quite complex because we use a number of different judgment forms. However, most of these forms follow naturally from the development of previous sections and other work on type systems for allocation semantics [30, 31, 33]. The extra complexity in the definition of the language will pay off when we come to prove type soundness: All of the main invariants are expressed directly in the typing rules and therefore most of the proof follows from straightforward inductions over these rules.

Figure 8 specifies the rules for typing memory, most of which are straightforward. The judgments ⊢ Ψ and ⊢ Υ specify when memory types and region types are well-formed. This is the case whenever their subcomponents are well-formed. The judgment ⊢ M : Ψ states that memory M is described by Ψ and the judgement Ψ ⊢ R at ν : Υ states that region R with name ν is described by Υ. Informally, these judgements ensure that for addresses ν.ℓ, Ψ(ν.ℓ) is type τ if and only if the memory M described by Ψ contains a value v at address ν.ℓ that has type τ.

The next judgment, Ψ ⊢ C sat is called the satisfiability judgment and it formalizes the connection between the static capability and the run-time state of memory. Clearly, the current capability must not contain any regions that are not in memory; this could lead to a runtime error. However, it is equally important that memory not contain regions for which we have no capability; these regions can never be freed. Consequently, satisfiability ensures that at any time during execution of the abstract machine, our capability contains exactly the regions in memory. Furthermore, by virtue of the fact that · ⊢ {r^{1}} ≠ {r^{1}, r^{1}} : Cap, no unique regions may appear more than once in C. Each of these properties are essential to ensure that regions are used safely.

Figure 9 contains rules for small values that only appear at run time (addresses and region handles). The rules for typing an address ν.ℓ are quite unusual, but crucial to the type soundness proof. The first rule, v-addr, is used during the lifetime of the region ν: If the region ν is in memory then ν will also be in the domain of the memory type Ψ. Therefore, rule v-addr applies and ν.ℓ will have type Ψ(ν.ℓ). Now consider some point in the computation after the region ν has been deallocated. The region ν is no longer in the memory, but the addresses ν.ℓ may still appear embedded in tuples or closures allocated in other regions, and, therefore, it must be given a type. If a region ν does not appear in memory type

Ψ; Δ; Γ ⊢ h at r : τ

\begin{matrix}Δ ⊢ τ_{f} \\ Ψ; ΔΔ′; Γ\{f:τ_{f}, x_{1}:τ_{1}, …, x_{n}:τ_{n}\}; C ⊢ e \end{matrix}

Ψ; Δ; Γ ⊢ fix f[Δ′](C, x_{1}:τ_{1}, …, x_{n}:τ_{n}).e at r : τ_{f} (\begin{matrix}τ_{f} = ∀[Δ′].(C, τ_{1}, …, τ_{n}) → 0at r \\ f, x_{1}, …, x_{n} ∉ Dom(Γ) \end{matrix}) (h-fix)

Ψ; Δ; Γ ⊢ v_{i} : τ_{i} (for 1 ≤ i ≤ n) Δ ⊢ r : Rgn

Ψ; Δ; Γ ⊢ ⟨v_{1}, …, v_{n}⟩ at r : ⟨τ_{1}, …, τ_{n}⟩ at r (h-tuple)

Ψ; Δ; Γ ⊢ h at r : τ′ Δ ⊢ τ′ = τ : Type
Ψ; Δ; Γ ⊢ h at r : τ

(h-eq)

Ψ; Δ; Γ ⊢ v : τ

Ψ; Δ; Γ ⊢ x : τ (Γ(x) = τ) (v-var)
Ψ; Δ; Γ ⊢ i : int (v-int)

Ψ; Δ; Γ ⊢ v : ∀[α:κ, Δ′].(C, τ_{1}, …, τ_{n}) → 0at r Δ ⊢ c : κ Ψ; Δ; Γ ⊢ v[c] : (∀[Δ′].(C, τ_{1}, …, τ_{n}) → 0)[c/α] at r

(v-type)

Ψ; Δ; Γ ⊢ v : ∀[ϵ ≤ C′′, Δ′].(C′, τ_{1}, …, τ_{n}) → 0at r Δ ⊢ C ≤ C′′ Ψ; Δ; Γ ⊢ v[C] : (∀[Δ′].(C′, τ_{1}, …, τ_{n}) → 0)[C/ϵ] at r

(v-sub)

Ψ; Δ; Γ ⊢ v : τ′ Δ ⊢ τ′ = τ : Type

Ψ; Δ; Γ ⊢ v : τ (v-eq)

Figure 6: Capability Static Semantics: Heap and Word Values

Ψ; Δ; Γ; C ⊢ d ⇒ Δ′; Γ′; C′

Ψ; Δ; Γ ⊢ v : τ

Ψ; Δ; Γ; C ⊢ x = v ⇒ Δ; Γ{x:τ}; C

(x ∉ Dom(Γ)) (val)

Ψ; Δ; Γ ⊢ v_{1} : int Ψ; Δ; Γ ⊢ v_{2} : int

Ψ; Δ; Γ; C ⊢ x = v_{1} p v_{2} ⇒ Δ; Γ{x:int}; C

(x ∉ Dom(Γ)) (prim)

Ψ; Δ; Γ ⊢ v : r handle Ψ; Δ; Γ ⊢ h at r : τ Δ ⊢ C ≤ C′ ⊕ {r^{+}} Ψ; Δ; Γ; C ⊢ x = h at v ⇒ Δ; Γ{x:τ}; C

(x ∉ Dom(Γ)) (hval)

Ψ; Δ; Γ ⊢ v : ⟨τ_{0}, …, τ_{n−1}⟩ at r Δ ⊢ C ≤ C′ ⊕ {r^{+}} Ψ; Δ; Γ; C ⊢ x = π_{i}v ⇒ Δ; Γ{x:τ_{i}}; C

(x ∉ Dom(Γ) ∧ 0 ≤ i < n) (proj)
Ψ; Δ; Γ; C ⊢ newrgn ρ, x ⇒ Δ\{ρ:Rgn\}; Γ\{x:ρ handle\}; C ⊕ \{ρ^{1}\} (\begin{matrix}ρ ∉ Dom(Δ) \\ x ∉ Dom(Γ) \end{matrix}) (newrgn)
Ψ; Δ; Γ ⊢ v : r handle Δ ⊢ C = C′ ⊕ {r^{1}} : Cap

Ψ; Δ; Γ; C ⊢ freergn v ⇒ Δ; Γ; C′

(freergn)

Ψ; Δ; Γ; C ⊢ e

Ψ; Δ; Γ; C ⊢ d ⇒ Δ′; Γ′; C′  Ψ; Δ′; Γ′; C′ ⊢ e Ψ; Δ; Γ; C ⊢ let d in e (letdec)  Ψ; Δ; Γ ⊢ v : int Ψ; Δ; Γ; C ⊢ e_{2}  Ψ; Δ; Γ; C ⊢ e_{3} Ψ; Δ; Γ; C ⊢ if0 v then e_{2} else e_{3} (if)
Ψ; Δ; Γ ⊢ v : ∀[ ].(C′, τ_{1}, …, τ_{n}) → 0at r Ψ; Δ; Γ ⊢ v_{i} : τ_{i} (for 1 ≤ i ≤ n) Δ ⊢ C ≤ C′′ ⊕ {r^{+}}  Δ ⊢ C ≤ C′ Ψ; Δ; Γ; C ⊢ v(v_{1}, …, v_{n}) (app)  Ψ; Δ; Γ ⊢ v : int Δ ⊢ C = ∅ : Cap Ψ; Δ; Γ; C ⊢ halt v (halt)

Figure 7: Capability Static Semantics: Declarations and Expressions

⊢ Υ ⊢ Ψ

{· ⊢ τ_{i}  (for 1 ≤ i ≤ n) \atop ⊢ \{ℓ_{1}:τ_{1}, …, ℓ_{n}:τ_{n}\}} (region-type)

{⊢ Υ_{i}  (for i ≤ i ≤ n) \atop ⊢ \{ν_{1}:Υ_{1}, …, ν_{n}:Υ_{n}\}} (memory-type)

Ψ ⊢ R at ν : Υ ⊢ M : Ψ

Ψ; ·; · ⊢ h_{i} at ν : τ_{i} (for 1 ≤ i ≤ n)

Ψ ⊢ {ℓ_{1} ↦ h_{1}, …, ℓ_{n} ↦ h_{n}} at ν : {ℓ_{1} : τ_{1}, …, ℓ_{n} : τ_{n}} (region)

⊢ Ψ Ψ ⊢ R_{i} at ν_{i} : Υ_{i} (for 1 ≤ i ≤ n)

⊢ {ν_{1} ↦ R_{1}, …, ν_{n} ↦ R_{n}} : Ψ (Ψ = {ν_{1} : Υ_{1}, …, ν_{n} : Υ_{n}}) (memory)

Ψ ⊢ C sat

· ⊢ C = {ν_{1}^{φ_{1}}, …, ν_{n}^{φ_{n}}} : Cap

{ν_{1} : Υ_{1}, …, ν_{n} : Υ_{n}} ⊢ C sat (ν_{i} ≠ ν_{j} for 1 ≤ i, j ≤ n and i ≠ j) (sat)

Figure 8: Capability Static Semantics: Memory

Ψ, the type system has the flexibility to give ν.ℓ any function type (by rule v-addr-arrow) or tuple type (by rule v-addr-tuple).

At first glance, these rules would appear to lead to unsoundness: The address ν.ℓ is a dangling pointer and it may be given a valid type. Fortunately, though, capabilities prevent anything from going wrong. The satisfiability judgment ensures that programs only ever possess capabilities for regions that appear in memory, and, as we explained earlier, programs can only access the regions they have capabilities for. Consequently, a dangling pointer may be given a valid tuple or function type, but capabilities prevent it from being accessed.

We now have all components necessary to define a well-formed machine state. The state (M, e) is well-formed if the memory M can be described by a well-formed heap type Ψ, there exists a capability C such that C satisfies the heap type Ψ, and finally, the expression e is well-formed with respect to Ψ and C:

{⊢ M : Ψ  Ψ ⊢ C sat  Ψ; ·; ·; C ⊢ e \atop ⊢ (M, e)} (program)

Ψ; Δ; Γ ⊢ v : τ

Ψ; Δ; Γ ⊢ ν.ℓ : τ (Ψ(ν.ℓ) = τ) (v-addr)

Δ ⊢ ⟨τ_{1}, …, τ_{n}⟩ at ν : Type
Ψ; Δ; Γ ⊢ ν.ℓ : ⟨τ_{1}, …, τ_{n}⟩ at ν

(ν ∉ Dom(Ψ)) (v-addr-tuple)

Δ ⊢ ∀[Δ′].(C, τ_{1}, …, τ_{n}) → 0at ν : Type
Ψ; Δ; Γ ⊢ ν.ℓ : ∀[Δ′].(C, τ_{1}, …, τ_{n}) → 0at ν

(ν ∉ Dom(Ψ)) (v-addr-arrow)

Ψ; Δ; Γ ⊢ handle(ν) : ν handle (v-handle)

Figure 9: Capability Static Semantics: Run-time Values

2.5 Formal Properties of the Calculus

The most important property of the Capability Calculus is Type Soundness. Type Soundness states that a program will never enter a stuck state during execution. A state (M, e) is stuck if there does not exist (M′, e′) such that (M, e) ⟼ (M′, e′) and e is not halt i. For example, a state that tries to project a value from a tuple that does not appear in memory is stuck.

Theorem 1 (Type Soundness) If ⊢ (M, e) and (M, e) ⟼^{∗} (M′, e′) then (M′, e′) is not stuck.

In the previous sections of this article, we have explained how to type memory, how to relate the memory typing to static capabilities and finally, given a collection of capabilities, how the rules for typing expressions prevent unsafe accesses to the store. These invariants are the main elements in the formal proof of soundness. However, there are many details to fill in. The proof is in the style of Wright and Felleisen [54] and uses the standard Type Preservation and Progress lemmas. Progress states that well-typed states are not stuck, and Preservation states that evaluation steps preserve well-typedness.

Lemma 2 (Type Preservation) If ⊢ (M, e) and (M, e) ⟼ (M′, e′) then ⊢ (M′, e′)

Lemma 3 (Progress) If ⊢ (M, e) then either:

1. There exists (M′, e′) such that (M, e) ⟼ (M′, e′), or

2. e = halt i

kinds  κ ::= Type | Rgn | Eff
constructor variables α, β, ρ, ϵ
constructor contexts  Δ ::= · | Δ, α:κ_{1}
type schemes  σ ::= τ | ∀[Δ].τ_{1} →^{ψ} τ_{2} at r
constructors  c, τ, r, ψ ::= α | int | r handle | ⟨τ_{1}, …, τ_{n}⟩ at r | τ_{1} →^{ψ} τ_{2} at r |
∅ | {r} | ψ_{1} ∪ ψ_{2}
term variables  x, f
term contexts  Γ ::= · | Γ, x:σ
terms  e ::= x | i | e_{1} p e_{2} | if0 e_{1} then e_{2} else e_{3} | ⟨e_{1}, …, e_{n}⟩ at e_{n+1} |

π_{i}e | letrecf[Δ](x) : σ at e_{1} = e_{2} in e_{3} | f[c_{1}, …, c_{n}] |

                                   e_{1}e_{2} | letregion ρ, x_{ρ} in e

Figure 10: Region Syntax

Because of the length and tedium of the proofs of these lemmas, we have removed them, along with the proof of soundness itself, to Appendix A.

The second important property of the language is that well-typed terminating programs return all of their memory resources to the system before they halt. We call this property Complete Collection.

Theorem 4 (Complete Collection) If ⊢ (M, e) then either (M, e) diverges or (M, e) ⟼^{∗} ({ }, halt i).

By Subject Reduction and Progress, terminating programs end in well-formed machine states (M, halt i). The typing rule for the halt expression requires that the capability C be empty. Using this fact, we can infer that the memory M contains no regions. Appendix A also contains a formal proof of this theorem.

3 From Regions to Capabilities

The primary goal of this work is the development of a type-safe language that gives compilers control over the allocation and deallocation of data. In order to use this technology effectively, we need compiler support for generating the intermediate language code from source language programs. In this section, we define a high-level explicitly-typed variant of Tofte and Talpin’s region-based language and show that it can be translated into the Capability Calculus. By composing this translation with region inference, we may obtain a type-preserving compiler front-end.

3.1 A Region-Based Calculus

Preliminaries The source language for our compiler is the region-based calculus shown in Figure 10. This language is an explicitly-typed variant of the calculus first presented by Tofte and Talpin [47]. Like the Capability Calculus, it contains integers, tuples and functions. However, unlike the Capability Calculus, allocation and deallocation of regions is combined in a single construct: letregion ρ, x_{ρ} in e. This construct allocates a new region ρ and places the handle for that region in the term variable x_{ρ}. Next, it executes the expression e. Finally, the region ρ is deallocated. As discussed in the introduction, this lexically-scoped construct is not as flexible as the separate newrgn and freergn constructs provided by the Capability Calculus. The main goal of this section is to show how to compile letregion expressions into these lower-level primitives.

As in the original Tofte-Talpin calculus, the region language has prenex predicative polymorphism. The term letrecf[Δ](x) : σ at e_{1} = e_{2} in e_{3} allocates a closure f of polytype σ. The closure is polymorphic over its type context Δ, which may contain ordinary type variables as well as region variables and effect variables (explained below). The closure is allocated in the region r if the expression e_{1} evaluates to a region handle for r. The expression e_{2} describes the body of the function.

Unlike previous work on region-based type systems, we treat all type constructors, including region constructors, as compile-time-only objects. Therefore, the term f[c_{1}, …, c_{n}], which denotes type application, has no runtime effect. During type checking, the type scheme for the polymorphic function f is instantiated with the types c_{1}, …, c_{n} to obtain the resultant type for the expression, but the dynamic semantics of the program (not shown here) do not depend upon these types. Hence, the types may be erased before the program is run without affecting the computation. As in the Capability Calculus, the data structures that are required to allocate and deallocate regions are treated as ordinarly values of type handle(r).

Types and Effects The main interest of the type constructor portion of the region language is the presence of effects. Effects, like capabilities, are used to control a program’s access to regions and, in particular, to prevent access to regions that have been deallocated. Intuitively, the effect of a term is the set of regions that the term accesses. Formally, an effect is either the empty effect (∅), an effect variable (ϵ), a singleton set ({r}), or the union of two effects (ψ_{1} ∪ ψ_{2}). The ∪ operator is associative, commutative, and idempotent and ∅ is the unit for the union operator. We write Δ ⊢_{R} ψ_{1} = ψ_{2} : Eff for equality on effects and we use the abbreviation Δ ⊢_{R} ψ_{1} ⊆ ψ_{2} when Δ ⊢_{R} ψ_{1} ∪ ψ_{3} = ψ_{2} : Eff for some effect ψ_{3}.

All functions have latent effects that are incurred when the function is called and its body is executed. The effect that appears on arrow types (∀[Δ].τ →^{ψ} τ′)^{2} specifies the set of regions that a function of that type may access when it is invoked. The formal rules for type and effect formation and equality may be found in Figure 11.

Static Semantics The static semantics (Figure 12) for terms use a judgement of the form Δ; Γ ⊢_{R} e : τ, ψ to track the effects produced by each expression. This judgement states that under the type context Δ and the value context Γ, a term e has type τ and produces effect ψ. For example, the rule for projection states that if e is an expression producing effect ψ then π_{i}e produces the effect ψ ∪ {r}. The projection operation reads from the region r and the subexpression e may read from or write to any of the regions in ψ. Hence the resulting effect must be the union of the two.

2Tofte and Talpin require each arrow type be annotated with an “arrow effect”, which is constrained to have the form ϵ ∪ ψ. The type variable ϵ is used to name the effect and plays a role in their inference system. Because we are interested in type checking rather than type inference, we do not need to name the effects on arrows.

Δ ⊢ Δ′

Δ ⊢ ·  {Δ ⊢ Δ′ \atop Δ ⊢ Δ′, \{α:κ\}} (α ∉ Dom(Δ))

Δ ⊢ σ

Δ ⊢ τ : Type Δ ⊢ τ

⊢ ΔΔ′ ΔΔ′ ⊢ τ_{i} : Type (for 1 ≤ i ≤ n + 1)

ΔΔ′ ⊢ ψ : Eff Δ ⊢ r : Rgn

Δ ⊢ ∀[Δ′].(τ_{1}, …, τ_{n}) →^{ψ} τ_{n+1} at r

Δ ⊢ c : κ

Δ ⊢ α : κ (Δ(α) = κ)

                      Δ ⊢ int : Type

Δ ⊢ r : Rgn

                                      Δ ⊢ r handle : Type

Δ ⊢ τ_{i} : Type (for 1 ≤ i ≤ n) Δ ⊢ r : Rgn

Δ ⊢ ⟨τ_{1}, …, τ_{n}⟩ at r : Type

Δ ⊢ r : Rgn Δ ⊢ ψ : Eff Δ ⊢ τ_{i} : Type (for 1 ≤ i ≤ n + 1)

Δ ⊢ (τ_{1}, …, τ_{n}) →^{ψ} τ_{n+1} at r : Type

Δ ⊢ ∅ : Eff

Δ ⊢ r : Rgn Δ ⊢ {r} : Eff
Δ ⊢ ψ_{1} : Eff Δ ⊢ ψ_{2} : Eff
Δ ⊢ ψ_{1} ∪ ψ_{2} : Eff

Δ ⊢ σ_{1} = σ_{2} Δ ⊢ c_{1} = c_{2} : κ (congruence rules omitted)

{Δ ⊢ c : κ \atop Δ ⊢ c = c : κ}  {Δ ⊢ c_{2} = c_{1} : κ \atop Δ ⊢ c_{1} = c_{2} : κ}  \begin{matrix}Δ ⊢ c_{1} = c_{2} : κ & Δ ⊢ c_{2} = c_{3} : κ \\ Δ ⊢ c_{1} = c_{3} : κ \end{matrix}
Δ ⊢ ψ : Eff
Δ ⊢ ∅ ∪ ψ = ψ : Eff

Δ ⊢ ψ_{1} : Eff Δ ⊢ ψ_{2} : Eff

Δ ⊢ ψ_{1} ∪ ψ_{2} = ψ_{2} ∪ ψ_{1} : Eff

Δ ⊢ ψ_{i} : Eff (for 1 ≤ i ≤ 3) Δ ⊢ (ψ_{1} ∪ ψ_{2}) ∪ ψ_{3} = ψ_{1} ∪ (ψ_{2} ∪ ψ_{3}) : Eff

Δ ⊢ ψ_{1} : Eff Δ ⊢ ψ_{2} : Eff
Δ ⊢ ψ_{1} ∪ ψ_{2} = ψ_{1} ∪ (ψ_{2} ∪ ψ_{2}) : Eff

{Δ ⊢ ψ_{1} ∪ ψ_{3} = ψ_{2} : Eff \atop Δ ⊢ ψ_{1} ⊆ ψ_{2}}

Figure 11: Region Type Formation, Equality, and Subset

Δ; Γ ⊢_{R} x : τ, ∅ (Γ(x) = τ)  Δ; Γ ⊢_{R} i : int, ∅
Δ; Γ ⊢_{R} e_{1} : int, ψ_{1} Δ; Γ ⊢_{R} e_{2} : int, ψ_{2}
Δ; Γ ⊢_{R} e_{1} p e_{2} : int, ψ_{1} ∪ ψ_{2}
Δ; Γ ⊢_{R} e_{i} : τ_{i}, ψ_{i} (for 1 ≤ i ≤ n) Δ; Γ ⊢_{R} e_{n+1} : r handle, ψ_{n+1}

Δ; Γ ⊢_{R} ⟨e_{1}, …, e_{n}⟩ at e_{n+1} : τ, ψ_{1} ∪ … ∪ ψ_{n+1} ∪ {r}

{Δ; Γ ⊢_{R} e : ⟨τ_{0}, …, τ_{n−1}⟩ at r, ψ \atop Δ; Γ ⊢_{R} π_{i}e : τ_{i}, ψ ∪ \{r\}} (0 ≤ i < n)
Δ; Γ ⊢_{R} e_{1} : int, ψ_{1} Δ; Γ ⊢_{R} e_{2} : τ, ψ_{2} Δ; Γ ⊢_{R} e_{3} : τ, ψ_{3}

Δ; Γ ⊢_{R} if0 e_{1} then e_{2} else e_{3} : τ, ψ_{1} ∪ ψ_{2} ∪ ψ_{3}

Δ ⊢_{R} σ ΔΔ′; Γ{f:σ, x:τ_{1}} ⊢_{R} e_{2} : τ_{2}, ψ Δ; Γ ⊢_{R} e_{1} : r handle, ψ_{1} Δ; Γ{f:σ} ⊢_{R} e_{3} : τ_{3}, ψ_{3}

Δ; Γ ⊢_{R} letrecf[Δ′](x) : σ at e_{1} = e_{2} in e_{3} : τ_{3}, ψ_{1} ∪ ψ_{3} ∪ {r} ( \begin{matrix}x, f ∉ Dom(Γ) \\ σ = ∀[Δ′].τ_{1} →^{ψ} τ_{2} at r \end{matrix} )

Δ ⊢_{R} c_{i} : κ_{i} (for 1 ≤ i ≤ n)

\begin{matrix}Δ; Γ ⊢_{R} f[c_{1}, …, c_{n}] : \\ (τ_{1} →^{ψ} τ_{2})[c_{1}, …, c_{n}/α_{1}, …, α_{n}] at r, ∅ \end{matrix}

(Γ(f) = ∀[α_{1}:κ_{1}, …, α_{n}:κ_{n}].τ_{1} →^{ψ} τ_{2} at r)

Δ; Γ ⊢_{R} e_{1} : τ_{1} →^{ψ} τ_{2} at r, ψ_{1} Δ; Γ ⊢_{R} e_{2} : τ_{1}, ψ_{2}
Δ; Γ ⊢_{R} e_{1}e_{2} : τ_{2}, ψ_{1} ∪ ψ_{2} ∪ ψ ∪ {r}

Δ{ρ:Rgn}; Γ{x_{ρ}:ρ handle} ⊢_{R} e : τ, ψ

Δ; Γ ⊢_{R} letregion ρ, x_{ρ} in e : τ, ψ\{ρ} ( \begin{matrix}ρ ∉ ftv(τ) ∪ Dom(Δ) \\ x_{ρ} ∉ Dom(Γ) \end{matrix} )

Δ; Γ ⊢_{R} e : τ, ψ Δ ⊢_{R} τ = τ′ : Type Δ ⊢_{R} ψ ⊆ ψ′
Δ; Γ ⊢_{R} e : τ′, ψ′

Figure 12: Region Term Static Semantics

The rules involving functions are more complex. First, consider a function call e_{1}e_{2}. Assume that e_{1} generates the effect ψ_{1} and evaluates to a closure of type ∀[ ].(τ) →^{ψ} τ′ at r, and that e_{2} produces the effect ψ_{2} and has type τ. After both expressions have been evaluated, the code for the function is projected from a closure that resides in region r. Now, because the function itself produces the effect ψ, the overall effect of the call is the union of {r} with ψ, ψ_{1}, and ψ_{2}. In contrast to the value application rule, the rule for type application produces no effect; remember, types are erased before an expression is executed. Finally, examine the rule for the letrec term. There are three components to the effect produced by this expression: ψ_{1}, the effect of evaluating handle expression; {r}, the effect of writing the closure data structure in region r; and ψ_{3}, the effect of the subsequent expression e_{3}. As well as checking that types match up properly, we must be sure that the effect produced by the body of the function is a subset of the declared effect. The type system would be unsound if functions could hide their effects.

The last rule checks the letregion construct. Here, we use the notation ψ\{ρ} to denote the effect ψ with all occurences of {ρ} replaced by ∅. This rule discharges the effect {r} from the effect produced by the subexpression e. Intuitively, because the letregion construct discharges effects whereas all other constructs pass on effect information from their subexpressions to their enclosing expressions, any access to a region outside of the scope of a letregion will be detected and the type checker will reject the expression as a whole.

Figure 13 shows an example program, a function count that counts down to zero. In order to have interesting allocation behavior the integers involved in the count are boxed, and hence are allocated in a region. The count function is stored in region ρ_{1} and takes two arguments, a handle for region ρ and a boxed integer x allocated in region ρ. If x is nonzero, count decrements it, storing the result again in ρ, and recurses. The function has two effects: a read on ρ_{1}, resulting from the recursive call, and a read/write effect on ρ, resulting from line 1’s read and line 2’s store. Therefore, we give the function count the effect {ρ_{1}, ρ_{2}}. Overall, the code in Figure 13 allocates two regions (ρ_{1} and ρ_{2}), stores the closure for count in ρ_{1}, stores a boxed integer in ρ_{2}, calls count, and then deallocates ρ_{1} and ρ_{2}.

3.2 The Translation

In order to make a formal connection to region-based calculi and to corroborate our claims that we can use the region inference techniques developped by Tofte and others as a front-end for a capability-based compiler, we have defined a type-directed and type-preserving translation from the region calculus of the previous section to the Capability Calculus. Appendix B contains a proof that any well-formed source term is translated into a well-formed target term.

Kind and Type Translation The translation is a continuation-passing style transformation in which we simultaneously transform effects into capabilities. The kind and type transformation is presented in Figure 14. The kind translation is trivial; effects become capabilities and the other kinds are unchanged. The translation of most types is equally simple. The translation of base types is the identity and, in general, to translate other types we recursively translate their components and recombine using the corresponding capability constructor. Thus, tuples are mapped to tuples and handles are mapped to handles, etc.

letregion ρ_{1}, x_{ρ_{1}} in
  letregion ρ_{2}, x_{ρ_{2}} in
    letrec count [ρ] (x_{ρ} : ρ handle, x : ⟨int⟩ at ρ) at x_{ρ_{1}} : σ_{count} =

      let n = π_{0}(x) in                   % (1)

        if0 n
          then ()
          else count [ρ] (x_{ρ}, ⟨n − 1⟩ at x_{ρ}) % (2)
      end
    in

count [ρ_{2}] (x_{ρ_{2}}, ⟨10⟩ at x_{ρ_{2}})

    end % letrec
  % end region ρ_{2} scope and deallocate
% end region ρ_{1} scope and deallocate

where σ_{count} = ∀[ρ]. (ρ handle, ⟨int⟩ at ρ) ⟶^{{ρ_{1},ρ}}unit

Figure 13: Count in the Region Calculus

                      K[[Type]] = Type
                       K[[Rgn]] = Rgn
                       K[[Eff]] = Cap

K[[α_{1}:κ_{1}, …, α_{n}:κ_{n}]] = α_{1}:K[[κ_{1}]], …, α_{n}:K[[κ_{n}]]
T [[α]] = α

                       T [[int]] = int

T [[⟨τ_{1}, …, τ_{n}⟩ at r]] = ⟨T [[τ_{1}]], …, T [[τ_{n}]]⟩ at T [[r]]
T [[τ_{1} →^{ψ} τ_{2} at r]] = ∀[ρ′:Rgn, ϵ:Cap, ϵ′ ≤ \overline{ϵ ⊕ T [[ψ]] ⊕ \{ρ^{′1}\}}].(ϵ′,

T [[τ_{1}]], ∀[ ].(ϵ′, T [[τ_{2}]]) → 0at ρ′) → 0at T [[r]]

T [[r handle]] = T [[r]] handle
T [[∅]] = ∅
T [[{r}]] = {T [[r]]^{1}}
T [[ψ_{1} ∪ ψ_{2}]] = T [[ψ_{1}]] ⊕ T [[ψ_{2}]]
S[[τ]] = T [[τ]]
S[[∀[Δ].τ_{1} →^{ψ} τ_{2} at r]] = ∀[K[[Δ]]].T [[τ_{1} →^{ψ} τ_{2} at r]]
S[[{x_{1}:σ_{1}, …, x_{n}:σ_{n}}]] = {x_{1}:S[[σ_{1}]], …, x_{n}:S[[σ_{n}]]}

Figure 14: Region to Capability Kind and Type Translation

The translation of function types is more involved. Recall that in the usual CPS-translation, an arrow type (τ_{1}) → τ_{2} is transformed so that it accepts a translated τ_{1} and a τ_{2} continuation:

(T [[τ_{1}]], T [[τ_{2}]] → 0) → 0

The translation of region arrow types has the same structure, but there are several complications that arise as we transform effects into capabilities. The first complication involves finding a region for the continuation closure. We solve this problem by allocating a new region ρ′ to hold the continuation; the translated function abstracts this region. The second complication is that an effect for a function may only mention a subset of the regions that are live at the call site. Nevertheless, the resulting Capability Calculus function must thread the capability describing all the live regions from the context where the function is called through the body of the function to the continuation. We accomplish this task by abstracting an additional capability variable ϵ that makes each function context sensitive. Using this mechanism, we can thread any capability in the calling context through the function to its continuation.

The third complication is that the type translation must ensure that equal types in the region calculus are translated to equal types in the Capability Calculus. For the most part, this obligation is satisfied trivially because the equality relation for most region types and their corresponding Capability Calculus analogues is simple syntactic equality up to α-conversion of bound variables. However, the equality relation for effects is set equality whereas the equality relation for arbitrary capabilities is not set equality (⊕ is not necessarily idempotent). Fortunately, equality of duplicatable capabilities is exactly set equality. Therefore, the type translation carefully translates all arrow effects into duplicatable capabilities.

These three insights naturally lead us to translate a region function type τ_{1} →^{ψ} τ_{2} at r into the Capability Calculus function type

∀[ρ′:Rgn, ϵ:Cap, ϵ′ ≤ \overline{ϵ ⊕ T [[ψ]] ⊕ \{ρ^{′1}\}}].(ϵ′, T [[τ_{1}]], τ_{2} cont at ρ′) → 0at T [[r]]

The capability for the translated function is ϵ′ where ϵ′ is a subtype of \overline{ϵ ⊕ T [[ψ]] ⊕ \{ρ^{′1}\}}. This capability gives the translated function access to all the regions it requires: The regions in T [[ψ]] are the regions accessed by the source language function; ρ′ is the region containing the continuation; and ϵ contains the regions from the calling context that are threaded through the call to the continuation. Notice also that the capability that appears in this type is duplicatable, so we can prove that equal types are translated to equal types. Finally, as explained in Section 2.3, if we give our τ_{2}-continuation the correct type, namely

∀[ ].(ϵ′, T [[τ_{2}]]) → 0at ρ′

then bounded quantification allows the continuation to recover the uniqueness information necessary to deallocate the regions used in the function.

Given these definitions, it is straightforward to prove that the essential properties of types (wellformedness, equality, and substitution) are preserved through the translation. Each of the following lemmas can be proven by a simple induction on the well-formedness or equality derivation.

Lemma 5 (Well-Formedness Preservation)

1. If Δ ⊢_{R} Δ′ then K[[Δ]] ⊢ K[[Δ′]]

2. If Δ ⊢_{R} c : κ then K[[Δ]] ⊢ T [[c]] : K[[κ]]

Lemma 6 (Equality Preservation)

1. If Δ ⊢_{R} ψ = ψ′ : Eff then K[[Δ]] ⊢ \overline{T [[ψ]]} = \overline{T [[ψ′]]} : Cap

2. If Δ ⊢_{R} c = c′ : κ and κ is not Eff then K[[Δ]] ⊢ T [[c]] = T [[c′]] : Cap

Lemma 7 (Substitution Preservation) If Δ, α:κ ⊢_{R} τ : Type and Δ ⊢_{R} c : κ then K[[Δ]] ⊢ T [[τ[c/α]]] = T [[τ]][T [[c]]/α].

Term Translation The heart of the term translation is a continuation-passing style [12, 39] transformation. There are many variations of this transformation [10, 43, 17, 9], some of which produce more efficient code than others, and some of which lead to simpler correctness proofs. We have chosen a simple translation that is straightforward to prove type preserving so that we may focus on the details relevant to region-based memory management.

We begin with an informal description of the basic mechanics of the CPS term translation, ignoring all of the details relevant to regions or capabilities. There are three main arguments to the translation:

• a type-checking context Φ,

• a source-language term e,

• and a target-language continuation k.

If the source term e is well-formed under the context Φ with type τ, and k is a T [[τ]]-continuation then the translation C_{Φ}(e)k should produce a well-formed target term.

Operationally, the target term computes e, producing a value v as a result, and then calls the continuation k with v as its argument. Therefore, if the source term e is already a value v, such as an integer or a variable, then the translation is simply the function call k(v). On the other hand, assuming a left-to-right evaluation order, if the source term e actually represents a computation, say the computation ⟨e_{1}, e_{2}⟩, the CPS translation arranges to compute e_{1} producing value v_{1}, compute e_{2} producing value v_{2}, allocate the pair ⟨v_{1}, v_{2}⟩ and finally pass the resulting pointer to the continuation k. We might write such a translation as follows.

C_{Φ}(⟨e_{1}^{τ_{1}}, e_{2}^{τ_{2}}⟩)k = C_{Φ}(e_{1})(λx_{1}.
C_{Φ,x_{1}:T [[τ_{1}]]}(e_{2})(λx_{2}.
let x = ⟨x_{1}, x_{2}⟩ in k(x)))

The translation of each subcomponent of e requires a continuation and that continuation contains code for all subsequent subcomponents. Finally, the primitive operation op is applied to the resulting values and the result is passed to k. The compilation of arithmetic operations and the projections have this form.

There are a couple of further details to notice about the translation. First, we have taken the liberty of annotating expressions with their types where necessary (e.g., e_{1}^{τ_{1}}). Second, when the translation introduces new variables, such as x_{1}, we add those variables, with their translated types, to the context Φ. The latter decision has no influence on the behaviour of the translation, but it facilitates the statement and proof of the type correctness theorem.

The translation of function application e_{1} e_{2} begins in the same way as other operations: Translate e_{1}, passing the resulting value to a continuation that contains the translation of e_{2}. The continuation for e_{2} contains the function application itself. Because user-defined CPS functions (unlike the primitive operations) do not return, the continuation k is passed directly to the translated function.

C_{Φ}(e_{1}^{τ_{1}→τ_{2}} e_{2})k = C_{Φ}(e_{1})(λx_{1}.
C_{Φ,x_{1}:T [[τ_{1}→τ_{2}]]}(e_{2})(λx_{2}.
x_{1}(x_{2}, k)))

Finally, expressions that declare functions must be translated so the result expects an extra continuation argument (x_{cont}) and calls that continuation to return.

C_{Φ}(let f : τ_{1} → τ_{2} = λx.e in e′) = let f : τ_{f} = λ(x, x_{cont}).C_{Φ,x:T [[τ_{1}]],x_{cont}:τ_{cont}}(e)x_{cont} in
C_{Φ,f:T [[τ_{1}→τ_{2}]]}(e′)k

Here, the type of the function’s continuation, τ_{cont}, is (T [[τ_{2}]]) → 0. The type τ_{f} of the function itself is (T [[τ_{1}]], τ_{cont}) → 0.

This simple CPS translation provides the basic structure for the translation from the region language into the Capability Calculus. However, as many previous researchers have observed, this translation introduces unnecessary or administrative redexes. For example, under the scheme we have presented so far, the translation of a simple pair ⟨2, 3⟩ with respect to a continuation k is

(λx_{1}.(λx_{2}.let x_{3} = ⟨x_{1}, x_{2}⟩ in k(x_{3})) (3)) (2)

instead of the much simpler term let x_{3} = ⟨2, 3⟩ in k (x_{3}). While we are not concerned with the time required to execute the extra function applications, we are concerned about the space required by additional function closures. If we based our region translation directly on this naive translation, we would be forced to allocate additional regions for each of the λ-expressions above. Previous work has avoided these problems by defining the translation in terms of a two-level type system and passing the translation meta-level continuations instead of target-level continuations. However, because we are only interested in the space properties of our translation, we will use a simpler solution. Rather than allocating continuation closures, we will use a let expression to bind the result of a computation and pass it to a continuation. This solution avoids additional allocation and does not lead to the complexities of a two-level type system. Hence, the translation of the pair ⟨2, 3⟩ with respect to continuation k will be

                                  let x_{1} = 2 in
                                  let x_{2} = 3 in

let x_{3} = ⟨x_{1}, x_{2}⟩ in
A(k, x_{3})

The notation A(k, x_{3}) denotes the “application” of the continuation k to the value x_{3}. The continuation k is not represented as a target-language λ-expression, but, intuitively, this “application” is simply k(x_{3}).

The continuation k is actually a pair ⟨x^{k}; e^{k}⟩. The variable x^{k} is the continuation’s parameter and e^{k} is its body. Given this representation, it is natural to define A(⟨x^{k}; e^{k}⟩, v) to be let x^{k} = v in e^{k}.

Using this notation, we can define a CPS translation for pairs in general as follows.

C_{Φ}(⟨e_{1}^{τ_{1}}, e_{2}⟩)k = C_{Φ}(e_{1})⟨x_{1};
C_{Φ,x_{1}:T [[τ_{1}]]}(e_{2})⟨x_{2};
let x = ⟨x_{1}, x_{2}⟩ in A(k, x)⟩⟩

From Region Expressions to Capability Calculus With the basic CPS transformation in hand, we are ready to investigate the formal details translation of the region language expressions into Capability Calculus expressions. As discussed above, the translation, C, has the following form.

C_{Φ}(e)k

The context Φ is actually Δ; Γ; Θ. The first two components are a region type context and a region value context. The third component, Θ, is a translation environment. This environment contains a Capability Calculus type context Δ^{Θ}, a Capability Calculus value context Γ^{Θ}, and a pair of capabilities C^{Θ} and B^{Θ}. The context Δ^{Θ} describes the kinds of the new type variables introduced by the translation and, if they are capability type variables, then possibly their bounds. The value context Γ^{Θ} describes the types of the new value variables introduced by the translation. Intuitively the capability C^{Θ} represents the current capability at a given point in the translation and B^{Θ} is a bound on C^{Θ}. If Θ is ⟨Δ^{Θ}; Γ^{Θ}; C^{Θ}; B^{Θ}⟩, then we use the notation Θ, x:τ to denote the translation environment ⟨Δ^{Θ}; Γ^{Θ}, x:τ; C^{Θ}; B^{Θ}⟩.

The formal translation is presented in Figures 15 and 16. In the translation, we make the assumption that all variables are unique and that when we introduce a variable in a term or in a continuation, it is “fresh” (i.e. it is does not conflict with any of the other variables in the source term, type-checking context, or continuation).

The invariant guiding the transformation has three main parts:

1. The region language term e is well-formed under the type and value contexts Δ and Γ. Formally, Δ; Γ ⊢_{R} e.

2. The continuation k = ⟨x^{k}; e^{k}⟩ is well-formed in the current context. Formally, { }; K[[Δ]], Δ^{Θ}; S[[Γ]], Γ^{Θ}, x^{k}:T [[τ]]; C^{Θ} ⊢ e^{k}.

3. Finally, the current capability C^{Θ} is a subcapability of \overline{B^{Θ}}, and moreover, B^{Θ} contains a superset of the regions mentioned in the effect of e. Formally,

• K[[Δ]], Δ^{Θ} ⊢ C^{Θ} ≤ \overline{B^{Θ}} and

• K[[Δ]], Δ^{Θ} ⊢ \overline{B^{Θ}} = \overline{B^{Θ} ⊕ T [[ψ]]}

As in the case for the simplified CPS translation, the translation of source-language values is the simplest. For example, to translate a variable x or the integer i, we simply apply the continuation k to x or i respectively. The type application expression f[c_{1}, …, c_{n}] is also a value because we take the interpretation that types are erased at run time. Therefore, we apply the continuation k directly to f[T [[c_{1}]], …, T [[c_{n}]]].

A(⟨Γ; x; e⟩, v) = (let x = v in e)

C_{Δ;Γ;Θ}(x)k = A(k, x) C_{Δ;Γ;Θ}(i)k = A(k, i) C_{Δ;Γ;Θ}(f[c_{1}, …, c_{n}])k = A(k, f[T [[c_{1}]], …, T [[c_{n}]]]) C_{Δ;Γ;Θ}(e_{1} p e_{2})k =

C_{Δ;Γ;Θ}(e_{1})⟨x_{1}; C_{Δ;Γ;Θ,x_{1}:int}(e_{2})⟨x_{2}; let x = x_{1} p x_{2} in A(k, x)⟩⟩

C_{Δ;Γ;Θ}(⟨e_{1}^{τ_{1}}, …, e_{n}^{τ_{n}}⟩ at e_{n+1}^{τ_{n+1}})k = C_{Δ;Γ;Θ}(e_{1})⟨x_{1}; ⋮ C_{Δ;Γ;Θ,x_{1}:T [[τ_{1}]],...,x_{n−1}:T [[τ_{n−1}]]}(e_{n})⟨x_{n}; C_{Δ;Γ;Θ,x_{1}:T [[τ_{1}]],...,x_{n}:T [[τ_{n}]]}(e_{n+1})⟨x_{n+1}; let x = ⟨x_{1}, …, x_{n}⟩ at x_{n+1} in A(k, x) ⟩⟩ ⋯⟩

C_{Δ;Γ;Θ}(π_{i}e)k = C_{Δ;Γ;Θ}(e)⟨x_{1}; let x = π_{i}x_{1} in A(k, x)⟩ C_{Δ;Γ;Θ}(if0 e_{1} then e_{2} else e_{3})k =

C_{Δ;Γ;Θ}(e_{1})⟨x_{1}; if0 x_{1} then C_{Δ;Γ;Θ,x_{1}:int}(e_{2})k else C_{Δ;Γ;Θ,x_{1}:int}(e_{3})k⟩

C_{Δ;Γ;Θ}(letregion ρ, x_{ρ} in e)k =

letnewrgn ρ, x_{ρ} in

C_{Δ{ρ:Rgn};Γ{x_{ρ}:ρ handle};Θ′}(e)⟨x′; freergn x_{ρ} in A(k, x′)⟩ where

Θ′ = ⟨Δ^{Θ}; Γ^{Θ}; C^{Θ} ⊕ {ρ^{1}}; B^{Θ} ⊕ {ρ^{1}}⟩

Figure 15: Region to Capability Term Translation C_{Δ;Γ;Θ}(letrecf[Δ′](x) : (∀[Δ′].τ_{1} →^{ψ_{f}} τ_{2} at r) at e_{1} = e_{2} in e_{3})k =

C_{Δ;Γ;Θ}(e_{1})⟨x_{1}; let f = (fix f[K[[Δ′]], ρ:Rgn, ϵ:Cap, ϵ′ ≤ \overline{B^{Θ′}}](ϵ′, x:T [[τ_{1}]], x_{cont}:τ_{cont}).

C_{ΔΔ′;Γ{f:σ,x:τ_{1}};Θ′}(e_{2})⟨x_{2}; x_{cont}(x_{2})⟩) at x_{1}

in

C_{Δ;Γ{f:∀[Δ′].τ_{1} →^{ψ_{f}}τ_{2}atr};Θ,x_{1}:T [[r handle]]}(e_{3})k⟩

where

τ_{cont} = ∀[ ].(ϵ′, T [[τ_{2}]]) → 0at ρ
Δ^{Θ′} = Δ^{Θ}, ρ:Rgn, ϵ:Cap, ϵ′ ≤ \overline{B^{Θ′}}
Γ^{Θ′} = Γ^{Θ}, x_{1}:r handle, x_{cont}:τ_{cont}
C^{Θ′} = ϵ′
B^{Θ′} = ϵ ⊕ T [[ψ_{f}]] ⊕ {ρ^{1}}
Θ′  = ⟨Δ^{Θ′}; Γ^{Θ′}; C^{Θ′}; B^{Θ′}⟩

C_{Δ;Γ;Θ}(e_{1}^{τ_{f}} e_{2})k = C_{Δ;Γ;Θ}(e_{1})⟨x_{1}; C_{Δ;Γ;Θ,x_{1}:T [[τ_{f}]]}(e_{2})⟨x_{2};

letnewrgn ρ, x_{ρ} in

let f_{cont} = (fix f_{cont}[ ](C^{Θ} ⊕ {ρ^{1}}, x:T [[τ_{2}]]).letfreergn x_{ρ} in A(k, x)) at x_{ρ} in x_{1}[ρ, B^{Θ}, C^{Θ} ⊕ {ρ^{1}}](x_{2}, f_{cont})⟩⟩

where

τ_{f} = τ_{1} →^{ψ_{f}} τ_{2} at r

Figure 16: Region to Capability Term Translation (Functions)

The translation of tuples also follows our informal description closely. We translate each of the computations e_{1}, …, e_{n+1} that make up the tuple in sequence and bind the resulting values to x_{1}, …, x_{n+1}. Once we have translated all expressions, we allocate the tuple ⟨x_{1}, …, x_{n}⟩ using the region handle x_{n+1}.

In order for the tuple allocation operation to be safe, we must ensure the region (say, ρ) that corresponds to the region handle x_{n+1} is still live. In other words, we must be able to prove that the current capability C^{Θ} contains a capability for ρ. The invariants above provide us with the means to deduce this fact using the following informal reasoning. Invariant 1 states that the expression ⟨e_{1}, …, e_{n}⟩ at e_{n+1} is well-formed and has effect ψ. Inspection of the region language typing rule for tuples reveals that ψ contains an effect on ρ. Now, the second part of invariant 3 states that the capability B^{Θ} contains capabilities on all regions that appear in the effect ψ, including, of course, ρ. Finally, using the first part of invariant 3, we know that the current capability C^{Θ} is subcapability of B^{Θ}, and, therefore, that it too contains ρ. Consequently, the tuple allocation operation is safe. Using similar reasoning, it is straightforward to verify informally that the translation of arithmetic operations, projections and if statements will not fail to type check because they lack sufficient capabilities.

The translation of the term letregion ρ, x_{ρ} in e is not much more difficult: letregion ρ, x_{ρ} in e is translated into a newrgn ρ, x_{ρ} declaration followed by the translation of the inner expression e and finally a freergn declaration to deallocate ρ. Once again, some simple reasoning allows us to check that the stated invariants hold throughout the transformation. In particular, the translation of the inner expression e reflects the fact that a new region ρ has just been allocated; the translation environment for that step contains capabilities C^{Θ} ⊕ {ρ^{1}} and B^{Θ} ⊕ {ρ^{1}}. Since we know that C^{Θ} is a subcapability of \overline{B^{Θ}}, we may conclude that C^{Θ} ⊕ \{ρ^{1}\} is a subcapability of \overline{B^{Θ} ⊕ \{ρ^{1}\}} and therefore that invariant 3, part 1 is satisfied. Next, inspection of the typing rule for letregion reveals that if ψ′ is the effect of e then ψ′ \ {ρ} is the effect of the entire letregion expression. Since, B^{Θ} contains ψ′ \ {ρ}, we know that B^{Θ} ⊕ {ρ^{1}} contains capabilities for all regions in ψ′, including, of course, ρ. Hence, we also satisfy invariant 3, part 2 during the translation of e. Finally, recall that the region type system ensures that the region ρ can only be used inside of e. Therefore, in the continuation for the translation of e, we safely free the region and proceed with k. Invariant 2 specified that k only expected the capability C^{Θ} and this is exactly the capability of the context after freeing the region ρ.

The most complex part of the translation involves functions. Fortunately, the type translation, which we have already explained, specifies the main invariants; the translation of functions terms follows directly from this specification. More specifically, we extend the function’s type context Δ′ with ρ, a region for the continuation’s closure, ϵ, a capability for hiding extra regions in the calling context, and ϵ′, the current capability, which is bounded by \overline{ϵ ⊕ T [[ψ_{f}]] ⊕ \{ρ^{1}\}}. We also add a value argument to the translated function, the continuation x_{cont}. It is simple to verify that the translated function has the translated function type. The body of the function is translated under these assumptions. The continuation for this part of the translation does nothing but invoke the function’s new argument x_{cont}.

Finally, we examine the translation of a function application. First, the translation allocates a new region ρ for the continuation closure. Next, the translation actually allocates the continuation in ρ. This continuation is defined to expect the capability C^{Θ} ⊕{ρ^{1}}. This is the maximum capability at this point in the computation and it permits the continuation to deallocate the region containing its own closure. After allocating the continuation, the translation continues with the translation of the actual function application. The translated function value, x_{1}, will have the type

∀[ρ′:Rgn, ϵ:Cap, ϵ′ ≤ \overline{ϵ ⊕ T [[ψ_{f}]] ⊕ \{ρ^{′1}\}}].(⋯) → 0at r

Therefore, before calling the function, the code must instantiate the variables ρ′, ϵ, and ϵ′ properly. The code naturally instantiates ρ′ with the region ρ that was just allocated. At this point in the program, the capability C^{Θ} ⊕{ρ^{1}} represents the current capability and B^{Θ} ⊕{ρ^{1}} is its upper bound. Therefore, the code instantiates ϵ with B^{Θ} and ϵ′ with C^{Θ} ⊕ {ρ^{1}}, which is legal provided we can prove that

C^{Θ} ⊕ \{ρ^{1}\} ≤ \overline{B^{Θ} ⊕ ψ_{f} ⊕ \{ρ^{1}\}}

Given invariant 3, which states that C^{Θ} ≤ \overline{B^{Θ}} and that \overline{B^{Θ}} = \overline{B^{Θ} ⊕ ψ_{f}}, it is easy to verify this fact. Now, we need only verify that the term arguments, x_{2} and the continuation f_{cont}, have the types expected by the translated function and this too can be easily checked.

Properties of the Translation We have proven that our translation preserves types.

Theorem 8 (CPS Type Preservation) If ·; · ⊢ e : int, ∅ then { }; ·; ·; ∅ ⊢ C_{·;·;Θ}(e)⟨·; x; halt x⟩ where x is fresh and Θ is the empty enviroment: ⟨·; ·; ∅; ∅⟩.

The proof proceeds by induction on the height typing derivation of the source language term with invariants 1, 2, and 3 forming the induction hypothesis. Appendix B contains a formal proof of the representative cases.

We would also like our translation to preserve the space used by the program. Recently, Minamide [26] has proven that a standard CPS translation preserves the maximum amount of reachable space within a constant factor. He defines a space-profiling semantics for the simply-typed lambda calculus that refines the work of Blelloch and Greiner [7]. If we were to augment our semantics with this sort of space-profiling information, we may be able to prove a similar result for our translation. An informal inspection of the translation indicates that the resultant term allocates no more data structures than the source term with the exception of the continuation closure that we require to return from a function call, and intuitively, this closure corresponds to the stack space that is required to save local variables across a function call. However, a formal investigation of the space properties of our translation is beyond the scope of this paper.

An Example The program below is the translation of the count function from the previous section. We have made several simplifications to the output of the formal translation to improve the readability of the program. In particular, we have optimized away many of the administrative redexes and performed a tail-call optimization on the recursive call to the count function. Rather than writing capabilities \overline{\{ρ_{1}^{1}, ρ^{1}\}}, we use the equivalent form \{ρ_{1}^{+}, ρ^{+}\}.

The program begins by allocating regions ρ_{1} and ρ_{2} using the newrgn declaration, and puts the closure for count into ρ_{1}. The count function requires a capability ϵ′ at least as good as the capability {ρ_{1}^{+}, ρ^{+}, ρ_{cont}^{+}} needed to access itself, its argument, and its continuation; and it passes on that same capability ϵ′ to its continuation k. As we type check the body of the count function, we verify that we possess the capabilities necessary to make all data accesses legal. Comments in the code indicate where these checks occur. When calling count, we pass it the continuation cont. This continuation requires the capability {ρ_{1}^{1}, ρ_{2}^{1}, ρ_{3}^{1}} in order to free the three regions. Hence, at the application site, count’s capability, ϵ′, is instantiated with the stronger capability needed by the continuation.

let newrgn ρ_{1}, x_{ρ_{1}} in
let newrgn ρ_{2}, x_{ρ_{2}} in
% capability held is {ρ_{1}^{1}, ρ_{2}^{1}}
let count =
  (fix count

[ρ:Rgn, ρ_{cont}:Rgn, ϵ:Cap, ϵ′ ≤ \overline{ϵ} ⊕ \{ρ_{1}^{+}, ρ^{+}, ρ_{cont}^{+}\}] (ϵ′, x_{ρ}:ρ handle, x:⟨int⟩ at ρ, k:(ϵ′) → 0at ρ_{cont}) .

% capability held is ϵ′ ≤ \overline{ϵ} ⊕ \{ρ_{1}^{+}, ρ^{+}, ρ_{cont}^{+}\}

    let n = π_{0}(x) in                                % ρ ok
      if0 n

then k() % ρ_{cont} ok

        else
          let n′ = n − 1 in
          let x′ = ⟨n′⟩ at x_{ρ} in                      % ρ ok

count [ρ, ρ_{cont}, \overline{ϵ} ⊕ \{ρ_{1}^{+}, ρ^{+}, ρ_{cont}^{+}\}, ϵ′] (x_{ρ}, x′, k) % ρ_{1} ok

  ) at x_{ρ_{1}} in
let newrgn ρ_{3}, x_{ρ_{3}} in
% capability held is {ρ_{1}^{1}, ρ_{2}^{1}, ρ_{3}^{1}}
let ten = ⟨10⟩ at x_{ρ_{2}} in
let cont =

(λ ({ρ_{1}^{1}, ρ_{2}^{1}, ρ_{3}^{1}}) .

    % capability held is {ρ_{1}^{1}, ρ_{2}^{1}, ρ_{3}^{1}}
    let freergn x_{ρ_{3}} in                              % ρ_{3} unique
    let freergn x_{ρ_{2}} in                              % ρ_{2} unique
    let freergn x_{ρ_{1}} in                              % ρ_{1} unique
      halt 0
  ) at x_{ρ_{3}}
in

count [ρ_{2}, ρ_{3}, {ρ_{1}^{1}, ρ_{2}^{1}, ρ_{3}^{1}}, {ρ_{1}^{1}, ρ_{2}^{1}, ρ_{3}^{1}}] (x_{ρ_{2}}, ten, cont)

Another Example In this context, the count function uses all of the regions that are currently allocated and the capability variable ϵ is redundant. When the code instantiates ϵ at the call site for count, it does so with exactly the regions ρ_{1}, ρ, and ρ_{cont} which already appear in the bound on ϵ′. However, in general, ϵ will hide some “left-over” capability. For example, if we had allocated a fourth region, ρ_{4}, we would need to instantiate ϵ with the capability {ρ_{4}^{1}}⊕{ρ_{1}^{1}, ρ_{2}^{1}, ρ_{3}^{1}} and make corresponding changes to the continuation. Now, ϵ would hide the capability on the fourth region from count but preserve it across the call so it could be deallocated in the continuation:

%%% count with ϵ hiding a left-over capability
let newrgn ρ_{1}, x_{ρ_{1}} in
let newrgn ρ_{2}, x_{ρ_{2}} in
let newrgn ρ_{3}, x_{ρ_{3}} in
let newrgn ρ_{4}, x_{ρ_{4}} in
let count = ... as before ...

% capability held is {ρ_{1}^{1}, ρ_{2}^{1}, ρ_{3}^{1}, ρ_{4}^{1}}
let ten = ⟨10⟩ at x_{ρ_{2}} in
let cont =

(λ ({ρ_{1}^{1}, ρ_{2}^{1}, ρ_{3}^{1}, ρ_{4}^{1}}) ...) at x_{ρ_{2}}

in

count [ρ_{2}, ρ_{3}, {ρ_{4}^{1}} ⊕ {ρ_{1}^{1}, ρ_{2}^{1}, ρ_{3}^{1}}, {ρ_{4}^{1}} ⊕ {ρ_{1}^{1}, ρ_{2}^{1}, ρ_{3}^{1}}] (x_{ρ_{2}}, ten, cont)

The power of bounded quantification comes into play when a function is called with several regions, some of which may or may not be the same. For example, the original code could be rewritten to have ten and cont share a region, without changing the function count in any way:

%%% count with ten and cont sharing ρ_{2}
let newrgn ρ_{1}, x_{ρ_{1}} in
let newrgn ρ_{2}, x_{ρ_{2}} in
let count = ... as before ...
% capability held is {ρ_{1}^{1}, ρ_{2}^{1}}
let ten = ⟨10⟩ at x_{ρ_{2}} in
let cont =

(λ ({ρ_{1}^{1}, ρ_{2}^{1}}) ...) at x_{ρ_{2}}

in

count [ρ_{2}, ρ_{2}, {ρ_{1}^{1}, ρ_{2}^{1}}, {ρ_{1}^{1}, ρ_{2}^{1}}] (x_{ρ_{2}}, ten, cont)

In this example, ρ_{cont} is instantiated with ρ_{2} and ϵ′ is instantiated with {ρ_{1}^{1}, ρ_{2}^{1}} (which is again the capability required by cont). However, count proceeds exactly as before because ϵ′ is still as good as {ρ_{1}^{+}, ρ^{+}, ρ_{cont}^{+}} since:

{ρ_{1}^{1}, ρ_{2}^{1}} ≤ {ρ_{1}^{+}, ρ_{2}^{+}}
= {ρ_{1}^{+}, ρ_{2}^{+}} ⊕ {ρ_{1}^{+}, ρ_{2}^{+}, ρ_{2}^{+}}
= \overline{\{ρ_{1}^{1}, ρ_{2}^{1}\}} ⊕ \{ρ_{1}^{+}, ρ_{2}^{+}, ρ_{2}^{+}\}
= (\overline{ϵ} ⊕ \{ρ_{1}^{+}, ρ_{2}^{+}, ρ_{2}^{+}\})[\{ρ_{1}^{1}, ρ_{2}^{1}\}/ϵ]

An Optimization In the examples above, even though count is tail-recursive, we allocate a new cell each time around the loop and we do not deallocate any of the cells until the count is complete. However, since ρ never contains any live values other than the current argument, it is safe to reduce the program’s space usage by deallocating the argument’s region each time around the loop, as shown in Figure 17. Note that this optimization is not possible when region lifetimes must be lexically scoped.

In order to deallocate its argument, the revised count requires a unique capability for its argument’s region ρ. Note that if the program were again rewritten so that ten and cont shared a region (which would lead to a run-time error, since ten is deallocated early), the program would no longer typecheck, since {ρ_{1}^{1}, ρ_{2}^{1}} ≰ {ρ_{1}^{+}, ρ_{2}^{+}, ρ_{2}^{1}}. However, the program rewritten so that count and cont share a region does not fail at run time, and does typecheck, since {ρ_{1}^{1}, ρ_{2}^{1}} ≤ {ρ_{1}^{+}, ρ_{1}^{+}, ρ_{2}^{1}}.

let newrgn ρ_{1}, x_{ρ_{1}} in
let newrgn ρ_{2}, x_{ρ_{2}} in
% capability held is {ρ_{1}^{1}, ρ_{2}^{1}, ρ_{3}^{1}}
let count =
  (fix count

[ρ:Rgn, ρ_{cont}:Rgn, ϵ ≤ {ρ_{1}^{+}, ρ_{cont}^{+}}] (ϵ ⊕ {ρ^{1}}, x_{ρ}:ρ handle, x:⟨int⟩ at ρ,

k:∀(ϵ) → 0at ρ_{cont}) .

    % capability held is ϵ ⊕ {ρ^{1}}
    let n = π_{0}(x) in                  % ρ ok
    let freergn x_{ρ} in                 % ρ unique
      % capability held is ϵ
      if0 n

then k() % ρ_{cont} ok

        else
          let n′ = n − 1 in
          let newrgn ρ′, x_{ρ′} in
          % capability held is ϵ ⊕ {ρ^{′1}}
          let x′ = ⟨n′⟩ at x_{ρ′} in        % ρ′ ok

count [ρ′, ρ_{cont}, ϵ] (x_{ρ′}, x′, k) % ρ_{1} ok

  ) at x_{ρ_{1}} in
let ten = ⟨10⟩ at x_{ρ_{2}} in
let newrgn ρ_{3}, x_{ρ_{3}} in
let cont =

(λ ({ρ_{1}^{1}, ρ_{3}^{1}}) .

    % capability held is {ρ_{1}^{1}, ρ_{3}^{1}}
    let freergn x_{ρ_{1}} in                % ρ_{1} unique
    let freergn x_{ρ_{3}} in                % ρ_{3} unique
      halt 0
  ) at x_{ρ_{3}}
in

count [ρ_{2}, ρ_{3}, {ρ_{1}^{1}, ρ_{3}^{1}}] (x_{ρ_{2}}, ten, cont)

Figure 17: Count with Efficient Memory Usage

4 From Capability Calculus to Typed Assembly Language

In this section, we informally describe how to construct the backend of a compiler that translates the Capability Calculus into a capability-based typed assembly language.

The continuation-passing style transformation of the previous section makes the order of evaluation of expressions explicit and names all of the intermediate computations. It also reduces all unconditional control-flow transfers to one uniform mechanism: the function call or “functional goto.” Hence, this first transformation performs a significant portion of the compilation of a high-level language. However, we are still a long way from a strongly-typed assembly code.

Morrisett et al. [33] describe how to eliminate high-level language features such as closures and other data structures by compiling them into a strongly-typed RISC-like assembly language. Fortunately, the addition of capability constructs to our CPS-language does not interfere with the type-directed compilation as they describe it. In fact, the capability constructors are the same at the machine language level as they appear in the Capability Calculus that we have already described. Therefore, in this section, we briefly retrace the compilation strategy that has already been laid out for us by Morrisett et al. [33] and point out how it interacts with our capability framework.

4.1 Closure Conversion

Assembly languages do not contain the nested functions that are common in some high-level languages. Closure conversion is the process of transforming each function so that it only depends upon its explicitly declared parameters and does not depend upon values defined in an outer, non-global scope. Once all nested functions have been closed in this way, they may be lifted to the top level. This process usually results in pairing closed function code with an environment to create the closure data structure.

There are many typed closure conversion algorithms of various complexities [27, 33, 32]. Minamide et al. [27] show that closure converting a polymorphic type-passing language requires a very sophisticated target language that includes translucent sums and abstract kinds as well as existential types. Morrisett et al. [33], on the other hand, are able to define a much simpler closure translation because they give up the advantages of a type-passing semantics and assume a type-erasure semantics instead. More recently, Crary et al. [8] have discovered how to preserve the advantages of a type-passing language through closure conversion and yet retain the simplicity of the algorithm proposed by Morrisett et al.. Crary’s approach achieves the expressiveness of type-passing with the simplicity of a type-erasure semantics by passing values that represent types at runtime instead of types themselves. Crary distinguishes between type constructors (erased at runtime) and type representations (values manipulated at runtime) just as we distinguish between region constructors (erased at runtime) and region handles (values manipulated at runtime). This decision allows us to use a much simpler closure conversion algorithm than would be possible in the type-passing region calculus of Tofte and Talpin.

There are many additional considerations in the choice of closure conversion algorithms involving how to represent environments and how to closure convert mutually recursive functions. For the purposes of this paper, we will assume the simple closure transformation described by Morrisett et al.. This algorithm only requires the addition of existential types (∃α.τ) to the type language. The disadvantage of this algorithm is that it recreates the closure each time around the loop of a recursive function.^{3} Morrisett and Harper [32] discuss translations that require either recursive types or a cyclic pack operation and do not incur the overhead of repeated closure creation. Any practical language implementation would choose one of these more efficient translations, but because the details of closure conversion are orthogonal to our central concerns, we assume the simplest alternative here and refer the interested reader to the literature for a deeper investigation of the tradeoffs.

3An observant reader will recognize that this extra allocation must show up as an extra effect in the high-level languages.

4.2 Code Generation

Once closure conversion has been completed, all program memory requirements are explicit. Compiler writers have the opportunity to optimize memory usage further by eliminating closure creation for known functions, optimizing environment representations, and removing the resulting dead regions.

At this point, we begin code generation. Morrisett et al. [33] describe code generation in two phases. The first phase breaks the atomic data structure allocation and initialization of high-level languages into a series of lower level instructions that initialize the fields of the data structure one by one. In order to prevent access to uninitialized fields, they add a flag to each field that indicates whether or not it can be read. For example, the expression let x = ⟨2, 3⟩ at x_{r}in ⋯ becomes

                 let x_{0} = malloc [int, int] at x_{r} in % x_{0} : ⟨int^{0}, int^{0}⟩ at r

let x_{1} = x_{0}[0] ← 2 in  % x_{1} : ⟨int^{1}, int^{0}⟩ at r
let x = x_{1}[1] ← 3 in  % x : ⟨int^{1}, int^{1}⟩ at r
⋯

A 1-flag indicates the field has been initialized is therefore readable. A 0-flag indicates the field has not been initialized. In this case, the initialization steps appear one after another. However, in general, they may separated and if a field is unused, it need not ever be initialized. This flexibility allows an optimizer to schedule instructions as it chooses, without interference from the type system.

The major task of the second phase of code generation is to compile closed code and branching constructs such as our if0 statements into assembly language control-flow operations. At this point, all control transfers become jumps to typed assembly language code blocks. Each of these code blocks has a typing precondition and, for the most part, contains standard assembly language instructions with a few additional typing annotations. Because we have already eliminated high-level abstract data structures such as closures and tuples and named all our intermediate computations, there is almost a one-to-one correspondence between the intermediate language declarations and the assembly language instructions.

The next section describes these typed code blocks precisely and gives a complete description of a capability-based typed assembly language. Because code generation has little impact on the novel features of the Capability Calculus, we refer the reader to the work of Morrisett et al. [33], which gives a formal description of the details of code generation for a closed, continuation-passing style lambda calculus.

Indeed, to accomodate this translation, when checking a recursive region calculus function of type τ_{1} →^{ψ} τ_{2} at r, we must require that ψ contain an effect in region r. Similarly, the capability of a recursive capability calculus function must contain the region that function is allocated in.

4.3 Capability-Based Typed Assembly Language

The Capability-Based Typed Assembly Language is based on the generic Typed Assembly Language of Morrisett et al. [33]. Because of the great similarity, we only discuss the capability features in detail. The syntax for the language is given in Figure 18.

4.3.1 Types

As discussed above, there is little change to the type language. The kind structure is identical and only tuples and function types have changed. Tuple types have initialization flags on each field as discussed in the previous section. Continuation-passing style function types have been translated into code block types with the following form:

∀[Δ].C⇒Γ

As before, these types abstract a type context Δ and specify the capability C that the code requires. However, the typed assembly language does not have alpha-varying variables and uses a fixed set of non-varying registers instead. Therefore, the precondition for the code block is a finite map Γ from registers to types rather than a simple list of types. Furthermore, these types classify code not closures (a pair of code and data) and we assume all code is allocated in its own special region before execution of the program begins. Therefore, we omit the trailing region annotation that appears in the Capability Calculus closure types. Tuples are the only remaining heap-allocated data. The only addition to the type language is the existential type ∃α.τ, which we need to encode the results of closure conversion.

The separation between code and data is also reflected in the memory types, which are now split into a pair of a code region (Υ_{cd}) and the familiar mapping of region names to data regions (Υ).

Figure 19 contains the well-formedness rules for the new types. The rules for the well-formedness of capabilities and other types are identitical to the rules we gave for the Capability Calculus as are the rules governing the well-formedness of contexts and the type equality and subcapability relations. We refer the reader to previous sections for these rules. For technical reasons, the TAL type system requires a simple subtyping relation on tuple types and register file types. These subtyping relations do not interact with capability subtyping. See Morrisett et al. [34] for a discussion of these items or a more complete description of the TAL type structure in general.

4.3.2 Values

In TAL, values are split into three categories: word values, small values, and heap values. Heap values (h), code and tuples, are analogous to their Capability Calculus counterparts except as discussed above. Both small values (v) and word values (w), are “small.” We distinguish between the two because the former contains registers whereas the latter does not. The register file (ℜ) is a mapping from registers (𝔯) to word values. We do not map registers to other registers.

Word values contain the integers (i), data addresses (ν.ℓ), and region handles (handle(ν)) that we saw in the Capability Calculus. Code addresses (cd.ℓ) refer to code in the code region. The word value ?τ is an uninitialized value of type τ. Thus, ⟨?int,?int⟩ is an uninitialized pair of integers. The values w[c] and pack[τ′, w] as τ are both coercions that change the type of the word value w but have no runtime effect (for technical reasons, there are analogous small value forms v[c] and pack[τ′, v] as τ).

kinds  κ ::= Type | Rgn | Cap
constructors  c ::= α | τ | r | C
types  τ ::= α | int | r handle | ∀[Δ]. C⇒Γ | ⟨τ_{1}^{ξ}, …, τ_{n}^{ξ}⟩ at r | ∃α.τ
regions  r ::= ρ | ν
capabilities  C ::= ϵ | ∅ | \{r^{φ}\} | C_{1} ⊕ C_{2} | \overline{C}
multiplicities  φ ::= 1 | +
init flags  ξ ::= 0 | 1
memory types  Ψ ::= {cd : Υ_{cd}, ν_{1} : Υ_{1}, …, ν_{n} : Υ_{n}}
region types  Υ ::= {ℓ_{1} : τ_{1}, …, ℓ_{n} : τ_{n}}
register file types Γ ::= {𝔯_{1} : τ_{1}, …, 𝔯_{n} : τ_{n}}
contexts  Δ ::= · | Δ, α:κ | Δ, ϵ ≤ C
registers  𝔯 ∈ {r1, r2, …}
word values  w ::= ν.ℓ | cd.ℓ | i | ?τ | w[c] | pack[τ′, w] as τ | handle(ν)
small values  v ::= 𝔯 | w | v[c] | pack[τ′, v] as τ
heap values  h ::= ⟨w_{1}, …, w_{n}⟩ | code[Δ]C⇒Γ.I
inst. sequences  I ::= ι; S | jmp v | halt
instructions  ι ::= add 𝔯_{d}, 𝔯_{s}, v | bnz 𝔯, v | freergn v | ld 𝔯_{d}, 𝔯_{s}[i] | malloc 𝔯_{d}, v[τ⃗] |

mov 𝔯_{d}, v | mul 𝔯_{d}, 𝔯_{s}, v | newrgn ρ, 𝔯_{d} | st 𝔯_{d}[i], 𝔯_{s} |

sub 𝔯_{d}, 𝔯_{s}, v | unpack [α, 𝔯_{d}], v
memory  M ::= {cd ↦ R_{cd}, ν_{1} ↦ R_{1}, …, ν_{n} ↦ R_{n}}
heaps  R ::= {ℓ_{1} ↦ h_{1}, …, ℓ_{n} ↦ h_{n}}
register files  ℜ ::= {𝔯_{1} ↦ w_{1}, …, 𝔯_{n} ↦ w_{n}}
programs  P ::= (M, ℜ, I)

Figure 18: Capability-Based TAL Syntax The first is the type instantiation that we saw in the Capability Calculus. If τ is ∃α.τ′′ then the second value form introduces an existential type by hiding τ′ behind the abstract type variable α.

In general, the form and meaning of the static semantic judgements for values are similar to their counter-parts in the Capability Calculus. One addition is the judgement Ψ; Δ; Γ; C ⊢ w : τ^{ξ} fwval, which states that given a well-formed typing context the word value w can be given the flagged type τ^{ξ}. Figure 20 contains the rules for value well-formedness.

4.3.3 TAL Abstract Machine

In general, the TAL instruction set closely ressemble the instructions of a standard RISC instruction set and their semantics should be intuitive. For example, add 𝔯_{d}, 𝔯_{s}, v, adds the contents of register 𝔯_{s} and the value v, and places the result in register 𝔯_{d}. The instructions mul and sub, multiply and subtract in a similar fashion. The ld 𝔯_{d}, 𝔯_{s}[i] instruction loads the ith word from the data block indicated by the pointer in register 𝔯_{s} into the register 𝔯_{d}. The st 𝔯_{d}[i], 𝔯_{s} instruction writes the contents of 𝔯_{s} into the ith word of memory pointed to by 𝔯_{d}. The mov 𝔯_{d}, v instruction, copies the source operand (v) to the destination register (𝔯_{d}). This simplified language also contains two control-flow instructions: jmp v, an unconditional jump to the address contained in v and bnz 𝔯, v, a jump to v if the contents of the register 𝔯 are non-zero and a fall-thru to the next instruction otherwise.

The other instructions cannot be found in a typical RISC instruction set. The commands malloc, newrgn , and freergn are calls to the runtime system. newrgn and freergn allocate and deallocate regions in a similar manner to their high-level counter-parts. malloc 𝔯_{d}, v[τ⃗] allocates space equivalent to the sum of the sizes of the types τ⃗ in the region indicated by the region handle v. The resulting address is placed in register 𝔯_{d}. None of these instructions can be coded in our typed assembly language. Hence, their implementations, along with the implementation of the type checker forms our trusted computing base. Fortunately, these region primitives are much simpler to implement than a standard tracing garbage collector. Hence, we have acheived one of our goals, a reduction in the trusted computing base over previous low-level safe language efforts such as the orginal TAL and Proof-Carrying Code [35].

The last two instructions, halt and unpack are also somewhat special. The unpack instruction is the elimination form for existential types. An existential v of type ∃α.τ is opened and a value of type τ is written to the register 𝔯_{d}. The type variable α is introduced into the type context. At runtime, types are erased so this instruction reduces to either a move, or if v is the same register as 𝔯_{d} (the normal case), this instruction becomes a no-op. Intuitively, the halt instruction returns control to the operating system, which expects an integer in register 𝔯_{1}.

An abstract machine state (P) contains three components: memory, a register file, and a list of instructions. As noted above, memory (M), contains both a code region and a set of data regions. Memory is described by the memory type Ψ. The register file (ℜ), described by the register file type Γ, is a mapping from registers (𝔯) to word values. The typing rules for the abstract machine and its instruction set is presented in Figures 21 and 22. The operational semantics of the machine can be found in Figure 23. Again, given the previous development, the semantics is quite straightforward. In this semantics, we use one additional piece of notation: [c_{1}, …, c_{n}/Δ] denotes the substitution of the constructors c⃗ for the variables in the domain of Δ.

We claim that the static semantics for the TAL abstract machine is sound with respect to the operational semantics:

Δ ⊢ c : κ (new rules)

Δ ⊢ Δ′ Δ, Δ′ ⊢ C : Cap Δ, Δ′ ⊢ Γ
Δ ⊢ ∀[Δ′].C⇒Γ : Type

Δ ⊢ τ_{i} : Type (for 1 ≤ i ≤ n) Δ ⊢ r : Rgn
Δ ⊢ ⟨τ_{1}^{ξ_{1}}, …, τ_{n}^{ξ_{n}}⟩ at r : Type

                                 Δ, α:Type ⊢ τ : Type

Δ ⊢ ∃α.τ : Type

⊢ Ψ ⊢ Υ Δ ⊢ Γ

⊢ Υ_{cd} ⊢ Υ_{i} (for 1 ≤ i ≤ n) ⊢ {cd : Υ_{cd}, ν_{1} : Υ_{1}, …, Υ_{n} : τ_{n}}

· ⊢ τ_{i} : Type ⊢ {ℓ_{1} : τ_{1}, …, ℓ_{n} : τ_{n}}

Δ ⊢ τ_{i} : Type (for 1 ≤ i ≤ n)
Δ ⊢ {𝔯_{1} : τ_{1}, …, 𝔯_{n} : τ_{n}}

Δ ⊢ c_{1} ≤ c_{2} : κ (new rules) Δ ⊢ Γ_{1} ≤ Γ_{2}

{Δ ⊢ c_{1} = c_{2} : κ \atop Δ ⊢ c_{1} ≤ c_{2} : κ}  \begin{matrix}Δ ⊢ c_{1} ≤ c_{2} : κ & Δ ⊢ c_{2} ≤ c_{3} : κ \\ Δ ⊢ c_{1} ≤ c_{3} : κ \end{matrix}
Δ ⊢ τ_{i} : Type (for 1 ≤ i ≤ n) Δ ⊢ r : Rgn

Δ ⊢ ⟨τ_{1}^{ξ_{1}}, …, τ_{j−1}^{ξ_{j−1}}, τ_{j}^{1}, τ_{j+1}^{ξ_{j+1}}, …, τ_{n}^{ξ_{n}}⟩ at r ≤ ⟨τ_{1}^{ξ_{1}}, …, τ_{j−1}^{ξ_{j−1}}, τ_{j}^{0}, τ_{j+1}^{ξ_{j+1}}, …, τ_{n}^{ξ_{n}}⟩ at r : Type

Δ ⊢ τ_{i} = τ′_{i} : Type (for 1 ≤ i ≤ n) Δ ⊢ τ_{i} : Type (for n + 1 ≤ i ≤ m)

Δ ⊢ {𝔯_{1} : τ_{1}, …, 𝔯_{m} : τ_{m}} ≤ {𝔯_{1} : τ′_{1}, …, 𝔯_{n} : τ′_{n}} (m ≥ n)

Figure 19: Capability-Based TAL: Abbreviated Type Well-Formedness Ψ ⊢ h at ν : τ Ψ ⊢ h : τ hcode Ψ; Δ ⊢ w : τ Ψ; Δ ⊢ w : τ^{ξ}

Ψ; · ⊢ w_{i} : τ_{i}^{ξ_{i}} (for 1 ≤ i ≤ n) Ψ; ν ⊢ ⟨w_{1}, …, w_{n}⟩ : ⟨τ_{1}^{ξ_{1}}, …, τ_{n}^{ξ_{n}}⟩ at ν · ⊢ Δ Δ ⊢ C : Cap Δ ⊢ Γ Ψ; Δ; Γ; C ⊢ I

Ψ ⊢ code[Δ]C⇒Γ.I : ∀[Δ]. C⇒Γ hcode
{Δ ⊢ τ = ⟨τ_{1}^{ξ_{1}}, …, τ_{n}^{ξ_{n}}⟩ at ν \atop Ψ; Δ ⊢ ν.ℓ : τ} (ν ∉ Dom(Ψ))  {Δ ⊢ τ_{1} ≤ τ_{2} \atop Ψ; Δ ⊢ ν.ℓ : τ_{2}} (Ψ(ν.ℓ) = τ_{1})
Ψ; Δ ⊢ cd.ℓ : τ_{1} (Ψ(cd.ℓ) = τ_{1}) Ψ; Δ ⊢ i : int Ψ; Δ ⊢ handle(ν) : ν handle
Ψ; Δ ⊢ w : ∀[α:κ, Δ]. C⇒Γ Δ ⊢ c : κ

Ψ; Δ ⊢ w[c] : (∀[Δ]. C⇒Γ)[c/α]

Ψ; Δ ⊢ w : ∀[ϵ≤C_{1}, Δ]. C_{2}⇒Γ Δ ⊢ C ≤ C_{1} : Cap
Ψ; Δ ⊢ w[C] : (∀[Δ]. C_{2}⇒Γ)[C/ϵ]
Δ ⊢ c : Type Ψ; Δ ⊢ w : τ[c/α]

Ψ; Δ ⊢ pack[τ′, w] as ∃α.τ : ∃α.τ

{Ψ; Δ ⊢ w : τ \atop Ψ; Δ ⊢ w : τ^{ξ}}  {Δ ⊢ τ : Type \atop Ψ; Δ ⊢ ?τ : τ^{0}}

Ψ; Δ; Γ ⊢ v : τ

Ψ; Δ; Γ ⊢ 𝔯 : τ (Γ(r) = τ)  {Ψ; Δ ⊢ w : τ \atop Ψ; Δ; Γ ⊢ w : τ}
Ψ; Δ; Γ ⊢ v : ∀[α:κ, Δ]. C⇒Γ Δ ⊢ c : κ

Ψ; Δ; Γ ⊢ v[c] : (∀[Δ]. C⇒Γ)[c/α]

Ψ; Δ; Γ ⊢ v : ∀[ϵ≤C_{1}, Δ]. C_{2}⇒Γ Δ ⊢ C ≤ C_{1} : Cap
Ψ; Δ; Γ ⊢ v[C] : (∀[Δ]. C_{2}⇒Γ)[C/ϵ]
Δ ⊢ c : Type Ψ; Δ; Γ ⊢ v : τ[c/α]

Ψ; Δ; Γ ⊢ pack[τ′, v] as ∃α.τ : ∃α.τ Figure 20: Capability-Based TAL: Value Formation

Ψ; Δ; Γ; C ⊢ I

Ψ; Δ; Γ; C ⊢ ι ⇒ Δ′; Γ′; C′ Ψ; Δ′; Γ′; C′ ⊢ I
Ψ; Δ; Γ; C ⊢ ι; I

Ψ; Δ; Γ ⊢ r1 : τ
Ψ; Δ; Γ; C ⊢ halt [τ]
Ψ; Δ; Γ ⊢ v : ∀[ ]. C′⇒Γ′ Δ ⊢ C ≤ C′ : Cap Δ ⊢ Γ ≤ Γ′
Ψ; Δ; Γ; C ⊢ jmp v

Ψ; Δ; Γ; C ⊢ ι ⇒ Δ′; Γ′; C′ (interesting rules)

Ψ; Δ; Γ ⊢ v : r handle Δ ⊢ C ≤ C′ ⊕ {r} : Cap

Ψ; Δ; Γ; C ⊢ freergn v ⇒ Δ; Γ; C′

Ψ; Δ; Γ ⊢ 𝔯_{s} : ⟨τ_{0}^{ξ_{0}}, …, τ_{n−1}^{ξ_{n−1}}⟩ at r Δ ⊢ C ≤ C′ ⊕ \overline{\{r\}} : Cap

Ψ; Δ; Γ; C ⊢ ld 𝔯_{d}, 𝔯_{s}[i] ⇒ Δ; Γ{𝔯_{d} : τ_{i}}; C (ξ_{i} = 1, 0 ≤ i < n)

Δ ⊢ τ_{i} : Type (for 1 ≤ i ≤ n) Ψ; Δ; Γ ⊢ v : r handle Δ ⊢ C ≤ C′ ⊕ \overline{\{r\}} : Cap

Ψ; Δ; Γ; C ⊢ malloc 𝔯_{d}, v[τ_{1}, …, τ_{n}] ⇒ Δ; Γ{𝔯_{d} : ⟨τ_{1}^{0}, …, τ_{n}^{0}⟩ at r}; C

Ψ; Δ; Γ; C ⊢ newrgn ρ, 𝔯_{d} ⇒ (Δ, ρ); Γ{𝔯_{d} : ρ handle}; (C ⊕ {ρ}) (ρ ∉ Δ)
Ψ; Δ; Γ ⊢ 𝔯_{d} : ⟨τ_{0}^{ξ_{0}}, …, τ_{n−1}^{ξ_{n−1}}⟩ at r Ψ; Δ; Γ; C ⊢ 𝔯_{s} : τ_{i} Δ ⊢ C ≤ C′ ⊕ \overline{\{r\}} : Cap

Ψ; Δ; Γ; C ⊢ st 𝔯_{d}[i], 𝔯_{s} ⇒ Δ; Γ{𝔯_{d}:⟨τ_{0}^{ξ_{0}}, …, τ_{i−1}^{ξ_{i−1}}, τ_{i}^{1}, τ_{i+1}^{ξ_{i+1}}, …, τ_{n−1}^{ξ_{n−1}}⟩ at p}; C

(0 ≤ i < n)

Figure 21: Capability-Based TAL: Instructions ⊢ M : Ψ Ψ ⊢ R at ν : Υ Ψ ⊢ R : Υ Ψ ⊢ ℜ : Γ Ψ ⊢ C sat ⊢ P

⊢ Ψ Ψ ⊢ R_{cd} : Υ_{cd} code Ψ ⊢ R_{i} at ν_{i} : Υ_{i} val (for 1 ≤ i ≤ n)

⊢ {cd : Υ_{cd}, ν_{1} ↦ R_{1}, …, ν_{n} ↦ R_{n}} : Ψ (Ψ = {cd : Υ_{cd}, ν_{1} : Υ_{1}, …, ν_{n} : Υ_{n}})

Ψ ⊢ h_{i} : τ_{i} hcode (for 1 ≤ i ≤ n) Ψ ⊢ {ℓ_{1} ↦ h_{1}, …, ℓ_{n} ↦ h_{n}} : {ℓ_{1} : τ_{1}, …, ℓ_{n} : τ_{n}} code

Ψ; ν ⊢ h_{i} : τ_{i} (for 1 ≤ i ≤ n)

Ψ ⊢ {ℓ_{1} ↦ h_{1}, …, ℓ_{n} ↦ h_{n}} : {ℓ_{1} : τ_{1}, …, ℓ_{n} : τ_{n}} at ν val

{Ψ; · ⊢ w_{i} : τ_{i} (for 1 ≤ i ≤ n) \atop Ψ ⊢ \{𝔯_{1} ↦ w_{1}, …, 𝔯_{n} ↦ w_{m}\} : \{𝔯_{1} : τ_{1}, …, 𝔯_{n} : τ_{n}\}} (m ≥ n)

· ⊢ C = {ν_{1}^{φ_{1}}, …, ν_{n}^{φ_{n}}} : Cap

{ν_{1} : Υ_{1}, …, ν_{n} : Υ_{n}} ⊢ C sat (ν_{i} ≠ ν_{j} for 1 ≤ i, j ≤ n and i ≠ j)

⊢ M : Ψ Ψ ⊢ ℜ : Γ Ψ ⊢ C sat Ψ; ·; Γ; C ⊢ I
⊢ (M, ℜ, I)

Figure 22: Capability-Based TAL: Abstract Machine

(M, R, I) ⟼ P where

if I =  then P =
add r_{d}, r_{s}, v; I′  (M, R{r_{d} ↦ R(r_{s}) + R̂(v)}, I′)

and similarly for mul and sub

bnz r, v; I′  (M, R, I′)

when R(r) = 0

bnz r, v; I′  (M, R, I′′[c⃗/Δ])
when R(r) = i and i ≠ 0 where R̂(v) = cd.ℓ[c⃗]

and M(cd.ℓ) = code[Δ]C⇒Γ.I′′

freergn v  (M′, R, I′′)

where R̂(v) = handle(ν) and ν ∈ Dom(M) and M′ = M\ν

jmp v  (M, R, I′[τ⃗/Δ])

where R̂(v) = cd.ℓ[τ⃗] and M(cd.ℓ) = code[Δ]Γ.I′

ld r_{d}, r_{s}[i]; I′  (M, R{r_{d} ↦ w_{i}}, I′)

where R(r_{s}) = ν.ℓ and M(ν.ℓ) = ⟨w_{0}, …, w_{n−1}⟩ with 0 ≤ i < n

malloc r_{d}, v[τ_{1}, …, τ_{n}]; I′ (M{ν.ℓ ↦ ⟨?τ_{1}, …,?τ_{n}⟩}, R{r_{d} ↦ ν.ℓ}, I′)

where R̂(v) = handle(ν) and ν ∈ Dom(M) and ℓ ∉ M(ν)

mov r_{d}, v; I′  (M, R{r_{d} ↦ R̂(v)}, I′)
newrgn ρ, r_{d}; I′  (M{ν ↦ {}}, R{r_{d} ↦ handle(ν)}, I′[ν/ρ])

where ν is new

st r_{d}[i], r_{s}; I′  (M{ν.ℓ ↦ ⟨w_{0}, …, w_{i−1}, R(r_{s}), w_{i+1}, …, w_{n−1}⟩}, R, I′)

where R(r_{d}) = ν.ℓ and M(ν.ℓ) = ⟨w_{0}, …, w_{n−1}⟩ with 0 ≤ i < n

unpack [α, r_{d}], v; I′  (M, R{r_{d} ↦ w}, I′[τ/α])

where R̂(v) = pack[τ, w] as τ′

Where R̂(v) = \{ \begin{matrix}R(r) & when v = r \\ w & when v = w \\ R̂(v′)[τ] & when v = v′[τ] \\ pack[τ, R̂(v′)] as τ′ & when v = pack[τ, v′] as τ′ \end{matrix}

Figure 23: Operational Semantics of TAL Claim 9 (Capability-Based TAL Type Safety) If ⊢ P, then there is no stuck state P′ such that P ⟼^{∗} P′.

We believe the proof would be long and tedious but straightforward. Like the proof of type safety for the Capability Calculus, this proof is driven by the syntax of the language and does not involve a complicated greatest fixed-point construction.

5 Discussion

We believe the general framework of our capability system is quite robust. There are several ways to extend the language and a number of directions for future research.

5.1 Language Extensions

In this article, we have concentrated on using the Capability Calculus to implement safe region-based memory management, but with a few changes, we believe our capability apparatus may be used in a variety of other settings as well. One potential application involves reducing the overhead of communication across the user-kernel address space boundary in traditional operating systems. Typically, in such systems, when data in user space is presented to the kernel, the kernel must copy that data to ensure its integrity is preserved. However, if a user process hands off a unique capability for a region to the kernel, the kernel does not have to copy that region’s data; without the capability, the user can no longer read or modify the contents of that region.

By handing off a user’s capability to the kernel, we ensure that the kernel has exclusive access to the data governed by the capability. We can generalize this idea and use capabilities to ensure mutuallyexclusive access to shared mutable data in a multi-threaded environment, by viewing locks as analogous to regions. If we associate each piece of sensitive data with a lock, we can statically check that every client of the data obtains the corresponding lock and its associated capability before attempting access. When the code releases the lock, the type system would revoke the capability on the data, just as it revokes a capability after a region is freed. Flanagan and Abadi [13] have investigated this idea in the context of a high-level lexically-scoped language. Just as we compiled Tofte and Talpin’s high-level region language into the Capability Calculus, we conjecture we could compile Flanagan and Abadi’s locking language into a variant of the Capability Calculus with locking primitives instead of allocation primitives.

A third application of capabilities is to control and reason about aliasing on a per-object basis rather than a per-region basis. Smith, Walker, and Morrisett [45] have investigated the idea of associating a different capability with each individual object and including the type of the object within the capability itself. When code possesses the unique capability for an object, it may deallocate the object, or, if it chooses, it may explicitly reuse the space for that object to store a value of a different type. This new design may be viewed as an extension to conventional linear type systems [16, 50] as it admits aliasing and yet allows safe deallocation of objects. Recently, these techniques have been used to extend the Typed Assembly Language implementation [29] with operations for explicit, but verifiably safe memory management.

In general, whenever a system wishes to restrict access to some data statically, and/or to ensure a certain sequence of operations are performed, it may consider using capabilities. In fact, Walker [52] has shown that the combination of capabilities and a simple logic are sufficiently powerful to encode any property that can be enforced using a security automaton. Since security automata can specify any safety property [2, 44], the extended Capability Calculus can too.

5.2 Related Work

There are many formalisms for reasoning about computational effects in programming languages including type-and-effects systems [15, 25, 21, 47], monads [28, 38, 23, 11], linear types [16, 50, 49], and now capabilities. Many researchers are actively investigating the relationships between these different areas, but the overall picture is not yet fully understood. We are eager to continue this line of research and explore the formal links between our system and the others.

Our translation of Tofte and Talpin’s region calculus into the Capability Calculus reveals that the relationship between effects and capabilities is quite close. A necessary prerequisite for the use of either system is type inference, performed by a programmer or compiler, and much of the research into effects systems has concentrated on this difficult task. However, because of the focus on inference, effect systems are usually formulated as a bottom-up synthesis of effects. Our work may viewed as producing verifiable evidence of the correctness of an inference. Hence, while effect systems typically work bottom-up, specifying the effects that might occur, we take a top-down approach, specifying by capabilities the effects that are permitted to occur. Moreover, unlike Tofte and Talpin’s effect system, our capabilities are sensitive to control-flow. Rather than constructing the overall effect of an expression by taking the union of the effects of the subexpressions, and thereby losing information about the order of evaluation, we verify that programs are safe by checking one instruction after another and using the capability produced by previous instructions to verify that the instructions that follow are safe.

A connection can also be drawn between capabilities and monadic type systems. Work relating effects to monads has viewed effectful functions as pure functions that return state transformers. This might be called an ex post view: the effect takes place after the function’s execution. In contrast, we take an ex ante view in which the capability to perform the relevant effect must be satisfied before the function’s execution. Nevertheless, there is considerable similarity between the views; just as the monad laws ensure that the store is single-threaded through a computation, our typing rules thread a capability (which summarizes aspects of the store) along the execution path of a program.

Perhaps the closest relationship occurs between linear type systems and capabilities. An inspection of the axioms of capability equality reveals that they are very similar to the structural rules of linear type systems (See Wadler [50] for an introduction to linear logic). In particular, linear assumptions, like unique capabilities, do not allow contraction and weakening rules whereas non-linear assumptions, like duplicatable capabilities, do allow contraction and weakening rules.^{4} One essential difference between the two formalisms is that the capability to access an object (say, {ρ^{1}}) is separated from the type of the object itself (say, ⟨int⟩ at ρ). This level of indirection makes it possible to allow aliasing and yet verify that deallocation is still safe, operations that are not permissible in conventional linear type systems.

There has also been a significant amount of prior research on the more specific topic of the theory and implementation of region-based memory management. On the implementation side, Birkedal et al. [6] describe several optimizations to the basic region-allocation scheme that are used in the ML Kit with Regions to improve space-efficiency. One of their observations is that functions can be used in two different contexts: one context in which no live object remains in a region after a function call and a second context in which there may be live objects remaining in a region after a call. In order to avoid code duplication and yet ensure efficient space usage, the call site passes information to the called function at run time. Using this information, the function may make dynamic decisions about region deallocation. The type system we present here is not powerful enough to encode these storage-mode polymorphic functions. However, we believe these dynamic tests may be viewed as form of intensional type analysis [18, 8], and, therefore, if we augment the Capability Calculus with a variant of Harper and Morrisett’s typecase mechanism, we may be able to verify the results of storage-mode optimizations as well.

4Many formulations of linear logic admit a weakening rule that allows an assumption to be completely forgotten. As explained earlier, we do not allow complete forgetting of capabilities because it leads to space leaks. Instead, we admit a more restrictive weakening rule that allows all but the last capability to be forgotten.

Aiken et al. [1] have also studied how to optimize the original Tofte-Talpin region framework. As in the Capability Calculus, they separate region allocation from region deallocation. However, they have not presented a technique for verifying that the results of their optimizations are safe. We conjecture, based on the soundness proof for Aiken et al.’s analyses, that the analysis could be used to produce typing annotations and that verification could take place using the Capability Calculus.

Gay and Aiken [14] have developed extensions to C that gives programmers complete control over region allocation and deallocation. They use reference counting to prevent programmers from accidentally accessing deallocated regions. Hawblitzel and von Eicken [20] have also used the notion of a region in their language Passport to support sharing and revocation between multiple protection domains. Both of these groups use run-time checking to ensure safety and it would be interesting to investigate hybrid systems that combine features of our static type system with more dynamic systems.

On the theory side, we believe that one of our most important contributions is the syntactic proof of the soundness of region deallocation. As mentioned earlier, our formulation of the Capability Calculus allows us to use the standard proof techniques popularized by Wright and Felleisen [54]. Although long, the proof requires very little creativity. In contrast, Tofte and Talpin [48] use a greatest fixed-point construction and a co-inductive argument to prove the correctness of their region-inference scheme. Despite these high-level differences between the proof techniques, there are illuminating similarities in some of the details of the proof. Most notably, Tofte and Talpin’s proof involves a notion of consistency that relates source and target values in the region inference translation. Consistency is defined with respect to the effect (ψ) of the rest of the computation. Informally, one of the consistency conditions states that a source value is consistent with a target value in region ρ, with respect to effect ψ, if ρ does not appear in ψ. Hence, if ρ is not in the effect, or capability, of the rest of the computation, then we can deallocate that region because the rest of the computation cannot distinguish a dangling pointer into ρ from a value in the source language. Therefore, within the Tofte-Talpin proof, the effect of the rest of the computation plays a role very similar to the capability required by a continuation. So perhaps the key reason that our language admits a syntactic proof of soundness is that it makes continuations and their capabilities explicit in the language whereas Tofte and Talpin introduce this idea as a meta-level construction in their proof.

6 Conclusions

We have presented a new strongly typed language that admits operations for explicit allocation and deallocation of data structures. Furthermore, this language is expressive enough to serve as a target for region inference and admits a relatively straightforward proof of soundness. We believe that the notion of capabilities that support statically checkable attenuation, amplification, and revocation is an effective new tool for language designers.

7 Acknowledgements

We would like to thank Lars Birkedal, Martin Elsman, Dan Grossman, Chris Hawblitzel, Fred Smith, Mads Tofte, Stephanie Weirich, Steve Zdancewic, and the anonymous reviewers for their comments and suggestions on earlier versions of this work.

References

[1] Alexander Aiken, Manuel Fähndrich, and Raph Levien. Better static memory management: Improving region-based analysis of higher-order languages. In ACM Conference on Programming Language Design and Implementation, pages 174–185, La Jolla, California, 1995.

[2] Bowen Alpern and Fred Schneider. Recognizing safety and liveness. Distributed Computing, 2:117– 126, 1987.

[3] H. G. Baker. List processing in real-time on a serial computer. Communications of the ACM, 21(4):280–294, 1978.

[4] Brain Bershad, Stefan Savage, Przemyslaw Pardyak, Emin Sirer, Marc Fiuczynski, David Becker, Craig Chambers, and Susan Eggers. Extensibility, safety and performance in the SPIN operating system. In Fifteenth ACM Symposium on Operating Systems Principles, pages 267–284, Copper Mountain, December 1995.

[5] Lars Birkedal, Nick Rothwell, Mads Tofte, and David N. Turner. The ML Kit (version 1). Technical Report 93/14, Department of Computer Science, University of Copenhagen, 1993.

[6] Lars Birkedal, Mads Tofte, and Magnus Vejlstrup. From region inference to von Neumann machines via region representation inference. In Twenty-Third ACM Symposium on Principles of Programming Languages, pages 171–183, St. Petersburg, January 1996.

[7] Guy Blelloch and John Greiner. A provably time and space efficient implementation of NESL. In ACM International Conference on Functional Programming, pages 213–225, June 1996.

[8] Karl Crary, Stephanie Weirich, and Greg Morrisett. Intensional polymorphism in type-erasure semantics. In ACM International Conference on Functional Programming, pages 301–312, Baltimore, September 1998.

[9] Olivier Danvy, Belmina Dzafic, and Frank Pfenning. On proving syntactic properties of CPS programs. In Third International Workshop on Higher-Order Operational Techniques in Semantics, September 1999. Published in Alan Gordon and Andrew Pitts, editors, Electronic Notes in Computer Science, volume 26, pages 19-31. 1999.

[10] Olivier Danvy and Andrzej Filinski. Representing control: a study of the CPS transformation. Mathematical Structures in Computer Science, 2(4):361–391, December 1992.

[11] Andrzej Filinski. Controlling Effects. PhD thesis, Carnegie Mellon University, School of Computer Science, Pittsburgh, Pennsylvania, May 1996.

[12] M. J. Fischer. Lambda calculus schemata. In Proceedings of the ACM Conference on Proving Assertions about Programs, pages 104–109, 1972.

[13] Cormac Flanagan and Martin Abadi. Types for safe locking. In Proceedings of the Eighth European Symposium on Programming, pages 91–108, March 1999.

[14] David Gay and Alex Aiken. Memory management with explicit regions. In ACM Conference on Programming Language Design and Implementation, pages 313 – 323, Montreal, June 1998.

[15] D. K. Gifford and J. M. Lucassen. Integrating functional and imperative programming. In ACM Conference on Lisp and Functional Programming, Cambridge, Massachusetts, August 1986.

[16] Jean-Yves Girard. Linear logic. Theoretical Computer Science, 50:1–102, 1987.

[17] Robert Harper and Mark Lillibridge. Explicit polymorphism and CPS conversion. In Twentieth ACM Symposium on Principles of Programming Languages, pages 206–219, Charleston, January 1993.

[18] Robert Harper and Greg Morrisett. Compiling polymorphism using intensional type analysis. In Twenty-Second ACM Symposium on Principles of Programming Languages, pages 130–141, San Francisco, January 1995.

[19] Chris Hawblitzel, Chi-Chao Chang, Grzegorz Czajkowski, Deyu Hu, and Thorsten von Eicken. Implementing multiple protection domains in Java. In 1998 USENIX Annual Technical Conference, New Orleans, June 1998.

[20] Chris Hawblitzel and Thorsten von Eicken. Sharing and revocation in a safe language. Unpublished manuscript., 1998.

[21] Pierre Jouvelot and D. K. Gifford. Algebraic reconstruction of types and effects. In Eighteenth ACM Symposium on Principles of Programming Languages, pages 303–310, January 1991.

[22] Dexter Kozen. Efficient code certification. Technical Report TR98-1661, Cornell University, January 1998.

[23] John Launchbury and Simon L. Peyton Jones. State in Haskell. LISP and Symbolic Computation, 8(4):293–341, December 1995.

[24] Tim Lindholm and Frank Yellin. The Java Virtual Machine Specification. Addison-Wesley, 1996.

[25] John M. Lucassen. Types and Effects—Towards the Integration of Functional and Imperative Programming. PhD thesis, MIT Laboratory for Computer Science, 1987.

[26] Y. Minamide. Space-profiling semantics of the call-by-value lambda calculus and the CPS transformation. In Third International Workshop on Higher-Order Operational Techniques in Semantics, September 1999. Published in Alan Gordon and Andrew Pitts, editors, Electronic Notes in Computer Science, volume 26, pages 103-118. 1999.

[27] Y. Minamide, G. Morrisett, and R. Harper. Typed closure conversion. In Twenty-Third ACM Symposium on Principles of Programming Languages, pages 271–283, St. Petersburg, January 1996.

[28] Eugenio Moggi. Notions of computation and monads. Information and Computation, 93:55–92, 1991.

[29] Greg Morrisett, Karl Crary, Neal Glew, Dan Grossman, Richard Samuels, Frederick Smith, David Walker, Stephanie Weirich, and Steve Zdancewic. Typed Assembly Language for the Intel IA32 architecture. See http://www.cs.cornell.edu/talc for the latest implementation.

[30] Greg Morrisett, Matthias Felleisen, and Robert Harper. Abstract models of memory management. In ACM Conference on Functional Programming and Computer Architecture, pages 66–77, La Jolla, June 1995.

[31] Greg Morrisett and Robert Harper. Semantics of memory management for polymorphic languages. In A.D. Gordon and A.M. Pitts, editors, Higher Order Operational Techniques in Semantics, Publications of the Newton Institute. Cambridge University Press, 1997.

[32] Greg Morrisett and Robert Harper. Typed closure conversion for recursively-defined functions (extended abstract). In Carolyn Talcott, editor, Higher-Order Techniques in Operational Semantics, volume 10 of Electronic Notes in Theoretical Computer Science. Elsevier, 1998.

[33] Greg Morrisett, David Walker, Karl Crary, and Neal Glew. From System F to Typed Assembly Language. In Twenty-Fifth ACM Symposium on Principles of Programming Languages, pages 85–97, San Diego, January 1998.

[34] Greg Morrisett, David Walker, Karl Crary, and Neal Glew. From System F to Typed Assembly Language. ACM Transactions on Progamming Languages and Systems, 21(3):528–569, May 1999.

[35] George Necula. Proof-carrying code. In Twenty-Fourth ACM Symposium on Principles of Programming Languages, pages 106–119, Paris, 1997.

[36] George Necula and Peter Lee. Safe kernel extensions without run-time checking. In Proceedings of Operating System Design and Implementation, pages 229–243, Seattle, October 1996.

[37] George Necula and Peter Lee. The design and implementation of a certifying compiler. In ACM Conference on Programming Language Design and Implementation, pages 333 – 344, Montreal, June 1998.

[38] Simon L. Peyton Jones and Philip Wadler. Imperative functional programming. In Twentieth ACM Symposium on Principles of Programming Languages, Charleston, South Carolina, January 1993.

[39] G. D. Plotkin. Call-by-name, call-by-value, and the lambda calculus. Theoretical Computer Science, 1:125–159, 1975.

[40] John C. Reynolds. Definitional interpreters for higher-order programming languages. In Conference Record of the 25th National ACM Conference, pages 717–740, Boston, August 1972.

[41] John C. Reynolds. Syntactic control of interference. In Fifth ACM Symposium on Principles of Programming Languages, pages 39–46, Tucson, Arizona, 1978.

[42] John C. Reynolds. Syntactic control of interference, part 2. In Sixteenth International Colloquium on Automata, Languages, and Programming, July 1989.

[43] Amr Sabry and Matthias Felleisen. Reasoning about programs in continuation-passing style. LISP and Symbolic Computation, 6(3/4):289–360, 1993.

[44] Fred Schneider. Enforceable security policies. Technical Report TR98-1664, Cornell University, January 1998.

[45] Frederick Smith, David Walker, and Greg Morrisett. Alias types. Technical Report TR99-1773, Cornell University, October 1999.

[46] Mads Tofte and Lars Birkedal. A region inference algorithm. Transactions on Programming Languages and Systems, November 1998. To appear.

[47] Mads Tofte and Jean-Pierre Talpin. Implementation of the typed call-by-value λ-calculus using a stack of regions. In Twenty-First ACM Symposium on Principles of Programming Languages, pages 188–201, Portland, Oregon, January 1994.

[48] Mads Tofte and Jean-Pierre Talpin. Region-based memory management. Information and Computation, 132(2):109–176, 1997.

[49] Philip Wadler. Linear types can change the world! In M. Broy and C. Jones, editors, Programming Concepts and Methods, Sea of Galilee, Israel, April 1990. North Holland. IFIP TC 2 Working Conference.

[50] Philip Wadler. A taste of linear logic. In Mathematical Foundations of Computer Science, volume 711 of LNCS, Gdansk, Poland, August 1993. Springer-Verlag.

[51] Robert Wahbe, Steven Lucco, Thomas Anderson, and Susan Graham. Efficient software-based fault isolation. In Fourteenth ACM Symposium on Operating Systems Principles, pages 203–216, Asheville, December 1993.

[52] David Walker. A type system for expressive security policies. In Twenty-Seventh ACM Symposium on Principles of Programming Languages, January 2000. To appear.

[53] Paul R. Wilson. Uniprocessor garbage collection techniques. In Yves Bekkers and Jacques Cohen, editors, International Workshop on Memory Management, number 637 in Lecture Notes in Computer Science, pages 1–42, St. Malo, September 1992. Springer-Verlag.

[54] Andrew K. Wright and Matthias Felleisen. A syntactic approach to type soundness. Information and Computation, 115(1):38–94, 1994.

[55] W. A. Wulf, R. Levin, and S. P. Harbison. Hydra/C.mmp: An Experimental Computer System. McGraw-Hill, New York, NY, 1981.

A Soundness of The Capability Calculus

Notation The capability {r^{+}} is a derived form that we used for expository purposes in the article. It is equivalent to \overline{\{r^{1}\}}. For the sake of simplicity, the proof operates on a new language that does not include capabilities of the form {r^{+}}. The syntax of capabilities is:

C ::= ϵ | ∅ | \{r\} | C_{1} ⊕ C_{2} | \overline{C}

The form {r} is the new syntax for unique capabilities. The only way to form a duplicatable capability is to use the bar operator as in \overline{\{r\}}, hence multiplicity annotations are unnecessary. The rule eq-flag is a derived rule. If the abbreviation {r^{+}} is replaced by its definition, it is clear the rule is simply a special case of reflexivity, and therefore, we do not need it in our system. Where convenient, we continue to use \{r^{+}\} as an abbreviation for \overline{\{r\}}.

We also use the following notational conventions:

- Alpha-equivalent expressions are considered identical.

- Memories, memory regions, memory types, and region types that differ only in the order of their fields are considered identical.

- The expression E[E′/X] denotes the capture-avoiding substitution of E′ for X in E.

- Updates of finite maps M are denoted by M{X↦E} or M{X:E}.

- Juxtaposition of two maps M and MN as in MN denotes an update of the first with the elements of the second.

- The notation M\X excludes X from the domain of map M.

- We abbreviate M(ν)(ℓ) by M(ν.ℓ).

- We abbreviate M{ν ↦ M(ν){ℓ ↦ E}} by M{ν.ℓ ↦ E}.

- We abbreviate (⋯ ((∅ ⊕ {r_{1}^{φ_{1}}}) ⊕ {r_{2}^{φ_{2}}}) ⋯) ⊕ {r_{n}^{φ_{n}}} by {r_{1}^{φ_{1}}, …, r_{n}^{φ_{n}}}.

- We abbreviate (⋯ ((∅ ⊕ C_{1}) ⊕ C_{2}) ⋯) ⊕ C_{n} by C_{1} ⊕ ⋯ ⊕ C_{n}.

- We use the notation C ∈ C′ to denote the fact that C appears in the syntax of C′.

Overview The proof is broken down into a series of lemmas, most of which are proven by induction on the typing derivations or by induction on the syntax of the language. The proof culminates in a proof Type Soundness and Complete Collection. The supporting lemmas are grouped as follows:

- Lemmas 10 to 12 describe when extensions to type contexts or exchanges of elements within a type context are permissible.

- Lemmas 13 to 15 state that constructors involved in equality and subtyping judgements are wellformed and that all free variables of well-formed constructors are bound by the type context.

- Definitions and lemmas 16 to 23 describe which capabilities are equal to one another and which capabilities are subtypes of one another. They provide a higher level of abstraction than the rules for equality and subtyping and are used frequently in the rest of the proof.

- Lemmas 24 and 25 are substitution lemmas for types and values respectively.

- Lemma 26 states that well-formed small values, heap values, and declarations have well-formed types.

- Lemmas 27 to 29 are Canonical Forms lemmas. Given a type, these lemmas describe the shape of memory or of values.

- Lemmas 30 to 32 describe the conditions under which you can add labels or regions to the memory type and preserve typing.

- Lemma 34 states that satisfiability is preserved across equality and subtyping (under the empty context).

- Lemma 35 states that satisfiability is preserved when a region and the corresponding unique capability are removed both from memory and the current capability simulataneously.

- Lemmas 36 and 37 are the Preservation and Progress lemmas respectively. They are used directly

in the proof of Type Soundness. Lemma 10 If Δ ⊢ Δ′ then Dom(Δ) ∩ Dom(Δ′) = ∅. Proof: By induction on the derivation. □ Lemma 11 (Type Context Exchange) If Dom(Δ_{1}) ∩ Dom(Δ_{2}) = ∅ then

1. If Δ_{0}Δ_{1}Δ_{2}Δ_{3} ⊢ Δ then Δ_{0}Δ_{2}Δ_{1}Δ_{3} ⊢ Δ

2. If Δ_{0}Δ_{1}Δ_{2}Δ_{3} ⊢ c : κ then Δ_{0}Δ_{2}Δ_{1}Δ_{3} ⊢ c : κ Proof: By induction on the derivations. In the rule type-var:

Δ_{0}Δ_{1}Δ_{2}Δ_{3} ⊢ α : κ (Δ_{0}Δ_{1}Δ_{2}Δ_{3}(α) = κ)

we know Δ_{0}Δ_{1}Δ_{2}Δ_{3}(α) = Δ_{0}Δ_{2}Δ_{1}Δ_{3}(α) because the domains of Δ_{1} and Δ_{2} are disjoint. Consequently, Δ_{0}Δ_{2}Δ_{1}Δ_{3} ⊢ α : κ. □ Lemma 12 (Type Context Extension) If Δ ⊢ Δ′ then

1. If Δ ⊢ Δ′′ and Dom(Δ′′) ∩ Dom(Δ′) = ∅ then ΔΔ′ ⊢ Δ′′

2. If Δ ⊢ c : κ then ΔΔ′ ⊢ c : κ

3. If Δ ⊢ c_{1} = c_{2} : κ then ΔΔ′ ⊢ c_{1} = c_{2} : κ

4. If Δ ⊢ c_{1} ≤ c_{2} : κ then ΔΔ′ ⊢ c_{1} ≤ c_{2} : κ

Proof: By induction on the derivation. Almost all cases follow directly from the inductive hypothesis. Rules ctxt-sub and type-arrow require Type Context Exchange where Δ_{3} is ·. In part 2, the rules type-var and type-sub, and in part 3, the congruence rules for type variables α, and in part 4, the rule sub-var follow because, by reflemma:disjoint-domains, Dom(Δ) ∩ Dom(Δ′) = ∅ and thus Δ(α) = ΔΔ′(α).

□ Lemma 13 If Δ ⊢ c : κ then ftv(c) ⊆ Dom(Δ). Proof: By induction on the derivation. Lemma 14 (Equality Regularity) If Δ ⊢ C = C′ : κ then Δ ⊢ C : κ and Δ ⊢ C′ : κ. Proof: By induction on the derivation. Lemma 15 (Subtyping Regularity) If · ⊢ Δ and Δ ⊢ C ≤ C′ : κ then Δ ⊢ C : κ and Δ ⊢ C′ : κ. Proof: By induction on the derivation. In the rule sub-var, we show by induction on the derivation · ⊢ Δ, that if Δ(ϵ) =≤ C then Δ ⊢ Δ(ϵ) : Cap. □ Definition 16 (Atomic Element) An atomic element, a, is a type variable ϵ of kind Cap, a singleton capability \{r\}, or a barred capability \overline{ϵ} or \overline{\{r\}}. The meta-variable a ranges over atomic elements. Definition 17 E(C) is the set of elements ϵ or {r} that appear in C (where {|x_{1}, …, x_{n}|} is notation for the set of elements x_{1}, …, x_{n}):

E(∅) = ∅
E({r}) = {|{r}|}
E(ϵ) = {|ϵ|}
E(C_{1} ⊕ C_{2}) = E(C_{1}) ∪ E(C_{2})
E(\overline{C}) = E(C)

Lemma 18 (Equality) If Δ ⊢ C : Cap then 1. Δ ⊢ C = a_{1} ⊕ ⋯ ⊕ a_{n} : Cap for some atomic capabilities a_{1}, …, a_{n}

2. Δ ⊢ a_{1} ⊕ ⋯ ⊕ a_{i−1} ⊕ a_{i} ⊕ a_{i+1} ⊕ ⋯ ⊕ a_{n} = a′_{1} ⊕ ⋯ ⊕ a_{i−1} ⊕ a_{i+1} ⊕ ⋯ ⊕ a_{n} ⊕ a_{i} : Cap

3. Δ ⊢ a_{1} ⊕ ⋯ ⊕ a_{n} = a′_{1} ⊕ ⋯ ⊕ a′_{n} : Cap where a′_{1}, …, a′_{n} is any permutation of a_{1}, …, a_{n}.

4. Δ ⊢ a_{1} ⊕ ⋯ ⊕ a_{n} = a′_{1} ⊕ ⋯ ⊕ a′_{m} : Cap where a′_{1}, …, a′_{m} is a subsequence of a_{1}, …, a_{n} with all duplicate barred elements removed.

5. If Δ ⊢ C = C′ : Cap then the sets E(C) and E(C′) are equal.

6. If E(C) = E(C′) and Δ ⊢ C′ : Cap then Δ ⊢ \overline{C} = \overline{C′} : Cap.

7. If Δ ⊢ C ⊕ {r} = C′ ⊕ {r} : Cap then Δ ⊢ C = C′ : Cap.

Proof:

Part 1 follows by induction on the derivation Δ ⊢ C : Cap. Case type-∅ is immediate. Case type-single, follows from application of the equality rules eq-symm and eq-∅. Case type-plus is more intricate. The inductive hypothesis gives us:

Δ ⊢ C_{1} = a_{1} ⊕ ⋯ ⊕ a_{n} : Cap
Δ ⊢ C_{2} = a′_{1} ⊕ ⋯ ⊕ a′_{m} : Cap

By induction on m and using the rules eq-∅, eq-assoc, and eq-trans

Δ ⊢ a′_{1} ⊕ ⋯ ⊕ a′_{m} = a′_{1} ⊕ (a′_{2} ⊕ ⋯ ⊕ (a′_{m−1} ⊕ a′_{m}) ⋯) : Cap

By equality congruence and eq-trans,

Δ ⊢ C_{1} ⊕ C_{2} = (a_{1} ⊕ ⋯ ⊕ a_{n}) ⊕ a′_{1} ⊕ (a′_{2} ⊕ ⋯ ⊕ (a′_{m−1} ⊕ a′_{m}) ⋯) : Cap

By induction on m again and using eq-assoc, eq-symm, and eq-trans,

Δ ⊢ C_{1} ⊕ C_{2} = a_{1} ⊕ ⋯ ⊕ a_{n} ⊕ a′_{1} ⊕ ⋯ ⊕ a′_{m} : Cap

For the case \overline{C}, we have Δ ⊢ C = a_{1} ⊕⋯⊕a_{n} : Cap by IH. By congruence, Δ ⊢ \overline{C} = \overline{a_{1} ⊕ ⋯ ⊕ a_{n}} : Cap. By induction on n, Δ ⊢ \overline{C} = \overline{a_{1}} ⊕ ⋯ ⊕ \overline{a_{n}} : Cap. For each a_{i}, either \overline{a_{i}} is an atomic element or a_{i} is already barred and we use the eq-bar-idem rule to show that Δ ⊢ \overline{a_{i}} = a_{i} : Cap. In either case, by induction on n again and use of the congruence rules, we are done.

Part 2 follows by induction on m−i using eq-assoc, eq-comm as well as the transitivity and symmetry of equality. Part 3 is a corollary of part 2. Part 4 follows by induction on the number of barred duplicates and uses part 3, transitivity, symmetry, and eq-dup rules. Part 5 follows by induction on the equality judgement.

Part 6 may be proven as follows: Δ ⊢ C = a_{1} ⊕ ⋯ ⊕ a_{n} : Cap where E(C) = E(a_{1} ⊕ ⋯ ⊕ a_{n}) by parts 1 and 5. Δ ⊢ C′ = a′_{1} ⊕ ⋯ ⊕ a′_{m} : Cap where E(C′) = E(a′_{1} ⊕ ⋯ ⊕ a′_{m}) by parts 1 and 5. By parts 3 and 4 and congruence of equality: Δ ⊢ \overline{C} = \overline{a_{1} ⊕ ⋯ ⊕ a_{n}} = a_{j_{1}} ⊕ a_{j_{n}} : Cap Δ ⊢ \overline{C′} = \overline{a′_{1} ⊕ ⋯ ⊕ a′_{m}} = a′_{j_{1}} ⊕ a′_{j_{m}} : Cap where the a_{j_{i}} and a′_{j_{i}} contain no duplicates and are ordered according to some canonical ordering. If E(C) = E(C′) then the a_{j_{i}} and the a′_{j_{i}} are the same and are in the same order. Hence, the constructors are syntactically equal and thus definitionally equal.

Part 7 follows by induction on the typing derivation.

□

Definition 19 (Unique/Duplicatable Capabilities) A capability C is unique in C′ if there does not exist C′′ such that \overline{C′′} ∈ C′ and C ∈ C′′. A capability C is duplicatable in C′ if \overline{C′′} ∈ C′ and C ∈ \overline{C′′}.

Lemma 20 If Δ ⊢ C′ : Cap and C is duplicatable in C′ then Δ ⊢ C′ = C′′ ⊕ \overline{C} : Cap.

Proof: By induction on the typing derivation.

Lemma 21 If Δ ⊢ C′ : Cap and C is unique in C′ then Δ ⊢ C′ = C′′ ⊕ C : Cap. Proof: By induction on the typing derivation. Lemma 22 (Capability Equality Cardinality Preservation(CECP)) If Δ ⊢ C_{1} = C_{2} : Cap and Δ ⊢ a : Cap and a = ϵ or {r} then

1. a is unique (duplicatable) in C_{1} iff a is unique (duplicatable) in C_{2}.

2. The number of unique occurences of a is the same in C_{1} and C_{2}.

Proof: By induction on the derivation. Lemma 23 (Capability Subtyping Cardinality Preservation(CSCP)) If · ⊢ C_{1} ≤ C_{2} : Cap then

1. For all region names ν, {ν} ∈ C_{1} iff {ν} ∈ C_{2}.

2. For all region names ν, if {ν} is not unique in C_{1} then {ν} is not unique in C_{2}.

Proof: By induction on the derivation and Capability Equality Cardinality Preservation. Note that by Subtyping Regularity and Lemma 13, no type variables ϵ appear in C_{1} and consequently, the rule sub-var never appears in the derivation. □ Lemma 24 (Type Substitution) If Δ′ is b_{1}, …, b_{n} where for 1 ≤ i ≤ n: A1. if b_{i} is α_{i}:κ_{i} then · ⊢ c_{i} : κ_{i} A2. if b_{i} is ϵ_{i} ≤ C_{i} then · ⊢ c_{i} ≤ C_{i} : Cap Then when Δ_{0} is Δ[τ⃗/Δ′] Γ_{0} is Γ[τ⃗/Δ′] C_{0} is C[τ⃗/Δ′] r_{0} is r[τ⃗/Δ′] τ_{0} is τ[τ⃗/Δ′]:

1. If Δ′, Δ ⊢ Δ′′ then Δ_{0} ⊢ Δ′′[τ⃗/Δ′]

2. If Δ′, Δ ⊢ c : κ then Δ_{0} ⊢ c[τ⃗/Δ′] : κ

3. If Δ′, Δ ⊢ c_{1} = c_{2} : κ then Δ_{0} ⊢ c_{1}[τ⃗/Δ′] = c_{2}[τ⃗/Δ′] : κ

4. If Δ′, Δ ⊢ c_{1} ≤ c_{2} : κ then Δ_{0} ⊢ c_{1}[τ⃗/Δ′] ≤ c_{2}[τ⃗/Δ′] : κ

5. If Δ′, Δ ⊢ Δ_{1} = Δ_{2} then Δ_{0} ⊢ Δ_{1}[τ⃗/Δ′] = Δ_{2}[τ⃗/Δ′]

6. If Ψ; Δ′, Δ; Γ; r ⊢ h : τ then Ψ; Δ_{0}; Γ_{0}; r_{0} ⊢ h[τ⃗/Δ′] : τ_{0}

7. If Ψ; Δ′, Δ; Γ ⊢ v : τ then Ψ; Δ_{0}; Γ_{0} ⊢ v[τ⃗/Δ′] : τ_{0} 8. If Ψ; Δ′, Δ; Γ; C ⊢ d ⇒ Δ′, Δ′′; Γ′′; C′′ then

Ψ; Δ_{0}; Γ_{0}; C_{0} ⊢ d[τ⃗/Δ′] ⇒ (Δ′′; Γ′′; C′′)[τ⃗/Δ′].

9. If Ψ; Δ′, Δ; Γ; C ⊢ e then Ψ; Δ_{0}; Γ_{0}; C_{0} ⊢ e[τ⃗/Δ′]

Proof: By induction on the derivations. Almost all cases follow directly from the IH. In part 2, we must prove our lemma for the rules:

Δ′, Δ ⊢ α : κ (Δ′, Δ(α) = κ)  Δ′, Δ ⊢ ϵ : Cap ((ϵ ≤ C) ∈ Δ′, Δ)

In the first case, we have our result by A1 and Type Context Extension. In the second case, assume ϵ is ϵ_{i}. By A2, we have · ⊢ c_{i} ≤ C_{i} : Cap. Because · ⊢ ·, Subtyping Regularity tells us that · ⊢ c_{i} : Cap. By Type Context Extension Δ_{0} ⊢ c_{i} : Cap. In part 4, for the rule:

Δ′, Δ ⊢ ϵ ≤ C : Cap ((ϵ ≤ C) ∈ Δ′, Δ)

our result follows by A2 and Type Context Extension. In part 9, the case for let , we can apply the induction hypothesis because inspection of the rules for declarations show that Ψ; Δ; Γ; C ⊢ d ⇒ Δ, Δ′′; Γ′′; C′ instead of the more general Ψ; Δ; Γ; C ⊢ d ⇒ Δ′′; Γ′′; C′. □ Lemma 25 (Value Substitution) If Γ is {x_{1}:τ_{1}, …, x_{n}:τ_{n}}, · ⊢ Γ and for 1 ≤ i ≤ n, Ψ; ·; · ⊢ v_{i} : τ_{i} then

1. If Ψ; Δ; Γ, Γ′ ⊢ h at r : τ then Ψ; Δ; Γ′ ⊢ h[v_{1}, …, v_{n}/x_{1}, …, x_{n}] at r : τ

2. If Ψ; Δ; Γ, Γ′ ⊢ v : τ then Ψ; Δ; Γ′ ⊢ v[v_{1}, …, v_{n}/x_{1}, …, x_{n}] : τ

3. If Ψ; Δ; Γ, Γ′; C ⊢ d ⇒ Δ′; Γ, Γ′′; C′ then Ψ; Δ; Γ′; C ⊢ d[v_{1}, …, v_{n}/x_{1}, …, x_{n}] ⇒ Δ′; Γ′′; C′

4. If Ψ; Δ; Γ, Γ′; C ⊢ e then Ψ; Δ; Γ′; C ⊢ e[v_{1}, …, v_{n}/x_{1}, …, x_{n}]

Proof: By induction on the typing derivations. In part 4, the case for let , we can use the induction hypothesis because inspection of the typing rules for declarations reveals that Ψ; Δ; Γ; C ⊢ d ⇒ Δ′; Γ, Γ′; C′ instead of the more general Ψ; Δ; Γ; C ⊢ d ⇒ Δ′; Γ′; C′. □ Lemma 26 (Term Judgement Regularity) If A1 ⊢ Ψ A2 · ⊢ C : Cap A3 · ⊢ r : Rgn then

1. If Ψ; ·; · ⊢ v : τ then · ⊢ τ : Type

2. If Ψ; ·; · ⊢ h at r : τ then · ⊢ τ : Type

3. If Ψ; ·; ·; C ⊢ d ⇒ Δ′; Γ′; C′ then · ⊢ Δ′ and Δ′ ⊢ Γ′ and Δ′ ⊢ C′ : Cap

Proof: By induction on the typing derivations. Almost all cases follow directly from the induction hypothesis and Equality Regularity or Subtyping Regularity. In part 1, consider the case for type application:

Ψ; ·; · ⊢ v : ∀[α:κ, Δ].(C′, τ_{1}, …, τ_{n}) → 0at r · ⊢ c : κ
Ψ; ·; · ⊢ v[c] : (∀[Δ].(C′, τ_{1}, …, τ_{n}) → 0)[c/α] at r

By the induction hypothesis, and then inspection of the typing rules for arrow types, we can deduce a judgement of the following form:

{α:κ ⊢ Δ \atop · ⊢ α:κ, Δ} α:κ, Δ ⊢ C′ : Cap α:κ, Δ ⊢ τ_{i} : Type (for 1 ≤ i ≤ n)
· ⊢ ∀[α:κ, Δ].(C′, τ_{1}, …, τ_{n}) → 0at r : Type

By Type Substitution, we may deduce that · ⊢ (∀[Δ′].(C′, τ_{1}, …, τ_{n}) → 0)[c/α] at r. The second type application rule follows similarly. □ Lemma 27 (Canonical Memory Forms) If ⊢ {ν_{1} ↦ R_{1}, …, ν_{n} ↦ R_{n}} : {ν_{1}:Υ_{1} …, ν_{n}:Υ_{n}} then For all 1 ≤ i ≤ n and for all ℓ ∈ Dom(Υ_{i}), either

1. Υ_{i}(ℓ) is ⟨τ_{1}, …, τ_{m}⟩ at ν_{i} and R_{i}(ℓ) = ⟨v_{1}, …, v_{m}⟩ and for 1 ≤ j ≤ m, Ψ; ·; · ⊢ v_{j} : τ_{j} or

2. Υ_{i}(ℓ) is ∀[Δ].(C, τ_{1}, …, τ_{n}) → 0at ν_{i} and R_{i}(ℓ) = fix f[Δ](C, x_{1}:τ_{1}, …, x_{n}:τ_{n}).e and Ψ; Δ; {f:∀[Δ].(C, τ_{1}, …, τ_{n}) → 0at ν_{i}, x_{1}:τ_{1}, …, x_{n}:τ_{n}}; C ⊢ e

Proof: By inspection of the typing judgements for memory, regions, and heap values. Lemma 28 (Canonical Memory Forms II)

1. If ⊢ M : Ψ and ν ∉ M then ν ∉ Ψ

2. If Ψ ⊢ R at ν′ : Υ and ν ∉ R and ν′ is not ν then ν ∉ Υ

3. If Ψ; ·; · ⊢ h at ν′ : τ and ν′ is not ν and ν ∉ h then ν ∉ τ

4. If Ψ; ·; · ⊢ v : τ and ν ∉ v then ν ∉ τ Proof: By induction on the typing derivations. Lemma 29 (Canonical Forms) If ⊢ M : Ψ and Ψ; ·; · ⊢ v : τ then

1. If τ is int then v = i.

2. If τ is ν handle then v = handle(ν).

3. If τ is ∀[Δ].(C, τ_{1}, …, τ_{n}) → 0at ν then (a) v = ν.ℓ[c_{1}, …, c_{m}]

(b) M(ν.ℓ) = fix f[Δ′, Δ′′](C′, x_{1}:τ′_{1}, …, x_{n}:τ′_{n}).e

(c) Δ′ is b_{1}, …, b_{m} and for 0 ≤ i ≤ m, either b_{i} is α_{i}:κ_{i} and · ⊢ c_{i}:κ_{i}, or b_{i} is ϵ_{i} ≤ C_{i} and · ⊢ c_{i} ≤ C_{i} : Cap.

(d) · ⊢ Δ = Δ′′[c_{1}, …, c_{m}/Δ′], and Δ ⊢ C = C′[c_{1}, …, c_{m}/Δ′], and for 1 ≤ i ≤ n, Δ ⊢ τ_{i} = τ′_{i}[c_{1}, …, c_{m}/Δ′] : Type

(e) Ψ; Δ′, Δ′′; {f:∀[Δ′, Δ′′].(C′, τ′_{1}, …, τ′_{n}) → 0at ν, x_{1}:τ′_{1}, …, x_{n}:τ′_{n}}; C′ ⊢ e

or instead of (b),(c),(d), and (e): ν ∉ Ψ.

4. If τ is ⟨τ_{1}, …, τ_{n}⟩ at ν then (a) v = ν.ℓ

(b) M(ν.ℓ) = ⟨v_{1}, …, v_{n}⟩

(c) Ψ; · ⊢ v_{i} : τ_{i}wval

or instead of (b),(c): ν ∉ Ψ.

Proof: Part 1, 2 follow by inspection of the typing rules for word values. Part 3 follows by induction on the derivation, Ψ; ·; · ⊢ v : τ . By Canonical Memory Forms and inspection of the typing rules for word values, either ν.ℓ or one of the type application rules are last:

case ν.ℓ where ν ∉ Ψ:

(a) Trivial. case ν.ℓ where ν ∈ Ψ:

(a) Trivial.

(b) By Canonical Memory Forms where Δ′ is ·, Δ′′ is Δ, C′ is C, and for 1 ≤ i ≤ n, τ′_{i} is τ_{i}.

(c) Trivial.

(d) Trivial.

(e) By inspection of judgement. case v[C]

Ψ; ·; · ⊢ v : ∀[ϵ ≤ C_{a}, Δ].(C_{b}, τ_{1}, …, τ_{n}) → 0at r · ⊢ C ≤ C_{a} : Cap
Ψ; ·; · ⊢ v[C] : (∀[Δ].(C_{b}, τ_{1}, …, τ_{n}) → 0)[C/ϵ] at r

By Term Judgement Regularity and Lemma 13, r is ν. The inductive hypothesis is as follows:

(a) v = ν.ℓ[c_{1}, …, c_{n}]

(b) M(ν.ℓ) = fix f[Δ′, ϵ ≤ C′_{a}, Δ′′](C′_{b}, x_{1}:τ′_{1}, …, x_{n}:τ′_{n}).e

(c) Δ′ is b_{1}, …, b_{m} and for 0 ≤ i ≤ m, either b_{i} is α_{i}:κ_{i} and · ⊢ c_{i}:κ_{i}, or b_{i} is ϵ_{i} ≤ C_{i} and

· ⊢ c_{i} ≤ C_{i} : Cap.

(d) · ⊢ ϵ ≤ C_{a}, Δ = (ϵ ≤ C′_{a}, Δ′′)[c_{1}, …, c_{m}/Δ′]

and ϵ ≤ C_{a}, Δ ⊢ C_{b} = C′_{b}[c_{1}, …, c_{m}/Δ′]
and for 1 ≤ i ≤ n, ϵ ≤ C_{a}, Δ ⊢ τ_{i} = τ′_{i}[c_{1}, …, c_{m}] : Type

(e) Ψ; Δ′, ϵ ≤ C_{a}, Δ′′; Γ; C′_{b} ⊢ e

where Γ = {f:∀[Δ′, ϵ ≤ C_{a}, Δ′′].(C′_{b}, τ′_{1}, …, τ′_{n}) → 0at ν, x_{1}:τ′_{1}, …, x_{n}:τ′_{n}}

or instead of (b),(c),(d), and (e), ν ∉ Ψ. Thus,

(a) v[C] = ν.ℓ[c_{1}, …, c_{n}, C] from IH. If ν ∉ Ψ then the result follows trivially. Thus assume ν ∈ Ψ.

(b) By IH.

(c) By IH and the typing judgement which states · ⊢ C ≤ C_{a} : Cap.

(d) By IH and Type Substitution.

(e) By IH.

case v[c] Similar. Part 4 follows by inspection of the typing rules for word values. Notice only the ν.ℓ rule when ν ∈ Ψ, or the rule for tuples when ν ∉ Ψ can apply. Assuming the former (the latter is trivial), then (a) is immediate and (b), (c) follow by Canonical Memory Forms. □ Lemma 30 (Memory Type GC) If ⊢ Ψ and Ψ′ is Ψ\ν then

1. If Ψ; Δ; Γ ⊢ h at r : τ then Ψ′; Δ; Γ ⊢ h at r : τ

2. If Ψ; Δ; Γ ⊢ v : τ then Ψ′; Δ; Γ ⊢ v : τ

3. If Ψ; Δ; Γ; C ⊢ d ⇒ Δ′; Γ′; C′ then Ψ′; Δ; Γ; C ⊢ d ⇒ Δ′; Γ′; C′

4. If Ψ; Δ; Γ; C ⊢ e then Ψ′; Δ; Γ; C ⊢ e

5. If Ψ ⊢ R at ν : Υ then Ψ′ ⊢ R at ν : Υ

Proof:

By induction on the typing derivation. All cases follow directly from IH except the rule:

Ψ; Δ; Γ ⊢ ν′.ℓ : τ (Ψ(ν′.ℓ) = τ)

When ν is not ν′, this case is trivial so assume ν is ν′. By Canonical Memory Forms, τ is either ∀[Δ′].(ϵ, τ_{1}, …, τ_{n}) → 0at ν or ⟨τ_{1}, …, τ_{n}⟩ at ν. Because ⊢ Ψ, we have · ⊢ τ : Type. By Type Context Extension, Δ ⊢ τ : Type. Thus, in either of the above cases, Ψ; Δ; Γ ⊢ ν′.ℓ : τ via one of the two rules for ν ∉ Dom(Ψ). □ Lemma 31 (Memory Type Extension) If ν does not appear in Ψ, Δ, Γ, r, h, v, d, e, or R, and Ψ′ is Ψ{ν:{ }} then

1. If Ψ; Δ; Γ ⊢ h at r : τ then Ψ′; Δ; Γ ⊢ h at r : τ

2. If Ψ; Δ; Γ ⊢ v : τ then Ψ′; Δ; Γ ⊢ v : τ

3. If Ψ; Δ; Γ; C ⊢ d ⇒ Δ′; Γ′; C′ then Ψ′; Δ; Γ; C ⊢ d ⇒ Δ′; Γ′; C′

4. If Ψ; Δ; Γ; C ⊢ e then Ψ′; Δ; Γ; C ⊢ e

5. If Ψ ⊢ R at ν′ : Υ then Ψ′ ⊢ R at ν′ : Υ Proof: By induction on the typing derivation. In part 2, for the rule:

Δ ⊢ ⟨τ_{1}, …, τ_{n}⟩ at ν′ : Type

Ψ; Δ; Γ ⊢ ν′.ℓ : ⟨τ_{1}, …, τ_{n}⟩ at ν′ (ν′ ∉ Ψ)

ν′ is not ν by assumption and thus the result holds and similarly for the analogous rule for arrow types. □ Lemma 32 (Region Type Extension) If ν ∈ Dom(Ψ), ℓ ∉ Dom(Ψ(ν)), and Ψ′ is Ψ{ν.ℓ:τ} then

1. If Ψ; Δ; Γ ⊢ h at r : τ then Ψ′; Δ; Γ ⊢ h at r : τ

2. If Ψ; Δ; Γ ⊢ v : τ then Ψ′; Δ; Γ ⊢ v : τ

3. If Ψ; Δ; Γ; C ⊢ d ⇒ Δ′; Γ′; C′ then Ψ′; Δ; Γ; C ⊢ d ⇒ Δ′; Γ′; C′

4. If Ψ; Δ; Γ; C ⊢ e then Ψ′; Δ; Γ; C ⊢ e

5. If Ψ ⊢ R at ν′ : Υ then Ψ′ ⊢ R at ν′ : Υ

6. If Ψ ⊢ C sat then Ψ′ ⊢ C sat Proof:

By induction on the typing derivation.

□

Lemma 33 If Δ ⊢ C_{1}⊕C_{2} : Cap and Δ ⊢ C_{1}⊕C_{2} = a_{1}⊕⋯⊕a_{n} : Cap then Δ ⊢ C_{1} = a′_{1}⊕⋯⊕a′_{m} : Cap and a′_{1}, …, a′_{m} is a subset of a_{1}, …, a_{n}.

Proof:

By Lemma 18 (1), Δ ⊢ C_{1} = a′_{1} ⊕ ⋯ ⊕ a′_{m} : Cap. By Lemma 18 (5), E(a′_{1} ⊕ ⋯ ⊕ a′_{m}) = E(C_{1}) ⊆ E(C_{1} ⊕ C_{2}) = E(a_{1} ⊕ ⋯ ⊕ a_{n}). By CECP, a_{i} is unique (duplicatable) in a′_{1} ⊕ ⋯ ⊕ a′_{m} if a_{i} is unique (duplicatable) in a_{1} ⊕ ⋯ ⊕ a_{n}.

□

Lemma 34 (Capability Satisfiability Preservation)

1. If Ψ ⊢ C sat and · ⊢ C = C′ : Cap then Ψ ⊢ C′ sat.

2. If Ψ ⊢ C sat and · ⊢ C ≤ C′ : Cap then Ψ ⊢ C′ sat.

Proof:

1. By symmetry and transitivity of equality and inspection of the sat derivation.

2. By induction on the subtyping derivation.

case equality: From Part 1. case transitivity: By IH. case · ⊢ ϵ ≤ C: Does not apply because the context (·) is empty and therefore, by Lemma 13, the

two capabilities must not contain any free variables. case · ⊢ C ≤ \overline{C}:

1. Assume {ν_{1}:Υ_{1}, …, ν_{n}:Υ_{n}} ⊢ C sat

2. Hence · ⊢ C = {ν_{1}^{φ_{1}}, …, ν_{n}^{φ_{n}}} : Cap

3. and ν_{i} ≠ ν_{j} for 1 ≤ i, j ≤ n and i ≠ j from 1

4. From 2, using rule eq-congruence-bar, · ⊢ \overline{C} = \overline{\{ν_{1}^{φ_{1}}, …, ν_{n}^{φ_{n}}\}} : Cap 5. From 4, by constructor equality rules, · ⊢ \overline{C} = \{ν_{1}^{+}, …, ν_{n}^{+}\} : Cap 6. Hence, from 5,3 we have \{ν_{1}:Υ_{1}, …, ν_{n}:Υ_{n}\} ⊢ \overline{C} sat

case

\begin{matrix}· ⊢ C_{1} ≤ C′_{1} (1) & · ⊢ C_{2} ≤ C′_{2} (2) \\ · ⊢ C_{1} ⊕ C_{2} ≤ C′_{1} ⊕ C′_{2} \end{matrix}

3. Assume {ν_{1}:Υ_{1}, …, ν_{n}:Υ_{n}} ⊢ C_{1} ⊕ C_{2} sat
4. From 3, · ⊢ C_{1} ⊕ C_{2} = {ν_{1}^{φ_{1}}, …, ν_{n}^{φ_{n}}} : Cap

5. and ν_{i} ≠ ν_{j} for 1 ≤ i, j ≤ n and i ≠ j from 1

6. By 4 and Equality Regularity, C_{1},C_{2},C′_{1},C′_{2} are all well-formed under the empty context ·.

7. By 6 and Lemma 18(1), · ⊢ C_{1} = {ν_{1,1}^{φ_{1,1}}, …, ν_{1,n_{1}}^{φ_{1,n_{1}}} } : Cap

8. From 7 and CECP, for 1 ≤ i ≤ n_{1}, ν_{1,i}^{φ_{1,i}} ∈ C_{1}

9. Hence, we have ν_{1,i}^{φ_{1,i}} ∈ C_{1} ⊕ C_{2}

10. and by 4 and CECP again, we can conclude ν_{1,i}^{φ_{1,i}} ∈ {ν_{1}^{φ_{1}}, …, ν_{n}^{φ_{n}}}

11. For 1 ≤ i ≤ n_{1} and i ≠ j, if ν_{1,i} = ν_{1,j} and φ_{1,i} = φ_{1,j} = + then by Lemma 18(4), we can eliminate the duplicates and assume without loss of generality that {ν_{1,1}^{φ_{1,1}}, …, ν_{1,n_{1}}^{φ_{1,n_{1}}} } does not contain duplicates of this form.

12. For some 1 ≤ i ≤ n_{1} and i ≠ j, assume (anticipating a contradiction) that ν_{1,i} = ν_{1,j} and one of φ_{1,i} or φ_{1,j} is 1 then by CECP, {ν_{1,i}^{φ_{1,i}}} and {ν_{1,j}^{φ_{1,j}}} both appear in C_{1}

13. From 12, we have {ν_{1,i}^{φ_{1,i}}} and {ν_{1,j}^{φ_{1,j}}} both appear in C_{1} ⊕ C_{2}

14. and from 13, and CECP, {ν_{1,i}^{φ_{1,i}}} and {ν_{1,j}^{φ_{1,j}}} both appear in {ν_{1}^{φ_{1}}, …, ν_{n}^{φ_{n}}}

15. However, 14 and 12 (ν_{1,i} = ν_{1,j}) contradict 5, indicating our assumption 12 was false 16. By 15 and 11, we may assume without loss of generality that for 1 ≤ i ≤ n_{1} and i ≠ j, ν_{1,i} ≠ ν_{1,j}

17. By 7, 11, and 16, we can conclude Ψ_{1} ⊢ C_{1} sat where Ψ_{1} is Ψ with domain restricted to {ν_{1,1} …, ν_{1,n_{1}}}

18. Analogous reasoning and definitions for Ψ_{2} yields Ψ_{2} ⊢ C_{2} sat

19. From 17 and 1, using the inductive hypothesis, we have Ψ_{1} ⊢ C′_{1} sat

20. From 18 and 2, using the inductive hypothesis, we have Ψ_{2} ⊢ C′_{2} sat

21. From 19 (20) and inspection of the sat judgement, we know · ⊢ C′_{1} = {ν_{1′,1}^{φ_{1′,1}}, …, ν_{1′,n′_{1}}^{φ_{1′,n′_{1}}} } :

Cap for some ν_{1′,1}^{φ_{1′,1}}, …, ν_{1′,n′_{1}}^{φ_{1′,n′_{1}}} (and we know · ⊢ C′_{2} = {ν_{2′,1}^{φ_{2′,1}}, …, ν_{2′,n′_{1}}^{φ_{2′,n′_{1}}} } : Cap for some

{ν_{2′,1}^{φ_{2′,1}}, …, ν_{2′,n′_{1}}^{φ_{2′,n′_{1}}} })

22. Now, by CSCP, 19 (20), and 1, we have that for 1 ≤ i ≤ n′_{1}, {ν_{1′,i}^{φ_{1′,i}}} ∈ C_{1} (and that for 1 ≤ i ≤ n′_{2}, {ν_{2′,i}^{φ_{2′,i}}} ∈ C_{2})

23. Consequently, from 22 using CECP, ν_{1′,1}, …, ν_{1′,n′_{1}} ∈ {ν_{1}, … ν_{n}} and similarly ν_{2′,1}, …, ν_{2′,n′_{2}} ∈ {ν_{1}, … ν_{n}}.

24. Conversely, also by CECP, ν_{1}, …, ν_{n} ∈ {ν_{1′,1}, …, ν_{1′,n′_{1}}, ν_{2′,1}, …, ν_{2′,n′_{2}}}

25. To summarize, 23 and 24 state that region names {ν_{1′,1}^{φ_{1′,1}}, …, ν_{1′,n′_{1}}^{φ_{1′,n′_{1}}} , ν_{2′,1}^{φ_{2′,1}}, …, ν_{2′,n′_{1}}^{φ_{2′,n′_{1}}} } are an exact cover of {ν_{1}, …, ν_{n}}

26. Now, reasoning analogously to steps 12 through 16, we can deduce that {ν_{1′,1}^{φ_{1′,1}}, …, ν_{1′,n′_{1}}^{φ_{1′,n′_{1}}} , ν_{2′,1}^{φ_{2′,1}}, …, ν_{2′,n′_{1}}^{φ_{2′,n′_{1}}} } contains no duplicate region names aside from those which both have multiplicity flag +.

27. By 21 and rule eq-congruence-plus, we have · ⊢ C′_{1} ⊕ C′_{2} = {ν_{1′,1}^{φ_{1′,1}}, …, ν_{1′,n′_{1}}^{φ_{1′,n′_{1}}} } ⊕

{ν_{2′,1}^{φ_{2′,1}}, …, ν_{2′,n′_{1}}^{φ_{2′,n′_{1}}} } : Cap

28. By Lemma 18(4) we may eliminate duplicate region names with flag + on the right-hand side of equation 27.

29. By Lemma 18(3), we can reorder the elements of the right-hand side of 28 which by 25

and 26 are exactly {ν_{1}, …, ν_{n}} giving us · ⊢ C′_{1} ⊕ C′_{2} = {ν_{1}^{φ′_{1}}, …, ν_{n}^{φ′_{n}}} : Cap
32. Consequently, we have {ν_{1}, …, ν_{n}} ⊢ C′_{1} ⊕ C′_{2} sat

□

Lemma 35 If Ψ ⊢ C ⊕ {ν} sat then Ψ\ν ⊢ C sat.

Proof:

1. Assume Ψ ⊢ C ⊕ {ν} sat

2. and Ψ = {ν_{1}:Υ_{1}, …, ν_{n}:Υ_{n}}

3. From 1, we know · ⊢ C ⊕ {ν} = {ν_{1}^{φ_{1}}, …, ν_{n}^{φ_{n}}} : Cap

4. and ν_{i} ≠ ν_{j}, for 1 ≤ i, j ≤ n and i ≠ j

5. From 3, 4, and CECP, ν appears once in {ν_{1}^{φ_{1}}, …, ν_{n}^{φ_{n}}} and once in C ⊕ {ν}.

6. From 5, and Equality (3), · ⊢ {ν_{1}^{φ_{1}}, …, ν_{i−1}^{φ_{i−1}}, ν^{1}, ν_{i+1}^{φ_{i+1}}, …, ν_{n}^{φ_{n}}} = {ν_{1}^{φ_{1}}, …, ν_{i−1}^{φ_{i−1}}, ν_{i+1}^{φ_{i+1}}, …, ν_{n}^{φ_{n}}} ⊕ {ν} : Cap

7. From 3, 6, transitivity of equality, and Equality (7), · ⊢ C = {ν_{1}^{φ_{1}}, …, ν_{i−1}^{φ_{i−1}}, ν_{i+1}^{φ_{i+1}}, …, ν_{n}^{φ_{n}}} : Cap

8. Hence, from 2,4,7 we have Ψ\ν ⊢ C sat

□

Lemma 36 (Preservation) If ⊢ (M, e) and (M, e) ⟼ (M′, e′) then ⊢ (M′, e′)

Proof:

The proof proceeds by cases on the structure of e. In each case, we show the form of the typing judgement that can be inferred by inspection of the typing rules and refer to it throughout the case as “the typing judgement”. Then we give the transition specified by the operational semantics. Using these two facts, we derive the result ⊢ (M′, e′).

  • let v

⊢ M : Ψ Ψ ⊢ C sat

{Ψ; ·; · ⊢ v : τ \atop Ψ; ·; ·; C ⊢ x = v ⇒ ·; \{x:τ\}; C} Ψ; ·; \{x:τ\}; C ⊢ e
Ψ; ·; ·; C ⊢ let x = v in e
⊢ (M, let x = v in e)

and (M, let x = v in e) ⟼ (M, e[v/x]). By the typing judgement and Value Substitution, ⊢ (M, e[v/x]).

  • let h

⊢ M : Ψ Ψ ⊢ C sat

Ψ; ·; · ⊢ v : ν handle
Ψ; ·; · ⊢ h at ν : τ · ⊢ C ≤ C′ ⊕ \overline{\{ν\}}
Ψ; ·; ·; C ⊢ x = h at v ⇒ ·; {x:τ}; C

⋮ ; Ψ; ·; {x:τ}; C ⊢ e

Ψ; ·; ·; C ⊢ let x = h at v in e

⊢ (M, let x = h at v in e)

where v = handle(ν) and ν ∈ Dom(M) and ℓ ∉ Dom(M(ν)) and M′ = M{ν.ℓ ↦ h} and (M, let x = h at v in e) ⟼ (M′, e[ν.ℓ/x]) and let Ψ′ = Ψ{ν.ℓ:τ}

1. (a) τ is ⟨τ_{1}, …, τ_{n}⟩ at ν or ∀[ ].(C′′, τ_{1}, …, τ_{n}) → 0at ν by inspection of the heap value typing

rules and the typing judgement.

(b) ⊢ M′ : Ψ′ by the typing judgement and inspection of the memory typing rule.

2. Ψ′ ⊢ C sat by Region Type Extension.

3. (a) Ψ′; ·; · ⊢ ν.ℓ : τ by the typing rules for word values.

(b) Ψ′; ·; {}; C ⊢ e[ν.ℓ/x] by (a) and Value Substitution. By 1(b), 2, and 3(b), we have ⊢ (M′, e[ν.ℓ/x]).

• π_{i}v

⊢ M : Ψ Ψ ⊢ C sat

\begin{matrix}Ψ; ·; · ⊢ v : ⟨τ_{1}, …, τ_{n}⟩ at ν \\ · ⊢ C ≤ C′ ⊕ \overline{\{ν\}} \end{matrix} ; Ψ; ·; ·; C ⊢ x = π_{i}v ⇒ ·; \{x:τ_{i}\}; C Ψ; ·; \{x:τ_{i}\}; C ⊢ e
Ψ; ·; ·; C ⊢ let x = π_{i}v in e
⊢ (M, let x = π_{i}v in e)

where v = ν.ℓ and M(ν.ℓ) = ⟨v_{0}, …, v_{n}⟩ and (M, let x = π_{i}v in e) ⟼ (M, e[v_{i}/x])

1. ⊢ M : Ψ by the typing judgement.

2. Ψ ⊢ C sat by the typing judgement.

3. (a) Ψ; ·; · ⊢ v_{i} : τ_{i} by Canonical Forms and the typing judgement.

(b) Ψ; ·; · C ⊢ e[v_{i}/x] by Value Substitution, (a), and the typing judgement. By 1,2,and 3(b), ⊢ (M, e[v_{i}/x]).

• freergn

⊢ M : Ψ Ψ ⊢ C sat

Ψ; ·; · ⊢ v : ν handle · ⊢ C ≤ C′ ⊕ {ν}
Ψ; ·; ·; C ⊢ freergn v ⇒ ·; ·; C′ Ψ; ·; ·; C′ ⊢ e
Ψ; ·; ·; C ⊢ freergn v in e

                           ⊢ (M, freergn v in e)

where v is handle(ν) and (M, freergn v in e) ⟼ (M\ν, e). Let Ψ′ be Ψ\ν.

1. ⊢ M′ : Ψ′ by Memory Type GC and the typing judgement.

2. (a) Ψ ⊢ C sat and · ⊢ C ≤ C′ ⊕ {ν} by the typing judgement.

(b) Ψ ⊢ C′ ⊕ {ν} sat by Capability Satisfiability Preservation and (a)

(c) Ψ′ ⊢ C′ sat by Lemma 35 and (b)

3. Ψ′; ·; ·; C′ ⊢ e by the typing judgement and Memory Type GC. By 1, 2(e), and 3, ⊢ (M\ν, e).

• newrgn

⊢ M : Ψ {· ⊢ C = C′ : Cap \atop Ψ ⊢ C sat} (...)

(A) (B)
Ψ; ·; ·; C ⊢ newrgn ρ, x_{ρ} in e
⊢ (M, newrgn ρ, x_{ρ} in e)
Ψ; ·; ·; C ⊢ newrgn ρ, x_{ρ} ⇒ ρ:Rgn; {x_{ρ}:ρ handle}; C ⊕ {ρ} (A)

⋮
Ψ; ρ:Rgn; {x_{ρ}:ρ handle}; C ⊕ {ρ} ⊢ e

(B)

The operational rule is

(M, newrgn ρ, x_{ρ} in e) ⟼ (M′, e′[ν, handle(ν)/ρ, x_{ρ}])

where M′ = M{ν ↦ { }} and ν ∉ M and ν ∉ e. In what follows, let Ψ′ = Ψ{ν:{ }}.

1. ⊢ Ψ′ by Memory Type Extension and the typing judgement.

2. Since ν ∉ Ψ by assumption in the operational semantics, we can satisfy the side condition on the sat judgement. We can also prove · ⊢ C ⊕ {ν} = C′ ⊕ {ν} : Cap by the congruence rule for equality. Consequently, Ψ′ ⊢ C ⊕ {ν} sat.

3. Ψ′; ·; ·; C ⊕{ν} ⊢ e[ν, handle(ν)/ρ, x_{ρ}] from the typing judgement and application of Type and Value Substitution and then Memory Type Extension Lemmas.

By 1, 2(e), and 3, ⊢ (M′, e[ν, handle(ν)/ρ, x_{ρ}]).

• if0

⊢ M : Ψ Ψ ⊢ C sat

Ψ; ·; · ⊢ i : int Ψ; ·; ·; C ⊢ e_{2} Ψ; ·; ·; C ⊢ e_{3}
Ψ; ·; ·; C ⊢ if0 i then e_{2} else e_{3}

                          ⊢ (M, if0 i then e_{2} else e_{3})

(M, e) ⟼ (M, e_{2}) if i = 0 and (M, e) ⟼ (M, e_{3}) otherwise. By the typing judgement, ⊢ (M, e_{2}), or ⊢ (M, e_{3}).

• v_{0}(v_{1}, …, v_{n})

⊢ M : Ψ Ψ ⊢ C sat

Ψ; ·; · ⊢ v_{i} : τ_{i} (for 0 ≤ i ≤ n) · ⊢ C ≤ C′′ ⊕ \overline{\{ν\}} : Cap · ⊢ τ_{0} = ∀[ ].(C′, τ_{1}, …, τ_{n}) → 0at ν

· ⊢ C ≤ C′ : Cap

Ψ; ·; ·; C ⊢ v_{0}(v_{1}, …, v_{n})

⊢ (M, v_{0}(v_{1}, …, v_{n}))

(M, v_{0}(v_{1}, …, v_{n})) ⟼ (M, S(e)) where w = ν.ℓ[c_{1}, …, c_{m}] and M(ν.ℓ) = fix f[b_{1}, …, b_{m}](C′′, x_{1} : τ_{1}, …, x_{n}:τ_{n}).e and for 1 ≤ i ≤ m, b_{i} = α_{i}:κ_{i} or b_{i} = α_{i} ≤ C_{i} and S = [c_{1}, …, c_{m}, ν.ℓ, v_{1}, …, v_{n}/α_{1}, …, α_{m}, f, x_{1}, …, x_{n}]

1. ⊢ M : Ψ by the typing judgement.

2. Ψ ⊢ C′ sat by Capability Satisfiability Preservation.

3. (a) Ψ ⊢ C′′ ⊕ \overline{\{ν\}} sat by Capability Satisfiability Preservation and the typing judgement (b) ν ∈ Dom(Ψ) by CECP and (a).

(c) Ψ; ·; · ⊢ v_{0} : ∀[ ].(C′′′, τ′′′_{1}, …, τ′′′_{n}) → 0 and · ⊢ ∀[ ].(C′′′, τ′′′_{1}, …, τ′′′_{n}) → 0 = ∀[ ].(C′, τ_{1}, …, τ_{n}) → 0 by the typing judgement

(d) Ψ; b_{1}, …, b_{m}; {x_{1}:τ_{1}, …, x_{n}:τ_{n}}; C′′ ⊢ e by Canonical Forms 3(e), (b), and (c).

(e) · ⊢ C′ = C′′[c_{1}, …, c_{m}/α_{1}, …, α_{m}] : Cap by the transitivity of equality, Canonical Forms 3(d), (b), and (c)

(f) Ψ; ·; ·; C′ ⊢ S(e) by Type and Value Substitution, and (e).

By 1, 2, and 3(f), ⊢ (M, S(e))

□

Lemma 37 (Progress) If ⊢ (M, e) then either:

1. There exists (M′, e′) such that (M, e) ⟼ (M′, e′), or

2. e = halt v and Ψ; ·; · ⊢ v : int.

Proof:

The proof proceeds by cases on the structure of e and makes heavy use of the Canonical Forms lemma.

• let v Trivial.

• let h

⊢ M : Ψ Ψ ⊢ C sat

Ψ; ·; · ⊢ v : r handle
Ψ; ·; · ⊢ h at r : τ
· ⊢ C ≤ C′ ⊕ \overline{\{r\}}

Ψ; ·; ·; C ⊢ x = h at v ⇒ ·; {x:τ}; C ⋯

Ψ; ·; ·; C ⊢ let x = h at v in e

⊢ (M, let x = h at v in e)

Ψ; ·; · ⊢ v : r handle directly from the typing judgement. By Term Judgement Regularity and Lemma 13, r is ν, and by Canonical Forms, v is handle(ν). By Capability Satisfiability Preservation, Ψ ⊢ C′ ⊕ \overline{\{ν\}} sat and thus ν ∈ Dom(Ψ). By inspection of the memory typing rules, ν ∈ Dom(M). Thus (M, e) ⟼ (M{ν.ℓ ↦ h}, e[ν.ℓ/x]).

• π_{i}v

⊢ M : Ψ Ψ ⊢ C sat

\begin{matrix}Ψ; ·; · ⊢ v : ⟨τ_{1}, …, τ_{n}⟩ at r & · ⊢ C ≤ C′ ⊕ \overline{\{r\}} \\ Ψ; ·; ·; C ⊢ x = π_{i}v ⇒ ·; \{x:τ_{i}\}; C \end{matrix} ⋯
Ψ; ·; ·; C ⊢ let x = π_{i}v in e
⊢ (M, let x = π_{i}v in e)

By Capability Satisfiability Preservation, Ψ ⊢ C′ ⊕ \overline{\{ν\}} sat. By CECP, ν ∈ Dom(Ψ) and by Canonical Forms, M(ν.ℓ) = ⟨v_{1}, …, v_{n}⟩. By the typing judgement, 0 ≤ i ≤ n − 1. Thus (M, let x = π_{i}v in e) ⟼ (M, e[v_{i}/x]).

• newrgn Trivial.

• freergn

⊢ M : Ψ Ψ ⊢ C sat

Ψ; ·; · ⊢ v : r handle · ⊢ C ≤ C′ ⊕ {r} : Cap

Ψ; ·; ·; C ⊢ freergn v ⇒ ·; ·; C′ ⋯

Ψ; ·; ·; C ⊢ freergn v in e

                            ⊢ (M, freergn v in e)

By Term Judgement Regularity and Lemma 13, r is ν, and by Canonical Forms, v is handle(ν). By Capability Satisfiability Preservation, Ψ ⊢ C ⊕ {ν} sat. Thus, by CECP, ν ∈ Dom(Ψ), and by inspection of the memory typing rules, ν ∈ Dom(M). Consequently, (M, freergn v in e) ⟼ (M\ν, e).

• if0

Ψ; Δ; Γ ⊢ v : int
Ψ; Δ; Γ; C ⊢ e_{2} Ψ; Δ; Γ; C ⊢ e_{3}
Ψ; Δ; Γ; C ⊢ if0 v then e_{2} else e_{3}

By Canonical Forms, v must be integer. Therefore, one of the two operational rules for if0 applies.

• v_{0}(v_{1}, …, v_{n})

⊢ M : Ψ Ψ ⊢ C sat

Ψ; ·; · ⊢ v_{i} : τ_{i} (for 0 ≤ i ≤ n)
· ⊢ C ≤ C′′ ⊕ \overline{\{r\}} : Cap
· ⊢ τ_{0} = ∀[ ].(C′, τ_{1}, …, τ_{n}) → 0at r
· ⊢ C ≤ C′ : Cap
Ψ; ·; ·; C ⊢ v_{0}(v_{1}, …, v_{n})
⊢ (M, v_{0}(v_{1}, …, v_{n}))

By Subtyping Regularity and Lemma 13, r is ν. By Capability Satisfiability Preservation, Ψ ⊢ C′′ ⊕ \overline{\{ν\}} sat, and by CECP, ν ∈ Dom(Ψ). Thus, by Canonical Forms, v = ν.ℓ[c_{1}, …, c_{m}], M(ν.ℓ) = fix f[b_{1}, …, b_{m}](C, x_{1}:τ_{1}, …, x_{n}:τ_{n}).e and for 1 ≤ i ≤ n, b_{i} = α_{i}:κ_{i} or b_{i} = α_{i} ≤ C_{i}. If S is [c_{1}, …, c_{m}, ν.ℓ, v_{1}, …, v_{n}/α_{1}, …, α_{m}, f, x_{1}, …, x_{n}] then (M, v_{0}(v_{1}, …, v_{n})) ⟼ (M, S(e))

  • halt

⊢ M : Ψ Ψ ⊢ C sat

Ψ; ·; · ⊢ v : int · ⊢ C = ∅ : Cap

Ψ; ·; ·; C ⊢ halt v

⊢ (M, halt v)

Part 2 holds by inspection of the typing judgement.

□

Definition 38 (Stuck State) An abstract machine state (M, e) is stuck if e is not halt v and there does not exist (M′, e′) such that (M, e) ⟼ (M′, e′).

Theorem 39 (Type Soundness) If ⊢ (M, e) and (M, e) ⟼^{∗} (M′, e′) then (M′, e′) is not stuck.

Proof:

By induction on the number of steps taken in the operational semantics and Preservation, if ⊢ (M, e) and (M, e) ⟼^{∗} (M′, e′) then ⊢ (M′, e′). By Progress, no well-typed state (M′, e′) is stuck: either e′ is halt v or (M′, e′) ⟼ (M′′, e′′).

□

Theorem 40 (Complete Collection) If ⊢ (M, e) then either (M, e) ⇑ or (M, e) ⟼^{∗} (M′, halt v) and M′ = { }.

Proof:

Assume ⊢ (M, e) and (M, e) ⟼^{∗} (M′, e′) and there is no (M′′, e′′) such that (M′, e′) ⟼ (M′′, e′′). By Preservation and Progress, e′ = halt v and

⊢ M′ : Ψ Ψ ⊢ C sat

Ψ; ·; · ⊢ v : int · ⊢ C = ∅ : Cap
Ψ; ·; ·; C ⊢ halt v
⊢ (M′, halt v)

By CECP and the sat judgement, ν ∈ Dom(Ψ) if and only if ν ∈ ∅. Consequently, Ψ = { }. By inspection of the judgement for memory types, M′ = { }.

□

B Region Translation Type Preservation

In this section, we prove our translation of the region calculus into the Capability Calculus is type preserving. In other words, given a well-formed source language term, the result of the translation is a well-formed Capability Calculus term. Section 3 describes the syntax and static semantics of the term constructs.

Notation In this proof, we use several abbreviations and conventions. Equality and subtyping judgements for capabilities are written in the form:

Δ ⊢ C_{1} = C_{2}
≤ C_{3}
= C_{4}
= ⋯

Transitivity rules link each of the equations together. We use associativity and commutativity rules without mentioning them and we will substitute a subcomponent of a capability for an equal capability without mentioning the use of the congruence rules.

We use the notation Δ ⊢_{R} Γ to indicate that all the types in Γ are well-formed under type context Δ. Formally:

Δ ⊢_{R} ·  Δ ⊢_{R} Γ Δ ⊢_{R} τ : Type Δ ⊢_{R} Γ, x:τ (x ∉ Dom(Γ))

Overview The theorem borrows several lemmas from the proof of soundness including lemmas for manipulating capabilities (Lemma 18) and asserting well-formedness (Lemma 14). We also require a number of suplementary lemmas:

• Lemmas 41 and 42 describe additional well-formedness constraints on the types and effects that appear in region calculus judgements.

• Lemmas 43, 44, and 45 state that well-formedness of constructors, constructor equality, and substitution is preserved across the translation.

• Lemma 48 describes the way the subset relation is preserved during the translation of effects (sets) to capabilities (not sets). This lemma makes use of Lemmas 46 and 47 in its proof.

• Lemma 49 is a miscellaneous lemma required in the proof of the letregion construct.

• Lemma 50 gives the conditions under which the static application of a continuation closure to its arguments (i.e. A(k, v)) is well-formed.

Lemma 41

1. If Δ ⊢_{R} c_{1} = c_{2} : κ then Δ ⊢_{R} c_{1} : κ and Δ ⊢_{R} c_{2} : κ.

2. If Δ ⊢_{R} ψ_{1} ⊆ ψ_{2} then Δ ⊢_{R} ψ_{1} : Eff and Δ ⊢_{R} ψ_{2} : Eff

Proof: By induction on the derivations.

Lemma 42 If Δ ⊢_{R} Γ and Δ; Γ ⊢_{R} e : τ, ψ then Δ ⊢_{R} τ : Type and Δ ⊢_{R} ψ : Eff

Proof: By induction on the derivation Δ; Γ ⊢_{R} e : τ, ψ.

Lemma 43 (Well-Formedness Preservation)

1. If Δ ⊢_{R} Δ′ then K[[Δ]] ⊢ K[[Δ′]]

2. If Δ ⊢_{R} c : κ then K[[Δ]] ⊢ T [[c]] : K[[κ]] Proof: By induction on the derivations. Lemma 44 (Equality Preservation)

1. If Δ ⊢_{R} ψ = ψ′ : Eff then K[[Δ]] ⊢ \overline{T [[ψ]]} = \overline{T [[ψ′]]} : Cap

2. If Δ ⊢_{R} c = c′ : κ and κ ≠ Eff then K[[Δ]] ⊢ T [[c]] = T [[c′]] : Cap Proof: By induction on the equality derivations. Lemma 45 (Substitution Preservation) If Δ, α:κ ⊢_{R} τ : Type and Δ ⊢_{R} c : κ then K[[Δ]] ⊢ T [[τ[c/α]]] = T [[τ]][T [[c]]/α]. Proof: By induction on the typing derivation. Lemma 46 If Δ ⊢ ψ = ψ′ : Eff then E(T [[ψ]]) = E(T [[ψ′]]). Proof: By induction on the derivation. Lemma 47 If Δ ⊢ ψ ⊆ ψ′ then E(T [[ψ]]) ⊆ E(T [[ψ′]]). Proof: By inspection of the sub-effecting rule, Δ ⊢ ψ ∪ ψ′′ = ψ′ : Eff for some effect ψ′′. By Lemma 46, E(T [[ψ ∪ ψ′′]]) = E(T [[ψ′]]). By definition of E and the type translation, we have E(T [[ψ]]) ∪ E(T [[ψ′′]]) = E(T [[ψ′]]). Hence, E(T [[ψ]]) ⊆ E(T [[ψ′]]). Lemma 48 If Δ ⊢ ψ ⊆ ψ′ and Δ ⊢ \overline{C} = \overline{C ⊕ T [[ψ′]]} : Cap then Δ ⊢ \overline{C} = \overline{C ⊕ T [[ψ]]} : Cap. Proof:

1. By Δ ⊢ \overline{C} = \overline{C ⊕ T [[ψ′]]} : Cap and Equality (5), E(C) = E(C ⊕ T [[ψ′]]).

2. Thus, by definition of E, E(T [[ψ′]]) ⊆ E(C).

3. By Δ ⊢ ψ ⊆ ψ′ and Lemma 47, E(T [[ψ]]) ⊆ E(T [[ψ′]]).

4. By 2 and 3, E(T [[ψ]]) ⊆ E(C).

5. Hence, by definition of E, E(C) = E(C ⊕ T [[ψ]]).

6. By 5 and Equality (6), Δ ⊢ \overline{C} = \overline{C ⊕ T [[ψ]]} : Cap. □ Lemma 49 If Δ ⊢_{R} ψ then K[[Δ]] ⊢ \overline{T [[ψ\\{ρ\}]] ⊕ \{ρ^{1}\}} = \overline{T [[ψ]] ⊕ \{ρ^{1}\}} : Cap Proof: The proof is by induction on the structure of ψ.

• ψ = ∅. By definition, T [[∅\{ρ}]] = ∅. The result follow immediately from the reflexivity of equality.

• ψ = ϵ or ψ = {ρ′} and ρ ≠ ρ′. Similar.

• ψ = {ρ}. The following reasoning provides the result:

K[[Δ]] ⊢ \overline{T [[\{ρ\}\\{ρ\}]] ⊕ \{ρ^{1}\}} = \overline{∅ ⊕ \{ρ^{1}\}}  (By definition)
= \overline{\{ρ^{1}\}}  (By rule eq-∅)
= \overline{\{ρ^{1}\} ⊕ \{ρ^{1}\}} (By rule eq-dup)

• ψ = ψ_{1} ∪ ψ_{2}. By induction, we know that (1) K[[Δ]] ⊢ \overline{T [[ψ_{i}\\{ρ\}]] ⊕ \{ρ^{1}\}} = \overline{T [[ψ_{i}]] ⊕ \{ρ^{1}\}} for i = 1, 2. Now, the following reasoning provides the result:

K[[Δ]] ⊢ \overline{T [[(ψ_{1} ∪ ψ_{2})\\{ρ\}]] ⊕ \{ρ^{1}\}} = \overline{T [[ψ_{1}\\{ρ\}]] ⊕ T [[(ψ_{2}\\{ρ\})]] ⊕ \{ρ^{1}\}}  (By def.)
= \overline{T [[ψ_{1}\\{ρ\}]] ⊕ T [[(ψ_{2}\\{ρ\})]] ⊕ \{ρ^{1}\} ⊕ \{ρ^{1}\}} (By eq-dup)
= \overline{T [[ψ_{1}\\{ρ\}]] ⊕ \{ρ^{1}\} ⊕ T [[(ψ_{2}\\{ρ\})]] ⊕ \{ρ^{1}\}} (By *)
= \overline{T [[ψ_{1}]] ⊕ \{ρ^{1}\} ⊕ T [[ψ_{2}]] ⊕ \{ρ^{1}\}}  (By 1)
= \overline{T [[ψ_{1}]] ⊕ T [[ψ_{2}]] ⊕ \{ρ^{1}\} ⊕ \{ρ^{1}\}}  (By *)
= \overline{T [[ψ_{1}]] ⊕ T [[ψ_{2}]] ⊕ \{ρ^{1}\}}  (By eq-dup)

where * is rule eq-comm. □ Lemma 50 Let k = ⟨x^{k}; e^{k}⟩. If Ψ; Δ; Γ, x^{k}:τ; C ⊢ e^{k} and Ψ; Δ; Γ ⊢ v : τ then Ψ; Δ; Γ; C ⊢ A(k, v). Proof: The term A(k, v) is defined to be let x^{k} = v in e^{k}. The following derivation proves the lemma:

Ψ; Δ; Γ ⊢ v : τ Ψ; Δ; Γ, x^{k}:τ; C ⊢ e^{k}
Ψ; Δ; Γ; C ⊢ let x^{k} = v in e^{k}

□ Lemma 51 If { }; Δ; Γ, x:τ; C ⊢ e and Δ ⊢ τ = τ′ : Type then { }; Δ; Γ, x:τ′; C ⊢ e. Proof: The proof is by induction on the typing derivation for expressions. □ Theorem 52 (CPS Type Preservation) If ·; · ⊢ e : int, ∅ then { }; ·; ·; ∅ ⊢ C_{·;·;Θ}(e)⟨x; halt x⟩ where x is fresh and Θ is the empty environment, ⟨·; ·; ∅; ∅⟩.

Proof:

The proof is by induction on the typing derivation of the expression using the following inductive hypothesis:

Given Δ, Γ, Θ, e, and k where Θ = ⟨Δ^{Θ}; Γ^{Θ}; C^{Θ}; B^{Θ}⟩ and k = ⟨x^{k}; e^{k}⟩. If:

A. Δ; Γ ⊢_{R} e : τ, ψ

B. { }; K[[Δ]], Δ^{Θ}; S[[Γ]], Γ^{Θ}, x^{k}:T [[τ]]; C^{Θ} ⊢ e^{k}

C. K[[Δ]], Δ^{Θ} ⊢ C^{Θ} ≤ \overline{B^{Θ}}

D. K[[Δ]], Δ^{Θ} ⊢ \overline{B^{Θ}} = \overline{B^{Θ} ⊕ T [[ψ]]}

Then:

E. { }; K[[Δ]], Δ^{Θ}; S[[Γ]], Γ^{Θ}; C^{Θ} ⊢ C_{Δ;Γ;Θ}(e)k

In this proof, we will use several abbreviations and conventions in order to make the derivations so that we can focus on the important elements in the proof. First, we will often use the meta-variable Φ to range over type-checking contexts of the form Ψ; Δ; Γ or Ψ; Δ; Γ; C.

We also abbreviate derivations involving let. A derivation:

\begin{matrix}D_{1} & ⋯ & D_{n} \\ Ψ; Δ; Γ; C ⊢ d ⇒ Δ′; Γ′; C′ \end{matrix} Ψ; Δ′; Γ′; C′ ⊢ e

Ψ; Δ; Γ; C ⊢ let d in e

is abbreviated by:

D_{1} ⋯ D_{n} Ψ; Δ′; Γ′; C′ ⊢ e

Ψ; Δ; Γ; C ⊢ let d in e

Many of the typing rules contain the side condition that a Capability Calculus variable ρ, ϵ, or x not be contained in the context Δ or Γ for that judgement. We have assumed that all the variables in the translated term have been generated fresh so that this will be the case. For the sake of brevity, we do not mention this side condition each time it occurs in the proof. Many of the rules also contain well-formedness constraints on types or capabilities (ie: Δ ⊢ τ or Δ ⊢ C). These well-formedness constraints always follow directly from the source typing judgement and Lemma 43. However, in order to concentrate on the more important aspects of the proof, we do not mention these conditions each time they appear in a derivation.

In the following, we prove the result for the more difficult cases: letrec, type application, value application, letregion , and equality. The other cases follow a similar, but simpler pattern.

• The case for letrec. The translation is:

C_{Δ;Γ;Θ}(letrecf[Δ′](x) : σ at e_{1} = e_{2} in e_{3})k = C_{Δ;Γ;Θ}(e_{1})⟨x_{1}; let f = (fix f[K[[Δ′]], Δ′′](ϵ′, x:T [[τ_{1}]], x_{cont}:τ_{cont}).

C_{ΔΔ′;Γ{f:σ,x:τ_{1}};Θ′}(e_{2})⟨x_{2}; x_{cont}(x_{2})⟩) at x_{1}

in C_{Δ;Γ{f:σ};Θ}(e_{3})k⟩

where

σ  = ∀[Δ′].τ_{1} →^{ψ_{f}} τ_{2} at r
τ_{cont} = ∀[ ].(ϵ′, T [[τ_{2}]]) → 0at ρ
B^{Θ′} = ϵ ⊕ T [[ψ_{f}]] ⊕ {ρ^{1}}
Δ′′ = ρ:Rgn, ϵ:Cap, ϵ′ ≤ \overline{B^{Θ′}}
Δ^{Θ′} = Δ^{Θ}, Δ′′
Γ^{Θ′} = Γ^{Θ}, x_{1}:r handle, x_{cont}:τ_{cont}
C^{Θ′} = ϵ′
Θ′  = ⟨Δ^{Θ′}; Γ^{Θ′}; C^{Θ′}; B^{Θ′}⟩

The source typing derivation A:

(A_{1}) Δ; Γ ⊢_{R} e_{1} : r handle, ψ_{1} (A_{2}) ΔΔ′; Γ{f:σ, x:τ_{1}} ⊢_{R} e_{2} : τ_{2}, ψ_{f}

(A_{3}) Δ; Γ{f:σ} ⊢_{R} e_{3} : τ_{3}, ψ_{3}

Δ; Γ ⊢_{R} letrecf[Δ′](x) : σ at e_{1} = e_{2} in e_{3} : τ_{3}, ψ_{1} ∪ ψ_{3} ∪ {r}

(x, f ∉ Dom(Γ))

In order to make the derivations for this case more manageable, we will use the following abbreviations:

Φ_{1} = { }; K[[Δ]], Δ^{Θ}; S[[Γ]], Γ^{Θ}, x_{1}:r handle; C^{Θ}
Φ_{2} = { }; K[[Δ, Δ′]], Δ^{Θ′}; S[[Γ, f:σ, x:τ_{1}]], Γ^{Θ′}, x_{1}:T [[r handle]], x_{2}:T [[τ_{1}]]; C^{Θ′}
Φ_{3} = { }; K[[Δ, Δ′]], Δ^{Θ′}; S[[Γ, f:σ, x:τ_{1}]], Γ^{Θ′}x_{1}:T [[r handle]]; C^{Θ′}
Φ_{4} = { }; K[[Δ]], Δ^{Θ}; S[[Γ, f:σ]], Γ^{Θ}; C^{Θ}
Φ_{5} = { }; K[[Δ]], Δ^{Θ}; S[[Γ, f:σ]], Γ^{Θ}, x_{1}:T [[r handle]]; C^{Θ}

We begin by showing the continuation used in the translation of e_{2} is well-formed under the appropriate context (call this fact B_{2}):

{(By v-var) \atop Φ_{2} ⊢ x_{cont} : T [[τ_{cont}]]} {(By v-var) \atop Φ_{2} ⊢ x_{2} : T [[τ_{1}]]} (By eq-reflex)

K[[Δ, Δ′]], Δ^{Θ′} ⊢ ϵ′ ≤ ϵ′ D_{ϵ′}
Φ_{2} ⊢ x_{cont}(x_{2})

The derivation D_{ϵ′} is the following (recall that Δ^{Θ′} is Δ^{Θ}, ρ:Rgn, ϵ:Cap, ϵ′ ≤ \overline{ϵ ⊕ T [[ψ]] ⊕ \{ρ^{1}\}}):

K[[Δ, Δ′]], Δ^{Θ′} ⊢ ϵ′ ≤ \overline{ϵ ⊕ T [[ψ]] ⊕ \{ρ^{1}\}} (By sub-var)
= \overline{ϵ ⊕ T [[ψ]]} ⊕ \{ρ^{+}\} (By eq-distrib)

We have now shown B_{2}. By use of rule sub-var, we can conclude that (C_{2}):

K[[Δ, Δ′]], Δ^{Θ′} ⊢ C^{Θ′} ≤ \overline{B^{Θ′}}

We also have (D_{2}):

K[[Δ, Δ′]], Δ^{Θ′} ⊢ \overline{B^{Θ′}} = \overline{ϵ ⊕ T [[ψ_{f}]] ⊕ \{ρ^{1}\}}  (expand abbreviation)
= \overline{ϵ ⊕ \{ρ^{1}\} ⊕ T [[ψ_{f}]]}  (By eq-comm)
= \overline{ϵ ⊕ \{ρ^{1}\} ⊕ T [[ψ_{f}]] ⊕ T [[ψ_{f}]]} (By eq-dup)

Using A_{2}, B_{2}, C_{2} and D_{2}, we can apply the induction hypothesis and obtain E_{2}:

Φ_{3} ⊢ C_{ΔΔ′;Γ{f:σ,x:τ_{1}};Θ′}(e_{2})⟨x_{2}; x_{cont}(x_{2})⟩

Now, from A_{3}, B, C, and D, we can apply the induction hypothesis and obtain E_{3}:

Φ_{4} ⊢ C_{Δ;Γ{f:σ};Θ,x_{1}:T [[r handle]]}(e_{3})k

Using E_{2} and E_{3}, we can build the typing derivation for the code in the continuation for translating e_{1} (call this fact B_{1}):

(By v-var) Φ_{1} ⊢ x_{1} : r handle

E_{2}

Φ ⊢ fix f[⋯](⋯).C_{ΔΔ′;Γ{f:σ,x:τ_{1}};Θ′}(e_{2})⟨x_{2}; x_{cont}(x_{2})⟩ at r D_{r} E_{3}

Φ_{1} ⊢ let f = (⋯) at x_{1} in C_{Δ;Γ{f:σ};Θ,x_{1}:r handle}(e_{3})k

where the derivation D_{r} is:

K[[Δ]]Δ^{Θ} ⊢ C^{Θ} ≤ \overline{B^{Θ}}  (By assumption C)
= \overline{B^{Θ} ⊕ \{r^{1}\}} (By assumption D, Lemma 48)
= \overline{B^{Θ}} ⊕ \{r^{+}\} (By eq-distrib)

Finally, using A_{1}, B_{1}, C, and D, we can apply the induction hypothesis to the translation of e_{1}, giving us the final result:

{ }; K[[Δ]], Δ^{Θ}; S[[Γ]], Γ^{Θ}; C^{Θ} ⊢ C_{Δ;Γ;Θ}(letrecf[Δ′](x) : σ at e_{1} = e_{2} in e_{3})k

• The case for type application. The translation is:

C_{Δ;Γ;Θ}(f[c_{1}, …, c_{n}])k = A(k, f[T [[c_{1}]], …, T [[c_{n}]]])

The source typing derivation A, where σ is ∀[α_{1}:κ_{1}, …, α_{n}:κ_{n}].τ_{1} →^{ψ} τ_{2} at r :

{Δ ⊢_{R} σ  Δ ⊢_{R} c_{i} : κ_{i} \atop Δ; Γ ⊢_{R} f[c_{1}, …, c_{n}] : (τ_{1} →^{ψ} τ_{2})[c_{1}, …, c_{n}/α_{1}, …, α_{n}] at r, ∅} (Γ(f) = σ)

First, we must show that the value f[T [[c_{1}]], …, T [[c_{n}]]] is well-formed under the context

Φ_{1} = { }; K[[Δ]], Δ^{Θ}; S[[Γ]], Γ^{Θ}

where Θ = ⟨Δ^{Θ}; Γ^{Θ}; C^{Θ}; B^{Θ}⟩ First, we can conclude that

(By A and rule v-var)

Φ_{1} ⊢ f : T [[∀[α_{1}:κ_{1}, …, α_{n}:κ_{n}].τ_{1} →^{ψ} τ_{2} at r]]

Now, by induction on the number of constructors c_{i} applied to f, and use of the rule v-type, we can conclude that

Φ_{1} ⊢ f[T [[c_{1}]], …, T [[c_{n}]]] : T [[τ_{1} →^{ψ} τ_{2} at r]][T [[c_{1}]], …, T [[c_{n}]]/α_{1}, …, α_{n}]

By the Substitution Lemma, Lemma 45, we have

Φ_{1} ⊢ f[T [[c_{1}]], …, T [[c_{n}]]] : T [[(τ_{1} →^{ψ} τ_{2} at r)[c_{1}, …, c_{n}/α_{1}, …, α_{n}]]]

Using this fact, assumption B, and Lemma 50, we obtain our final result:

Φ_{1}; C^{Θ} ⊢ A(k, f[T [[c_{1}]], …, T [[c_{n}]]])

• The case for application. The translation is:

C_{Δ;Γ;Θ}(e_{1}^{τ_{f}} e_{2})k =

C_{Δ;Γ;Θ}(e_{1})⟨x_{1};
C_{Δ;Γ;Θ,x_{1}:T [[τ_{f}]]}(e_{2})⟨x_{2};

          letnewrgn ρ, x_{ρ} in

let f_{cont} = (fix f_{cont}[ ](C^{Θ} ⊕ {ρ^{1}}, x:T [[τ_{2}]]).letfreergn x_{ρ} in A(k, x)) at x_{ρ}
in x_{1}[ρ, B^{Θ}, C^{Θ} ⊕ {ρ^{1}}](x_{2}, f_{cont})⟩⟩

where

τ_{f} = τ_{1} →^{ψ_{f}} τ_{2} at r

The source typing derivation for the term is (A):

(A_{1}) Δ; Γ ⊢_{R} e_{1} : τ_{1} →^{ψ_{3}} τ_{2} at r, ψ_{1} (A_{2}) Δ; Γ ⊢_{R} e_{2} : τ_{1}, ψ_{2}
Δ; Γ ⊢_{R} e_{1}e_{2} : τ_{2}, ψ_{1} ∪ ψ_{2} ∪ ψ_{3} ∪ {r}

We begin showing that the result of the translation is type-correct by showing that the body of the innermost continuation (letnewrgn ρ, x_{ρ} in ⋯) is well-formed under the appropriate context. In order to make the derivation more manageable, we will use the following abbreviations:

Φ_{1}  = { }; K[[Δ]], Δ^{Θ}; S[[Γ]], Γ^{Θ}, x_{1}:T [[τ_{f}]], x_{2}:T [[τ_{2}]]; C^{Θ}
Φ_{2}  = { }; K[[Δ]], Δ^{Θ}, ρ:Rgn; S[[Γ]], Γ^{Θ}, x_{1}:T [[τ_{f}]], x_{2}:T [[τ_{2}]], x_{ρ}:ρ handle; C^{Θ} ⊕ {ρ^{1}}
Φ_{3}  = { }; K[[Δ]], Δ^{Θ}, ρ:Rgn; S[[Γ]], Γ^{Θ}, x_{1}:T [[τ_{f}]], x_{2}:T [[τ_{2}]], x_{ρ}:ρ handle, f_{cont}:τ_{cont}
Φ_{4}  = { }; K[[Δ]], Δ^{Θ}, ρ:Rgn; S[[Γ]], Γ^{Θ}, x_{1}:T [[τ_{f}]], x_{2}:T [[τ_{2}]], x_{ρ}:ρ handle
Φ_{5}  = { }; K[[Δ]], Δ^{Θ}, ρ:Rgn; S[[Γ]], Γ^{Θ}, x_{1}:T [[τ_{f}]], x_{2}:T [[τ_{2}]], x_{ρ}:ρ handle, f_{cont}:τ_{cont}, x:T [[τ_{2}]]
e′_{1}  = let f_{cont} = h_{cont} at x_{ρ} in e′_{2}
e′_{2}  = x_{1}[ρ, B^{Θ}, C^{Θ} ⊕ {ρ^{1}}](x_{2}, f_{cont})
h_{cont} = fix f_{cont}[ ](C^{Θ} ⊕ {ρ^{1}}, x:T [[τ_{2}]]).letfreergn x_{ρ} in A(k, x))
τ_{app} = (C^{Θ} ⊕ {ρ^{1}}, T [[τ_{1}]], τ_{cont}) → 0at r
τ_{cont} = (C^{Θ} ⊕ {ρ^{1}}, T [[τ_{2}]]) → 0at ρ

The derivation is as follows:

{D_{app} \atop Φ_{3} ⊢ x_{1}[ρ, B^{Θ}, C^{Θ} ⊕ \{ρ^{1}\}] : τ_{app}} {(by v-var) \atop Φ_{3} ⊢ x_{2} : T [[τ_{1}]]} {(by v-var) \atop Φ_{3} ⊢ f_{cont} : τ_{cont}} D_{r} D_{C^{Θ}}

Φ_{2}, f_{cont}:τ_{cont} ⊢ x_{1}[ρ, B^{Θ}, C^{Θ} ⊕ {ρ^{1}}](x_{2}, f_{cont}) D_{x_{ρ}} D_{h} D_{ρ}

Φ_{2} ⊢ let f_{cont} = h_{cont} at x_{ρ} in e′_{2}

                                   Φ_{1} ⊢ letnewrgn ρ, x_{ρ} in e′_{1}

The derivation D_{app} can be proven as follows. First, by rule v-var, we can deduce

Φ_{3} ⊢ x_{1} : T [[τ_{f}]] = ∀[ρ′:Rgn, ϵ:Cap, ϵ′ ≤ \overline{ϵ ⊕ T [[ψ_{3}]] ⊕ \{ρ^{′1}\}}].(ϵ′, T [[τ_{1}]], τ_{cont}) → 0at r From this judgement, two applications of the rule v-type give us:

Φ_{3} ⊢ x_{1}[ρ, B^{Θ}] : ∀[ϵ′ ≤ \overline{B^{Θ} ⊕ T [[ψ_{3}]] ⊕ \{ρ^{1}\}}].(ϵ′, T [[τ_{1}]], τ_{cont}) → 0at r

Finally, by rule v-sub, we can conclude:

Φ_{3} ⊢ x_{1}[ρ, B^{Θ}, C^{Θ} ⊕ {ρ^{1}}] : ∀[].(C^{Θ} ⊕ {ρ^{1}}, T [[τ_{1}]], τ_{cont}) → 0at r

because the required sub-capability relation holds:

K[[Δ]], Δ^{Θ}, ρ:Rgn ⊢ C^{Θ} ⊕ \{ρ^{1}\} ≤ \overline{B^{Θ}} ⊕ \{ρ^{1}\}  (By assumption C)
= \overline{B^{Θ} ⊕ T [[ψ_{3}]]} ⊕ \{ρ^{1}\} (By assumption D, Lemma 48)
≤ \overline{B^{Θ} ⊕ T [[ψ_{3}]] ⊕ \{ρ^{1}\}} (By rule sub-bar)

Next, we consider the derivation D_{r}. Here we must show that

K[[Δ]], Δ^{Θ}, ρ:Rgn ⊢ C^{Θ} ⊕ {ρ^{1}} ≤ C′′ ⊕ {r^{+}}

for some capability C′′. The reasoning is straightforward:

K[[Δ]], Δ^{Θ}, ρ:Rgn ⊢ C^{Θ} ⊕ {ρ^{1}} = {ρ^{1}} ⊕ C^{Θ}  (By rule eq-comm)
≤ \{ρ^{1}\} ⊕ \overline{B^{Θ}}  (By assumption C)
= \{ρ^{1}\} ⊕ \overline{B^{Θ} ⊕ T [[\{r\}]]} (By assumption D, Lemma 48)
= \{ρ^{1}\} ⊕ \overline{B^{Θ} ⊕ \{r^{1}\}}  (By def. of translation)
= \{ρ^{1}\} ⊕ \overline{B^{Θ}} ⊕ \{r^{+}\} (By rule eq-distrib)

Next, we consider D_{C^{Θ}}. The judgement we must prove is K[[Δ]], Δ^{Θ} ⊢ C^{Θ} ⊕ {ρ^{1}} ≤ C^{Θ} ⊕ {ρ^{1}}. This follows by rules sub-eq and eq-reflex. Next, we consider D_{x_{ρ}}. The judgement we must prove is: Φ_{4} ⊢ x_{ρ} : ρ handle. The judgement follows by rule v-var. Next, we must prove D_{h}:

(by v-var) Φ_{5} ⊢ x_{ρ} : ρ handle

(by eq-reflex)

K[[Δ]], Δ^{Θ}, ρ:Rgn ⊢ C^{Θ} ⊕ {ρ^{1}} = C^{Θ} ⊕ {ρ^{1}} : Cap D_{A(k,x)}

Φ_{5}; C^{Θ} ⊕ {ρ^{1}} ⊢ letfreergn x_{ρ} in A(k, x)
Φ_{4} ⊢ h_{cont} at ρ : T [[τ_{f}]]

The judgement we are trying to prove in the derivation D_{A(k,x)} is Φ_{5}; C^{Θ} ⊢ A(k, x). Using rule v-var, we can conclude that Φ_{5} ⊢ x : T [[τ_{2}]]. Assumption B tells us that Φ_{5}; C^{Θ} ⊢ e^{k}. Hence, by Lemma 50, we have the result. Finally, we show D_{ρ}. We must prove K[[Δ]], Δ^{Θ}, ρ:Rgn ⊢ C^{Θ}⊕{ρ^{1}} ≤ C′′⊕{ρ^{+}} for some capability C′′. This fact follows using rule sub-dup (C′′ is C^{Θ}). We have now satisfied all of the requirements necessary to show that the body of the innermost continuation is well-formed:

(B_{2}) Φ_{1} ⊢ letregion ρ, x_{ρ} in e′_{1}

We have A_{2} from the source typing derivation. If we let C_{2} be C and D_{2} be D, then we fulfill all of the requirements for the induction hypothesis and we may conclude E_{2}:

{ }; K[[Δ]], Δ^{Θ}; S[[Γ]], Γ^{Θ}, x_{1}:T [[τ_{f}]]; C^{Θ} ⊢ C_{Δ;Γ;Θ,x_{1}:T [[τ_{f}]]}(e_{2})⟨x_{2}; letregion ρ, x_{ρ} in e′_{1}⟩

Now, using this fact, A_{1} from the source typing derivation, C, and D, we can apply the induction hypothesis and conclude E_{1}:

{ }; K[[Δ]], Δ^{Θ}; S[[Γ]], Γ^{Θ}; C^{Θ} ⊢ C_{Δ;Γ;Θ}(e_{1})⟨x_{1}; C_{Δ;Γ;Θ,x_{1}:T [[τ_{f}]]}(e_{2})⟨⋯⟩⟩

which is equivalent to the result E that we were trying to prove.

• The case for letregion . The translation is:

C_{Δ;Γ;Θ}(letregion ρ, x_{ρ} in e)k =

                    letnewrgn ρ, x_{ρ} in

C_{Δ{ρ:Rgn};Γ{x_{ρ}:ρ handle};Θ′}(e)⟨x′; freergn x_{ρ} in A(k, x′)⟩

where

Θ′ = ⟨Δ^{Θ}; Γ^{Θ}; C^{Θ} ⊕ {ρ^{1}}; B^{Θ} ⊕ {ρ^{1}}⟩

The source typing derivation A:

(A_{1}) Δ{ρ:Rgn}; Γ{x_{ρ}:ρ handle} ⊢_{R} e : τ, ψ

Δ; Γ ⊢_{R} letregion ρ, x_{ρ} in e : τ, ψ\{ρ} ( \begin{matrix}ρ ∉ ftv(τ) ∪ Dom(Δ) \\ x_{ρ} ∉ Dom(Γ) \end{matrix} )

First, we show that the continuation for the translation of e is well-formed under an appropriate context:

D_{A(k,x′)} D_{C^{Θ}}

(by v-var) K[[Δ, ρ:Rgn]], Δ^{Θ}; S[[Γ, x_{ρ}:ρ handle]], Γ^{Θ}, Γ^{k}, x′:T [[τ]] ⊢ x_{ρ} : ρ handle

(B_{1}) K[[Δ, ρ:Rgn]], Δ^{Θ}; S[[Γ, x_{ρ}:ρ handle]], Γ^{Θ}, x′:T [[τ]]; C^{Θ} ⊕ {ρ^{1}} ⊢ letfreergn x_{ρ} in A(k, x′)

The judgement we must prove in D_{A(k,x′)} is:

(J) K[[Δ, ρ:Rgn]], Δ^{Θ}; S[[Γ, x_{ρ}:ρ handle]], Γ^{Θ}, x′:T [[τ]]; C^{Θ} ⊢ A(k, x′)

By rule v-var, we can conclude:

K[[Δ, ρ:Rgn]], Δ^{Θ}; S[[Γ, x_{ρ}:ρ handle]], Γ^{Θ}, x′:T [[τ]] ⊢ x′ : T [[τ]]

Using this fact, assumption B and Lemma 50, we can conclude (J). The judgement we must prove in D_{C^{Θ}} is:

K[[Δ, ρ:Rgn]], Δ^{Θ} ⊢ C^{Θ} ⊕ {ρ^{1}} = C^{Θ} ⊕ {ρ^{1}}

which follows by the rule eq-reflex. Now, we have fulfilled all the requirements necessary to show that the body of the innermost continuation is well-formed (call this fact B_{1}). We have A_{1} from the typing derivation. In order to apply the induction hypothesis, we must show C_{1}:

K[[Δ, ρ:Rgn]], Δ^{Θ} ⊢ C^{Θ} ⊕ \{ρ^{1}\} ≤ \overline{B^{Θ}} ⊕ \{ρ^{1}\} (By assumption C)
≤ \overline{B^{Θ}} ⊕ \overline{\{ρ^{1}\}} (By rule sub-bar)
= \overline{B^{Θ} ⊕ \{ρ^{1}\}} (By rule eq-distrib)

and also D_{1}:

K[[Δ, ρ:Rgn]], Δ^{Θ} ⊢ \overline{B^{Θ} ⊕ \{ρ^{1}\}} = \overline{B^{Θ} ⊕ T [[ψ\\{ρ\}]] ⊕ \{ρ^{1}\}} (By assumption D)
= \overline{B^{Θ} ⊕ T [[ψ]] ⊕ \{ρ^{1}\}}  (By Lemma 49)
= \overline{B^{Θ} ⊕ \{ρ^{1}\} ⊕ T [[ψ]]}  (By rule eq-comm)

Together A_{1}, B_{1}, C_{1} and D_{1} satisfy the preconditions for applying the induction hypothesis. The result is E_{1}:

K[[Δ, ρ:Rgn]], Δ^{Θ}; S[[Γ, x_{ρ}:ρ handle]], Γ^{Θ}; C^{Θ} ⊕ {ρ^{1}} ⊢ C_{K[[Δ,ρ:Rgn]],Δ^{Θ};S[[Γ,x_{ρ}:ρ handle]],Θ′}(e)⟨⋯⟩

Now, we can show the result of the translation type-checks:

E_{1}
K[[Δ]], Δ^{Θ}; S[[Γ]], Γ^{Θ}; C^{Θ} ⊢ letnewrgn ρ, x_{ρ} in C_{K[[Δ,ρ:Rgn]],Δ^{Θ};S[[Γ,x_{ρ}:ρ handle]],Θ′}(e)⟨⋯⟩

• The equality rule. The source typing derivation A is

Δ; Γ ⊢_{R} e : τ, ψ Δ ⊢_{R} τ = τ′ : Type Δ ⊢_{R} ψ ⊆ ψ′
(A_{1})Δ; Γ ⊢_{R} e : τ′, ψ′

and the continuation k = ⟨x; e^{k}⟩ is well-formed under the appropriate context (B):

{ }; K[[Δ]], Δ^{Θ}; S[[Γ]], Γ^{Θ}, x:T [[τ]]; C^{Θ} ⊢ e^{k}

By Lemma 44 and the equality judgement Δ ⊢ τ = τ′ : Type we can deduce that

K[[Δ]] ⊢ T [[τ]] = T [[τ′]] : Type

Therefore, by Lemma 51, we can deduce (B_{1}).

{ }; K[[Δ]], Δ^{Θ}; S[[Γ]], Γ^{Θ}, x:T [[τ′]]; C^{Θ} ⊢ e^{k}

Now, recall Assumption D states that

K[[Δ]], Δ ⊢ \overline{B^{Θ}} = \overline{B^{Θ} ⊕ T [[ψ′]]} : Cap

Using this fact, and the source typing derivation (A), which states that Δ ⊢ ψ ⊆ ψ′, and Lemma 48, we can deduce that (D_{1})

K[[Δ]], Δ ⊢ \overline{B^{Θ}} = \overline{B^{Θ} ⊕ T [[ψ]]} : Cap

Using A_{1}, B_{1}, C, and D_{1}, we can apply the induction hypothesis and obtain

{ }; K[[Δ]], Δ^{Θ}; S[[Γ]], Γ^{Θ}; C^{Θ} ⊢ C_{Δ;Γ;Θ}(e)k

and we are done.

We have completed the proof that the induction hypothesis is preserved by the translation. In order to obtain the proof of the CPS translation theorem, we simply instantiate the induction hypothesis. We are given part A: ·; · ⊢ e : int, ∅.

The continuation k is ⟨x; halt x⟩. Using the halt rule, we have part B,

{ }; ·; x:int ⊢ x : int · ⊢ ∅ = ∅ : Cap
{ }; ·; x:int; ∅ ⊢ halt x

Part C is trivial: · ⊢ ∅ ≤ ∅.

Part D is also straightforward,

· ⊢ \overline{∅} ≤ \overline{∅}  (By rule sub-eq)
= \overline{∅ ⊕ ∅}  (By rule eq-dup)
= \overline{∅ ⊕ T [[∅]]} (By definition of T [[ ·]])

Therefore, we can conclude E, { }; ·; ·; ∅ ⊢ C_{Θ}(e)k where Θ is the empty translation environment ⟨·; ·; ∅; ∅⟩ and k is the trivial continuation ⟨x; halt x⟩.

□