Jan Schwinghammer

Lars Birkedal

François Pottier

Bernhard Reus

Kristian Støvring

Hongseok Yang

A Step-Indexed Kripke Model of Hidden State

des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

Introduction

Information hiding, or hidden state, is one of the key design principles used by programmers in order to control the complexity of large-scale software systems. The idea is that an object (or function, or module) need not reveal in its interface the fact that it owns and maintains a private, mutable data structure. Hiding this internal invariant from the client has several beneficial effects. First, the complexity of the object's specification is slightly decreased. More importantly, the client is relieved from the need to thread the object's invariant through its own code. In particular, when an object has multiple clients, they are freed from the need to cooperate with one another in threading this invariant. Last, by hiding its internal state, the object escapes the restrictions on aliasing and ownership that are normally imposed on objects with mutable state.

The recently proposed anti-frame proof rule [24] enables hiding in the presence of higher-order store, i.e., memory cells containing (pointers to) procedures or code fragments. Thus, in combination with frame rules that allow the irrelevant parts of the state to be hidden during verification, the anti-frame rule can provide an important ingredient for modular, scalable program verification techniques. In this article, we study the semantic foundation of the anti-frame rule and give a soundness proof for it. Soundness means in particular that the execution of a well-typed program is safe (does not go wrong). Our proof involves an intricate recursive domain equation, and it helps identify some of the key ingredients for soundness.

Information hiding with frame and anti-frame rules

Our results are in a line of work on logic-based approaches to information hiding. These approaches adopt a standard semantics of the programming language, and deal with information hiding on a logical basis, for instance by extending a Hoare calculus with special proof rules. These rules usually take the form of frame rules that allow the implementation of an object to ignore (hence implicitly preserve) some of the invariants provided by the context, and of anti-frame rules, which allow an object to hide its internal invariant from the context [10,18,24,29].

It is worth emphasizing that hiding and abstraction (as studied, for instance, in separation logic [5,16,19,20]) are distinct mechanisms, which may co-exist within a single program logic. In recent program logics, abstraction is often implemented in terms of assertion variables (called abstract predicates by Parkinson) that describe the private data structures of an object. These variables are exposed to a client, but their definitions are not, so that the object's internals are presented to the client in an abstract form. Hiding, on the other hand, conceals the object's internals completely.

In its simplest form, the frame rule [29] states that invariants R can be added to valid triples: if{P }C{Q} is valid, then so is{P * R}C{Q * R}, where the separating conjunction P * R indicates that P and R govern disjoint regions of the heap. In subsequent developments, the rule was extended to handle higher-order procedures [10,18] and higher-order store [7,30]. Moreover, it was argued that both extensions of the rule support information hiding: they allow one to hide the invariant of a module and to prove properties of clients, as long as the module is understood in continuation-passing style [18].

Thorough semantic analyses were required to determine the conditions under which these extensions of the frame rule are sound. Indeed, the soundness of these rules raises subtle issues. For instance, the frame rule for higher-order procedures turns out to be inconsistent with the conjunction rule, a standard rule of Hoare logic [10,18]. Furthermore, seemingly innocent variants of the frame rule for higher-order store have been shown unsound [26,30].

In the most recent development in this line of research, Pottier [24] proposed an antiframe rule, which expresses the information hiding aspect of an object directly, instead of in continuation-passing style. Besides giving several extensive examples of how the anti-frame rule supports hidden state, Pottier argued that the anti-frame rule is sound by sketching a plausible syntactic argument. This argument, however, relied on several non-trivial assumptions about the existence of certain recursively defined types and re-cursively defined operations over types. In the present paper we justify these assumptions and give a complete soundness proof of Pottier's anti-frame rule.

This paper

This article is an extended version of results that were presented in two papers at the FOSSACS 2010 andFOSSACS 2011 conferences [31, 32].

In the first of these papers we presented our results on a semantic foundation for the anti-frame rule in the context of a simple while language with higher-order store, using a denotational semantics of the programming language. In the second paper we gave an alternative approach to constructing a model for the anti-frame rule and presented our results in the context of Charguéraud and Pottier's calculus of capabilities [11] that not only features higher-order store but also higher-order functions. In this latter paper we based the model on an operational semantics of the programming language, using the discovery that the metric approach to solving recursive possible world equations works both for denotationally-and operationally-based models [6].

In the present paper we describe our results in the context of the calculus of capabilities, using operational semantics. We detail both the original approach to constructing a model of the anti-frame rule from the FOSSACS 2010 paper (but adapted to operational semantics and step-indexing) and the alternative approach from the 2011 paper. We have chosen to use the capability calculus setup since Pottier has already shown how to reason about a range of applications with the anti-frame rule in this system [24]. Moreover, Pottier has also proposed generalized versions of the frame and anti-frame rules [25] for capabilities, and we show that our approach extends to these generalizations.

Overview of the technical development

Recently, Birkedal et al. [6] developed a step-indexed model of Charguéraud and Pottier's type and capability system with higher-order frame rules, but without the anti-frame rule. This was a Kripke model in which capabilities are viewed as assertions (on heaps) that are indexed over recursively defined worlds: intuitively, these worlds are used to represent the invariants that have been added by the frame rules.

Proving soundness of the anti-frame rule requires a refinement of this idea, as one needs to know that additional invariants do not invalidate the invariants on local state which have been hidden by the anti-frame rule. This requirement can be formulated in terms of a monotonicity condition for the world-indexed assertions, using an order on the worlds that is induced by invariant extension, i.e., the addition of new invariants. † More precisely, in the presence of the anti-frame rule, it turns out that the recursive domain equation for the worlds involves monotone functions with respect to an order relation on worlds, and that this order is specified using the isomorphism of the recursive world solution itself. This circularity means that standard existence theorems [2], (as used for the model without the anti-frame rule in [6]) cannot be applied to define the worlds.

In the present paper we develop a new model of Charguéraud and Pottier's system, which can also be used to show soundness of the anti-frame rule. Moreover, we demonstrate how to extend our model to prove soundness of Pottier's generalized frame and anti-frame rules, which allow hiding of families of invariants [25]. The new model is a non-trivial extension of the earlier work because, as pointed out above, the anti-frame rule is the source of a circular monotonicity requirement. We present two alternative approaches that address this difficulty.

In the first approach, a solution to the recursive world equation is defined by an inverse-limit construction in a category of metric spaces; the approximants to this limit are defined simultaneously with suitably approximated order relations between worlds. This approach has originally been used by Schwinghammer et al. [32] for a separation logic variant of the anti-frame rule, for a simple while language (untyped and without higher-order functions), and with respect to a denotational semantics of the programming language. In this article, the metrics that are employed to define the recursive worlds are linked to an operational semantics of the programming language instead, using the stepindexing idea [3,6]. While the construction is laborious, it results in a set of worlds that evidently has the required properties.

The second approach can loosely be described as a metric space analogue of Pitts' approach to relational properties of domains [23] and thus consists of two steps. First, we consider a recursive metric space domain equation without any monotonicity requirement, for which we obtain a solution by appealing to a standard existence theorem. Second, we carve out a suitable subset of what might be called hereditarily monotone functions. We show how to define this recursively specified subset as a fixed point of a suitable operator. While this second construction is considerably simpler than the inverse-limit construction, the resulting subset of monotone functions is, however, not a solution to the original recursive domain equation. Hence, we must verify that the semantic constructions that are used to justify the anti-frame rule restrict in a suitable way to the recursively defined subset of hereditarily monotone functions.

We show that our techniques generalize, by extending the model to Pottier's generalized frame and anti-frame rules [25]. For this extension, capabilities denote families of hereditarily monotone functions that are invariant under index reordering. The invariance property is expressed by considering a (recursively defined) partial equivalence relation on these families.

Outline

This paper is organised as follows. In the next section we give a brief overview of Charguéraud and Pottier's type and capability system with higher-order frame and antiframe rules. In Section 3 we discuss the requirements that the frame and anti-frame rules place on the worlds of the Kripke model. Section 4 gives some background on metric spaces, and Sections 5 and 6 present the two approaches to constructing the recursive worlds for the possible worlds model. (Readers not interested in the details of these con- and6.) The model is described and used to prove soundness of Charguéraud and Pottier's system in Section 7. In Section 8 we show how to extend the model to also prove soundness of the generalized frame and anti-frame rules.

v ::= x | | inj 1 v | inj 2 v | v, v | fun f (x) = t | l t ::= v | (v t) | case(v, v, v) | proj 1 v | proj 2 v | ref v | get v | set v

A Calculus of Capabilities

Charguéraud and Pottier's calculus of capabilities uses (affine) capabilities and (unrestricted) singleton types to track aliasing and ownership properties in a high-level, MLlike programming language [11]. Capabilities describe the shape of heap data structures, much like the assertions of separation logic. By introducing static names for values, singleton types make it possible for capabilities to refer to values, including procedure arguments and results.

In the present paper, we focus on the semantic foundations of the frame and anti-frame rules. Therefore, the exact details of the type-and-capability system are less important: in this section, we only give a brief overview of the calculus. ‡ We refer to earlier work that motivates the design of the system and gives detailed examples of its use [11,22,24,25].

Syntax and operational semantics

The programming language that we consider is a standard call-by-value, higher-order language with general references, sum and product types, and polymorphic and recursive types. The grammar in Figure 1 gives the syntax of values and expressions, keeping close to the notation of [11]. Here, the expression fun f (x) = t stands for the recursive procedure f with body t, and locations l range over a countably infinite set Loc.

The operational semantics (Figure 2) is given by a relation (t | h) -→ (t ′ | h ′ ) between configurations that consist of a (closed) expression t and a heap h. We take a heap h to be a finite map from locations to closed values. We use the notation h#h ′ to indicate that two heaps h, h ′ have disjoint domains, and we write h • h ′ for the union of two such heaps. By Val we denote the set of closed values.

Types and capabilities

Charguéraud and Pottier's type system uses capabilities, value types, and computation types. Figure 3 presents a subset of those. (The full syntax is given in Section 7.)

A capability C describes a heap property, much like the assertions of separation logic. ‡ We only consider a fragment of the capability calculus. In particular, we omit existential types and group regions.

((fun f (x) = t) v | h) -→ (t[f := fun f (x) = t, x := v] | h) (proj i v1, v2 | h) -→ (vi | h) for i = 1, 2 (case(v1, v2, inj i v) | h) -→ (vi v | h) for i = 1, 2 (ref v | h) -→ (l | h•[l → v]) if l / ∈ dom(h) (get l | h) -→ (h(l) | h) if l ∈ dom(h) (set l, v | h) -→ ( | h[l := v]) if l ∈ dom(h) (v t | h) -→ (v t ′ | h ′ ) if (t | h) -→ (t ′ | h ′ )
Fig. 2. Operational semantics

Capabilities C ::= ∅ | {σ : ref τ } | C * C | . . .

Value types τ

::= 1 | int | τ × τ | τ + τ | χ → χ | [σ] | . . .

Computation types χ

::= τ | χ * C | ∃σ.χ | . . . Value contexts ∆ ::= ∅ | ∆, x : τ | . . . Affine contexts Γ ::= ∅ | Γ, x : χ | Γ * C | . . .

Fig. 3. Capabilities and types

For instance, {σ : ref int} asserts that σ is a singleton region inhabited by one valid location that contains an integer value. Here σ is from a fixed set of region names. Group regions are omitted from this paper (see Sect. 9). More complex capabilities can be built using separating conjunction C 1 * C 2 . We write RegNames(C) for the region names appearing in capability C. Capabilities are affine: the type system ensures that they are never duplicated. This means that a capability can be regarded as a proof of ownership of the heap fragment that it describes.

Value types τ classify values; they include base types like int, singleton types [σ], and are closed under products and sums. Values are duplicable: in other words, a value does not have an "owner". Computation types χ describe the result of computations. They include all types of the form ∃ σ.(τ * C), which describe both the value and the heap that result from the evaluation of an expression. Arrow types (which are value types) have the form χ 1 → χ 2 and thus, like the pre-and post-conditions of a triple in Hoare logic, make explicit which part of the heap is accessed and modified by a procedure call.

We allow recursive capabilities as well as recursive value and computation types, provided the recursive definition is formally contractive [21], i.e., the recursion must go through one of the type constructors +, ×, →, ref, or through the right-hand side of the operator ⊗, which we introduce below ( §2.3). We will later see how this syntactic notion of contractiveness is justified by the model (Lemma 19).

Since Charguéraud and Pottier's system tracks aliasing, strong (i.e., not necessarily type preserving) updates can be admitted. A possible type for such an update operation is (

[σ] × τ 2 ) * {σ : ref τ 1 } → 1 * {σ : ref τ 2 }.
Here, the argument to the procedure is a pair consisting of a location (named σ) and the value to be stored (whose type is τ 2 ), and the

Γ v : [σ] * {σ : ref τ } Γ get v : τ * {σ : ref τ } Γ v : ([σ] × τ2) * {σ : ref τ1} Γ set v : 1 * {σ : ref τ2}
Fig. 4. Some typing rules for values and expressions location is assumed to be allocated in the initial heap (and to hold a value of some type τ 1 ). The result of the procedure is the unit value , but as a side-effect a value of type τ 2 will be stored at the location σ.

There are two typing judgements, x 1 : τ 1 , . . . , x n : τ n ⊢ v : τ for values, and x 1 : χ 1 , . . . , x n : χ n t : χ for expressions. The latter is similar to a separation logic triple where (the separating conjunction of) χ 1 , . . . , χ n serves as a precondition and χ as a postcondition. Since values cannot be reduced, there is no need for pre-and postconditions in the value typing judgement. Note that the set of value contexts is included in the set of affine contexts. Some of the inference rules that define the two typing judgements are given in Figure 4.

Invariant extension, frame and anti-frame rules

As in Pottier's work [24], following Birkedal, Torp-Smith and Yang's approach to higherorder frame rules [10], each of the type-level syntactic categories is equipped with an invariant extension operation, • ⊗ C. Intuitively, this operation conjoins C to the domain and codomain of every arrow type that occurs within its left hand argument, which means that the capability C is preserved by all procedures of this type.

This intuition is made precise by regarding capabilities and types modulo a structural equivalence which subsumes the "distribution axioms" for ⊗ that are used to express generic higher-order frame rules [10]. The two key cases of the structural equivalence are the distribution axioms for arrow types, (χ 5 shows some of the axioms that define the structural equivalence. The operations * and • form two monoid structures on capabilities (equations 1-3). The operation * and the invariant extension operation ⊗ are actions of these monoids (equations 4-17). The structural equivalence also includes the unfolding equations for recursive capabilities and types.

1 → χ 2 ) ⊗ C = (χ 1 ⊗ C * C) → (χ 2 ⊗ C * C), and for successive extensions, (χ ⊗ C 1 ) ⊗ C 2 = χ ⊗ (C 1 • C 2 ) where the derived operation C 1 •C 2 abbreviates the conjunction (C 1 ⊗C 2 ) * C 2 . Figure
The view of capabilities as the assertions of a program logic provides some intuition for the "shallow" and "deep" frame rules, and for the (essentially dual) anti-frame rule given in Figure 6. As in separation logic, the frame rules can be used to add a capability C (which might assert the existence of an integer reference, say) as an invariant to a Monoid structures on capabilities

( • ) • C2 def = ( • ⊗ C2) * C2 C1 * C2 = C2 * C1 (1) (C1 • C2) • C3 = C1 • (C2 • C3) (C1 * C2) * C3 = C1 * (C2 * C3) (2) C • ∅ = C C * ∅ = C (3)
Monoid actions

(• ⊗ C1) ⊗ C2 = • ⊗ (C1 • C2) • ⊗ ∅ = • (4) (• * C1) * C2 = • * (C1 * C2) • * ∅ = • (5)
Action by * on affine environments

(Γ, x : χ) * C = Γ, x : (χ * C) = (Γ * C), x : χ (6)
Action by ⊗ on capabilities, types, and environments

(• * •) ⊗ C = (• ⊗ C) * (• ⊗ C) (7) {σ : ref τ } ⊗ C = {σ : ref (τ ⊗ C)} (8) 1 ⊗ C = 1 (9) int ⊗ C = int (10) (τ1 + τ2) ⊗ C = (τ1 ⊗ C) + (τ2 ⊗ C) (11) (τ1 × τ2) ⊗ C = (τ1 ⊗ C) × (τ2 ⊗ C) (12) (χ1 → χ2) ⊗ C = (χ1 • C) → (χ2 • C) (13) [σ] ⊗ C = [σ] ( 14
) (∃σ.χ) ⊗ C = ∃σ.(χ ⊗ C) if σ / ∈ RegNames(C) (15)
∅ ⊗ C = ∅ (16) (Γ, x : χ) ⊗ C = (Γ ⊗ C), x : (χ ⊗ C) (17)
Fig. 5. Some axioms of the structural equivalence relation

Shallow frame Γ t : χ Γ * C t : χ * C Deep frame (computations) Γ t : χ (Γ ⊗ C) * C t : (χ ⊗ C) * C Deep frame (values) ∆ ⊢ v : τ ∆ ⊗ C ⊢ v : τ ⊗ C Anti-frame Γ ⊗ C t : (χ ⊗ C) * C Γ t : χ
Fig. 6. Frame and anti-frame rules specification Γ t : χ. This is useful for local reasoning: if the expression t does not even know that this reference exists and contains an integer value, then it must preserve these facts. The difference between the shallow variant Shallow frame and the deep variant Deep frame is that the former adds C only on the top-level, whereas the latter also extends all arrow types nested inside Γ and χ, via • ⊗ C. While the frame rules can be used to reason about certain forms of information hiding [10], the anti-frame rule expresses a hiding principle more directly: the capability C can be removed from the specification if C is an invariant that is established by t (this is expressed by • * C) and that is guaranteed to hold whenever control passes from t to the context or back (this is expressed by • ⊗ C).

Example: Landin's knot

Pottier [24] illustrates the anti-frame rule by a number of applications. One of these is a fixed-point combinator implemented by means of "Landin's knot," i.e., using backpatching and recursion through the heap: employing the standard let notation as syntactic sugar, fix can be written as

fun fix(f ) = let r = ref h = λy. (f (λx.(get r) x)) y = set r, h in h
When the fix combinator is applied to a functional f : (χ 1 → χ 2 ) → (χ 1 → χ 2 ), a new reference cell r is allocated. This cell is created empty (it holds the unit value), but is shortly thereafter updated so as to hold the function h which fix(f ) will return. Circularly, the code for h refers to r: we are "tying a knot in the store". Subsequent calls by the client to h are safe because the cell r exists, because the code stored in r preserves the fact that r exists, and so on, ad nauseam (the code stored in r preserves the fact that the code stored in r preserves the fact that r exists, etc.). We see that the reason why h is safe must be expressed as a recursive invariant. Here, this invariant takes the form of a recursive capability I, which satisfies the equation I = {σ : ref ((χ 1 → χ 2 ) ⊗ I)}, where σ is the singleton region that contains the cell denoted by the variable r. This invariant literally states that "the cell r exists and contains code that preserves this very fact".

Let us now briefly review how the body of fix is type-checked in the context f : (χ 1 → χ 2 ) → (χ 1 → χ 2 ), which we abbreviate as Γ. After the reference allocation expression, the variable r receives a singleton type [σ], where σ is a fresh region variable, and the capability {σ : ref 1} implicitly appears. We then examine the little "callback" function λx.(get r) x, and find that we have:

(Γ, r : [σ]) ⊗ I ⊢ λx.(get r) x : (χ 1 → χ 2 ) ⊗ I
That is, this function requires I (this justifies why reading r is permitted at all) and preserves I (because, according to I itself, the code found in r preserves I).

Let us now examine the application of f to this callback function. In the context Γ ⊗ I, the function f has type ((χ 1 → χ 2 ) ⊗ I) * I → ((χ 1 → χ 2 ) ⊗ I) * I. That is, provided I holds when f is invoked, f will accept our callback function as an argument, and will preserve I. Formally, we find:

(Γ, r : [σ]) ⊗ I ⊢ λy. (f (λx.(get r) x)) y : (χ 1 → χ 2 ) ⊗ I
Thus, the function h has type (χ 1 → χ 2 ) ⊗ I. It is worth noting that, at this point, the invariant I does not yet hold: instead of I, for the moment, we have {σ : ref 1}. However, by writing h into r, the third line of the definition of fix causes a strong update and establishes the invariant I. Indeed, the capability {σ

: ref 1} is transformed into {σ : ref ((χ 1 → χ 2 ) ⊗ I)},
which by definition is I. Formally, we have:

(Γ, r : [σ]) ⊗ I, h : (χ 1 → χ 2 ) ⊗ I * {σ : ref 1} set r, h : 1 * I
From this, we obtain :

(Γ, r : [σ]) ⊗ I * {σ : ref 1} let h = . . . in h : (χ 1 → χ 2 ) ⊗ I * I
which, by the structural equivalence axioms 17, 14, 9, and 6, can be written as:

(Γ, r : [σ] * {σ : ref 1}) ⊗ I let h = . . . in h : (χ 1 → χ 2 ) ⊗ I * I
At this point, the anti-frame rule allows us to hide the fact that the function h relies on a reference cell:

Γ, r : [σ] * {σ : ref 1} let h = . . . in h : χ 1 → χ 2
In a realistic language design, the programmer would indicate that the anti-frame rule must be applied here, and would provide the definition of I. Pottier [24] suggests a "hide" construct for this purpose.

We can now conclude that, in the context Γ, the body of fix has type χ 1 → χ 2 . As a result, fix itself receives the type ((χ 1 → χ 2 ) → (χ 1 → χ 2 )) → (χ 1 → χ 2 ). This type does not contain any assertion about the heap: the fixed point combinator presents a purely functional interface to the outside world. Thus, we can reason about the type safety of programs that use the fixed-point combinator without considering the reference cells used internally by that combinator.

Example: locks

The anti-frame rule imposes a strong requirement: the invariant must hold whenever control crosses the boundary between the "inside" (where the invariant is visible) and the "outside" (where the invariant is hidden). This requirement is tolerable when the invariant is very simple, as in Landin's knot, where the invariant expresses the existence of a single reference cell. However, when the invariant describes a more complex data structure, say, a hash table, this requirement becomes intolerable. Indeed, in this situation, the code inside the boundary needs to call hash table manipulation functions (find, etc.) that are defined outside the boundary. Thus, in order for a call to find to be well-typed, the caller is required to supply a capability for the hash table and for the invariant, where "and" means separating conjunction. This is impossible: the hash table is part of the invariant, so we can have either the hash table or the invariant, but not both at the same time. This problem, first noted by Alexandre Pilkiewicz, is documented by Pottier [26].

A solution to this problem, or at least a workaround, is proposed by Pilkiewicz and Pottier [22]. They suggest using the anti-frame rule to implement a lock abstraction. Just as in concurrent separation logic [13,14,17], a lock protects an invariant. Acquiring the lock causes the invariant to appear, seemingly out of thin air. One can then decide to temporarily break the invariant, until one reaches the point where one wishes to release the lock. Releasing the lock requires the invariant to hold, and consumes it: the invariant disappears again into thin air. In short, locks can be viewed as a mechanism for hidden state. In concurrent separation logic, they are considered primitive, whereas, in a sequential setting, they can be implemented in terms of the anti-frame rule. In either setting, the use of locks implies that a problem might occur at runtime: a deadlock in a concurrent setting, or a failure (caused by an attempt to re-acquire the lock) in the present sequential setting. Thus, by using locks, we get a somewhat weak static guarantee, but, in return, we obtain great flexibility. In the hash table example, a lock-based approach allows us to call find within the critical section, that is, to call find without first restoring the invariant.

Let the variable γ range over (affine) capabilities. In the following, we use γ to represent the invariant that the user wishes to associate with a lock. We define the type of locks, lock γ, via the following type abbreviation:

lock γ ≡ (1 → 1 * γ) × (1 * γ → 1)
This type describes a pair of functions, or "methods". The left-hand component of the pair is the "lock" method. Its type is 1 → 1 * γ, which means that this function takes a unit argument, produces a unit result, and, in addition, produces the capability γ. In other words, acquiring the lock causes its invariant to appear. Symmetrically, the righthand component of the pair is the "unlock" method. Its type is 1 * γ → 1, which means that this function requires the capability γ and consumes it.

The type lock γ is a value type. In other words, locks are ordinary values, and can be duplicated. The type system does not keep track of how locks are aliased, nor does it assign a unique owner to every lock. This allows locks to be used in flexible ways. Now, how can we implement locks? The idea is to represent a lock as a hidden reference cell that holds a Boolean flag. The flag tells whether the lock is currently available. In the locked state, the invariant γ is not known to hold. In the unlocked state, the invariant holds: in fact, the capability γ is then conceptually stored inside the lock itself. In order to reflect this idea, we define the following abbreviation:

flag γ ≡ 1 + (1 * γ)
We write locked for the value inj 1 and unlocked for the value inj 2 . At runtime, capabilities are erased, so a value of type flag γ is just a Boolean value. However, this definition allows the type system to keep track of the fact that γ holds if and only if the flag is unlocked .

The untyped code for the function newlock, which dynamically allocates a new lock, is as follows:

fun newlock ( ) = let r = ref locked in let lock ( ) = let content = get r in case content of | unlocked → set r, locked | locked → fail and unlock ( ) = set r, unlocked in lock , unlock
The function newlock creates a new reference cell r in the state locked . This cell will be accessible only through the functions lock and unlock, which capture its address. The function unlock updates r so as to mark the lock as available. The function lock reads r and dynamically checks whether the lock is available. If so, all is well, and r is updated so as to mark the lock as now unavailable. Otherwise, a fatal runtime failure occurs. This dynamic check ensures that two calls to lock without an intervening unlock will cause a failure. In the end, the function newlock returns the lock, which is represented by the pair lock , unlock .

Let us sketch how this code is type-checked. We write σ for the singleton region that contains r. We wish to use the anti-frame rule to hide the existence of the cell r. This cell holds a flag, so, at first glance, it seems that the hidden invariant I should be defined by I ≡ {σ : ref (flag γ)}. However, this definition is not quite right. As in Landin's knot ( §2.4), the invariant must be self-stable: it must be recursively defined by I ≡ {σ : ref (flag γ)} ⊗ I. We note that, because ⊗ distributes over all of the type constructors involved here, I is also equal to {σ : ref (flag (γ ⊗ I))}.

We do not show in detail how the functions lock and unlock are type-checked. In short, we are able to derive the following judgement:

r : [σ] let lock ( ) = . . . in lock , unlock : (1 * I → 1 * (γ ⊗ I) * I) × (1 * (γ ⊗ I) * I → 1 * I)
This judgement states that lock and unlock require I (which allows them to access r) and preserve I. It states, furthermore, that lock produces γ ⊗ I. Indeed, this capability is extracted out of r in the unlocked state, and, once r has been placed in the locked state, this capability does not have to be stored back into r, so it can be returned. The above judgement finally also states that unlock consumes γ ⊗ I. Indeed, after writing unlocked to r, one must store γ ⊗ I into r in order to justify that {σ :

ref (flag (γ ⊗ I))} holds, that is, that I holds.
By definition of lock γ and by the laws that govern the ⊗ operator, the above lengthy judgement can be summarized in a much clearer fashion as follows:

r : [σ] let lock ( ) = . . . in lock , unlock : (lock γ) ⊗ I
Using the first-order frame rule, we frame I onto this judgement, and obtain: We are now in a position to apply the anti-frame rule. The invariant I becomes hidden, and we obtain a more readable judgement:

r : [σ] * {σ : ref (flag γ)} let lock ( ) = . . . in lock , unlock : lock γ
Now, the first line of code in the body of newlock produces precisely the binding r : [σ] and the capability {σ : ref (flag γ)}, for a fresh σ, so, from the above judgement, we deduce: let r = . . . in lock , unlock : lock γ and we conclude that, in an empty typing environment, the function newlock has type 1 → lock γ. This type does not advertise any side effect: its domain and codomain are value types. Even though the capability γ is in general affine (and the type system has checked that we do not duplicate γ), a lock produced by newlock can be duplicated. The dynamic check within lock can be viewed as a dynamic mechanism for enforcing affinity, that is, a dynamic mechanism for preventing the duplication of the user invariant γ.

Our definition of lock γ as a pair of functions has an object-oriented flavor: by definition, locks are objects that support "lock" and "unlock" operations. If desired, it is easy, a posteriori, to make lock γ an abstract type, equipped with newlock, lock, and unlock operations. Pilkiewicz and Pottier rely on this abstract view of locks in order to build a hash-consing facility [22].

Kripke Semantics of Frame and Anti-frame Rules

Our soundness proof of the frame and anti-frame rules is based on two key ideas. The first idea is an interpretation of arrow types which explicates the universal and existential quantifications that are implicit in the anti-frame rule. Recall that

• • C = • ⊗ C * C
abbreviates the operation of combining two capabilities. Roughly speaking, in our model, an arrow type χ 1 → χ 2 consists of the procedures that have type

∀C. χ 1 • C → ∃C ′ . χ 2 • (C • C ′ )
in a standard interpretation. Pottier [24] showed how the anti-frame rule allows encoding ML-like weak references in terms of strong references. Readers who are familiar with Kripke models of ML references (see, e.g., [15]) may thus find the above interpretation natural, by reading the type as for all worlds C, if the procedure is given an argument of type χ 1 in world C, then, for some future world C • C ′ (an extension of C), the procedure returns a result of type χ 2 in world C • C ′ .

As indicated earlier, capabilities are like assertions in separation logic and thus describe heaps. However, to formalize the above meaning of arrow types, we need the second key idea of our model that capabilities (as well as types and type contexts) are parameterized by invariants. This parameterization will make it easy to interpret the invariant extension operation ⊗, as in earlier work [10,30]. Concretely, rather than interpreting a capability C directly as a set of heaps, we interpret it as a function C : W → Pred(Heap) that maps "invariants" from W to sets of heaps. Essentially, invariant extension of C ⊗ C ′ is then interpreted by applying C to (the interpretation of) the given invariant C ′ .

Note that if we interpreted C simply as a set of heaps, the semantics would not keep enough information to determine the meanings of different invariant extensions of C precisely.

Another intuitive argument for parameterization is that using worlds enables benign information sharing among various parts of the program in the presence of callbacks. It is known from earlier work on object invariants that reasoning about callbacks (which we have here in the form of higher-order functions) amounts to proving properties about concurrent executions. Using world parameters, we can enable proofs about different concurrent executions to share information about the invariants hidden by the antiframe rule. For instance, by interpreting a capability as a map W → Pred(Heap) or, equivalently, as a set of worlds and heaps, we ensure that a capability in a precondition records not only a set of heaps but also the shared invariants that a computation must preserve.

The question is now what the set W of invariants should be. As the frame and antiframe rules in Figure 6 suggest, invariants are in fact arbitrary capabilities, so W should be the set used to interpret capabilities. But, as we just saw, capabilities should be interpreted as functions from W to Pred(Heap). Thus, we are led to consider a Kripke model where the worlds are recursively defined: to a first approximation, we need a solution to the equation W = W → Pred(Heap).

In fact, in order to prove the soundness of the anti-frame rule, we will also need to consider a preorder on W and ensure that the interpretation of capabilities and types is monotone. This means that we should solve the equation

W = W → mon Pred(Heap) . (18)
The preorder ⊑ on W is induced by a monoid structure on W . More precisely,

w 1 ⊑ w ′ 1 holds, if w ′ 1 is w 1 • w 2
for some w 2 and some • operation where the associative operation

• is required to satisfy (w 1 • w 2 )(w) = (w 1 ⊗ w 2 )(w) * w 2 (w) (19)
as well as

(w 1 ⊗ w 2 )(w) = w 1 (w 2 • w) . ( 20
)
The first condition on • reflects the definition of the syntactic operation C 1 • C 2 , and the second is the semantic analogue of invariant extension. The monotonicity condition in (18) states that C ( C 1 ) ⊆ C ( C 1 • C 2 ) holds for any capability C -additional invariants (here C 2 , appearing in the combined invariant C 1 • C 2 ) cannot invalidate C with respect to a given invariant (here C 1 ). Intuitively, this property is necessary since C 1 may have been hidden by the anti-frame rule (so C 1 is not visible in the program logic) when the frame rule is applied to introduce C 2 later during the proof of a program.

Note that w 2 on the right-hand side of ( 20) is used both as an element in W and as a function on W . Hence, the well-formedness of the equation ( 20) assumes that the equation ( 18) is solved already. But at the same time, the monotonicity condition in (18) refers to the • operation in ( 19) and ( 20), and it assumes the existence of the • operation, creating the circularity among all the three equations. In Sections 5 and 6 we will address this circularity and construct sets of worlds W that satisfy a suitable variant of (18), using ultrametric spaces. To this end, we recall some basic definitions and results about metric spaces in the next section.

Ultrametric Spaces and Uniform Relations

This section summarizes some basic notions from the theory of metric spaces, and introduces "uniform relations" which will be used as building blocks for the interpretation in the following sections. For a less condensed introduction we refer to Smyth [34] and Birkedal et al. [9].

Ultrametric spaces

A 1-bounded ultrametric space (X, d) is a metric space where the distance function d : X × X → R takes values in the closed interval [0, 1] and satisfies the "strong" triangle inequality d(x, y) ≤ max{d(x, z), d(z, y)}, for all x, y, z ∈ X. A Cauchy sequence is a sequence (x n ) n∈N of elements in X such that for every k ∈ N there exists an index n and for all n 1 , n 2 ≥ n, d(x n1 , x n2 ) ≤ 2 -k . A metric space is complete if every Cauchy sequence (x n ) n∈N has a limit lim n x n . A subset of a complete metric space is closed if it closed under the limit operation.

A function f :

X 1 → X 2 between metric spaces (X 1 , d 1 ), (X 2 , d 2 ) is non-expansive if d 2 (f (x), f (y)) ≤ d 1 (x, y) for all x, y ∈ X 1 . It is contractive if there exists some δ < 1 such that d 2 (f (x), f (y)) ≤ δ • d 1 (x,
y) for all x, y ∈ X 1 . By the Banach fixed point theorem, every contractive function f : X → X on a complete and non-empty metric space (X, d) has a (unique) fixed point. By multiplication of the distances of (X, d) with a non-negative factor δ < 1, one obtains a new ultrametric space, δ • (X, d) = (X, d ′ ) where d ′ (x, y) = δ • d(x, y); this can be used to ensure contractiveness of functions.

The complete, 1-bounded, non-empty, ultrametric spaces and non-expansive functions between them form a Cartesian closed category CBUlt. The terminal object 1 is given by any singleton space, and products are given by the set-theoretic product where the distance is the maximum of the componentwise distances. The exponential (X 1 , d 1 ) → (X 2 , d 2 ) has the set of non-expansive functions from (X 1 , d 1 ) to (X 2 , d 2 ) as underlying set, and the distance function is given by the sup metric: If X is bisected, i.e., if all distances in X are of the form 2 -n for some n, then a function f : X → Y is non-expansive if and only if

d X1→X2 (f, g) = sup{d 2 (f (x), g(x)) | x ∈ X 1 } (note that
x n = x ′ implies f (x) n = f (x ′ ).
In the following, all the metric spaces that we consider have this property.

Uniform relations

In order to rephrase the (informal) requirement ( 18) in CBUlt, we consider uniform relations [6] in place of arbitrary predicates on Heap. More generally, let (A, ≤) be a preordered set. An (upwards closed) uniform relation on A is a subset p ⊆ N × A that is downwards closed in the first and upwards closed in the second component:

(k, a) ∈ p ∧ j ≤ k ∧ a ≤ b ⇒ (j, b) ∈ p .
We write URel (A) for the set of all such relations on A, and for k ∈ N we define p

[k] = {(j, a) ∈ p | j < k}. Note that p [k] ∈ URel (A) if p ∈ URel (A), and that p ⊆ p ′ implies p [n] ⊆ p ′ [n] . We equip URel (A) with the distance function d(p, q) = inf{2 -n | p [n] = q [n]
}, which makes (URel (A), d) an object of CBUlt. Moreover, URel (A) forms a complete Heyting algebra.

Proposition 1. URel (A), ordered by inclusion, forms a complete Heyting algebra. Meets and joins are given by set-theoretic intersections and unions, resp., and implication p ⇒ q is given by the uniform relation such that (k, a) ∈ (p ⇒ q) holds if and only if for all j ≤ k and all b ≥ a, (j, b) ∈ p implies (j, b) ∈ q.

Meets, joins and implication are non-expansive operations on URel (A) with respect to the distance function d defined above.

In our model, we use URel (A) with the following concrete instances for the preorder (A, ≤):

1 heaps (Heap, ≤), where h ≤ h ′ if and only if h ′ = h • h 0 for some h 0 #h, 2 values (Val , ≤), where v ≤ v ′ if and only if v = v ′ , 3 stateful values (Val × Heap, ≤), where (v, h) ≤ (v ′ , h ′ ) if and only if v = v ′ and h ≤ h ′ , and 4 stateful expressions (Exp × Heap, ≤), where (t, h) ≤ (t ′ , h ′ ) if and only if t = t ′ and h = h ′ .
We also use variants of ( 2) and (3) where the set Val is replaced by the set of value substitutions, Env .

Proposition 2. URel (Heap) forms a complete BI algebra [28]. The separating conjunction and separating implication are given by

(k, h) ∈ (p 1 * p 2 ) ⇔ ∃h 1 , h 2 . h = h 1 •h 2 ∧ (k, h 1 ) ∈ p 1 ∧ (k, h 2 ) ∈ p 2 (k, h) ∈ (p - * q) ⇔ ∀j ≤ k. ∀h ′ #h. (j, h ′ ) ∈ p ⇒ (j, h • h ′ ) ∈ q
and the unit for * is given by I = N × Heap.

Up to the natural number indexing, URel (Heap) is just the standard intuitionistic (in the sense that it is not "tight") heap model of separation logic [29]. Both separating conjunction and separating implication are non-expansive operations on URel (Heap).

In the following, when interpreting types and capabilities, we will not need to use all of the algebraic structure on uniform relations. Nevertheless, the fact that the uniform relations form a complete Heyting (BI) algebra suggests that Charguéraud and Pottier's system could, in principle, be extended to a full-blown program logic by including all of the logical connectives of separation logic assertions in the syntax of capabilities.

Preordered metric spaces

The uniform relations URel (A), ordered by inclusion, form an example of a preordered metric space. More generally, a preordered, complete, 1-bounded ultrametric space is an object (X, d) ∈ CBUlt equipped with a preorder ≤ such that for all Cauchy sequences (x n ) n∈N and (y n ) n∈N , if x n ≤ y n holds for all n ∈ N then lim n x n ≤ lim n y n .

For preordered, complete, 1-bounded ultrametric spaces X 1 and X 2 we write X 1 → mon X 2 for the set of non-expansive and monotone functions between X 1 and X 2 . When equipped with the sup-distance,

d(f, g) = sup{d 2 (f x, g x) | x ∈ X 1 }, the set X 1 → mon X 2 becomes an object of CBUlt.
Proposition 3. For any preordered, complete, 1-bounded ultrametric spaces X and Y , if Y is a complete Heyting algebra with non-expansive algebra operations, so is X → mon Y , when this function space is equipped with the pointwise order. Meets and joins are given by the pointwise extension of the corresponding operations on Y , and

f ⇒ g is defined by (f ⇒ g)(x) = x ′ ≥x f (x ′ ) ⇒ g(x ′ ) .
In the case where Y is URel (Heap), X → mon URel (Heap) is a complete BI algebra where * and - * are non-expansive operations. Separating conjunction f * g and its unit I are defined pointwise, and the separating implication f - * g is defined by (f - * g)(x) =

x ′ ≥x f (x ′ ) - * g(x ′ ) .

Monotone Recursive Worlds

In this section we prove the following existence theorem:

Theorem 4 (Existence of monotone recursive worlds). There exists a preordered monoid (W, ⊑, •, e) where W is an object of CBUlt with a non-expansive isomorphism ι from 1 2 • W → mon URel (Heap) to W , such that the following conditions hold: 1 The preorder on W is given by w

⊑ w ′ ⇔ ∃w 0 . w ′ = w • w 0 . 2 The operation • : W × W → W is non-expansive. 3 For all w 1 , w 2 , w ∈ W , ι -1 (w 1 • w 2 )(w) = ι -1 (w 1 )(w 2 • w) * ι -1 (w 2 )(w).
In condition (3), the operation * is the separating conjunction on uniform heap relations described in Proposition 2. By Proposition 3, 1 2 • W → mon URel (Heap) is a complete BI algebra.

This theorem asserts the existence of a suitable set of worlds for the interpretation of the capability calculus. In particular, if we define

(f ⊗ w 1 )(w) = f (w 1 • w) for f ∈ 1 2 • W → mon URel (Heap) and w 1 , w ∈ W , we have ι -1 (w 1 • w 2 )(w) = (ι -1 (w 1 ) ⊗ w 2 )(w) * ι -1 (w 2 )(w) .
Apart from the insertion of the isomorphism in this equation, the difference between the statement of the theorem and the informal requirements (18-20) on page 14 are the use of uniform relations instead of arbitrary predicates over heaps, the restriction to non-expansive functions, and the scaling factor 1 2 . (Note that a non-expansive function

1 2 • W → mon URel (Heap)
is the same as a contractive function W → mon URel (Heap) with contraction factor 1 2 .) We prove Theorem 4 by constructing W ∼ = 1 2 • W → mon URel (Heap) explicitly, as (inverse) limit

W = x ∈ k≥0 W k | ∀k ≥ 0. x k = ǫ • k (x k+1 ) of a sequence of "approximations" W k of W , W 0 ǫ0 / / W 1 ǫ • 0 o o ǫ1 / / W 2 ǫ • 1 o o ǫ2 / / . . . ǫ • 2 o o ǫ k / / W k+1 ǫ • k o o ǫ k+1 / / . . . ǫ • k+1 o o (21)
Each W k is a complete, 1-bounded, ultrametric space with distance function d k , and comes equipped with a non-expansive operation

• k : W k × W k → W k
and a preorder ⊑ k . This sequence will be defined inductively, so that W k+1 = 1 2 • W k → mon URel (Heap) consists of the non-expansive and monotone functions with respect to ⊑ k .

Cauchy tower of approximants

We define preordered, complete, 1-bounded ultrametric spaces (W k , ⊑ k ), binary operations • k on W k , and functions

W k ǫ k / / 1 2 • W k → mon URel (Heap) ǫ • k o o
by induction on k as follows.

-

W 0 = {⋆} is a one-point space; -• 0 is given by ⋆ • 0 ⋆ = ⋆; -⊑ 0 is the trivial order, ⋆ ⊑ 0 ⋆; -ǫ 0 (w) = I, the unit of the BI algebra structure on 1 2 • W 0 → mon URel (Heap); -ǫ • 0 (f ) = ⋆. For k ≥ 0, -W k+1 = 1 2 • W k → mon URel (Heap); -• k+1 is given by (f • k+1 g)(w) = f ((ǫ • k g) • k w) * g(w); -f ⊑ k+1 g holds if g k+1 = f • k+1 f 0 for some f 0 ∈ W k+1 ; -ǫ k+1 (f ) sends g ∈ 1 2 • W k+1 to (f (ǫ • k g)) [k+2] ∈ URel (Heap); -ǫ • k+1 (F ) sends w ∈ 1 2 • W k to (F (ǫ k w)) [k+1]
∈ URel (Heap). In the rest of this subsection we show that ⊑ k indeed defines a preorder on W k , and that ǫ k and ǫ • k are non-expansive and map into the space of non-expansive and monotone functions. One technical inconvenience in these proofs is that the operations • k are not preserved by ǫ k and ǫ • k-1 , and that they are not associative. However, associativity holds "up to approximation k," which explains the definition of ⊑ k above.

Lemma 5 (Well-definedness). For all k ≥ 0,

1 ǫ k and ǫ • k are non-expansive functions between W k and 1 2 • W k → URel (Heap). 2 For all w, w ′ ∈ W k , w • k w ′ ∈ W k . 3 • k is a non-expansive operation on W k . 4 For all w, w ′ , w ′′ ∈ W k , (w • k w ′ ) • k w ′′ k = w • k (w ′ • k w ′′ ).
5 For all w ∈ W k+1 , I • k+1 w = w and w • k+1 I k+1 = w, where I is the unit of the BI algebra structure on

1 2 • W k → mon URel (Heap). 6 The relation ⊑ k is a preorder on W k . 7 For all w ∈ W k and F ∈ W k+2 , ǫ k (w) and ǫ • k+1 (F ) are monotone functions 1 2 • W k → mon URel (Heap). 8 For all w ∈ W k , ǫ • k (ǫ k w) k = w. For all g ∈ W k+1 , ǫ k (ǫ • k g) k = g. 9 For all w, w ′ ∈ W k , ǫ k (w • k w ′ ) k = (ǫ k w) • k+1 (ǫ k w ′ ). For all g, g ′ ∈ W k+1 , ǫ • k (g • k+1 g ′ ) k = (ǫ • k g) • k (ǫ • k g ′ ).
Proof. The properties are proved simultaneously by induction on k. The case k = 0 follows directly from the definitions. We give the key ideas for the case k > 0:

1 The claimed non-expansiveness properties are consequences of the non-expansiveness of ǫ k-1 and ǫ • k-1 , obtained from the induction hypothesis, and from the non-expansiveness of function composition. 2 By induction hypothesis, • k-1 and ǫ • k-1 are non-expansive functions; the non-expansiveness of w • k w ′ then follows with the non-expansiveness of * . The monotonicity of w • k w ′ follows from the definition of ⊑ k , the approximate associativity of • k-1 given by part (4) of the induction hypothesis, and the monotonicity of * on URel (Heap). 3 For non-expansiveness of 1) and (3) of the induction hypothesis. Thus, for all w 1 , w ′ 1 with w

• k , note that (ǫ • k-1 w 2 ) • k-1 w n = (ǫ • k-1 w ′ 2 ) • k-1 w holds for all w ∈ W k-1 and all w 2 , w ′ 2 ∈ W k with w 2 n = w ′ 2 by parts (
1 n = w ′ 1 , the non-expansiveness of * , w 1 and w ′ 1 yields (w 1 • k w 2 )(w) n = (w ′ 1 • k w ′ 2 )(w). Since w is chosen arbitrarily, the sup-metric on W k shows w 1 • k w 2 n = w ′ 1 • k w ′ 2 . 4 Given any x ∈ 1 2 • W k-1 , ((w • k w ′ ) • k w ′′ )(x) k = (w • k (w ′ • k w ′′ ))(x)
follows from parts (4) and (9) of the induction hypothesis. Thus, the claim follows with the sup-metric on W k . 5 That I • k+1 w = I follows easily from the definition of I. For the second claim, first note that (ǫ

• k I) k = I holds in W k . Thus, (ǫ • k I) • k x k+1 = I • k x = I holds in 1 2
• W k for any x, by the non-expansiveness of • k and by the first claim. From this observation, the k + 1-equivalence of w • k+1 I and w follows with the non-expansiveness of w and the definition of • k+1 . 6 That ⊑ k is a preorder follows from its definition using parts (4) and (5). 7 That ǫ k (w)(w 1 ) ⊆ ǫ k (w)(w 2 ) holds for any w, w 1 , w 2 ∈ W k with w 1 ⊑ k w 2 is a consequence of the monotonicity of w, part (9) of the induction hypothesis and the definition of ǫ k . For the second claim observe that, whenever w 1 ⊑ k w 2 , the definition of ⊑ k and part (9) of the induction hypothesis yield ǫ k (w 2 )

k = ǫ k (w 1 ) • k+1 ǫ k (w 0 ) for some w 0 . Hence, ǫ • k+1 (F )(w 2 ) = (F (ǫ k w 2 )) [k+1] = (F (ǫ k (w 1 ) • k+1 ǫ k (w 0 ))) [k+1] ⊇ (F (ǫ k w 1 )) [k+1] = ǫ • k+1 (F )(w 1 )
by the contractiveness and monotonicity of F and the definition of ǫ • k+1 . 8 The claims follow from part (8) of the induction hypothesis, using the fact that function composition is non-expansive and that functions in W k for k > 0 are contractive with contraction factor 1 2 , due to the scaling in the definition of W k . 9 By part (9) of the induction hypothesis and by property (8) that we have just es-

tablished, ǫ • k-1 (ǫ • k (ǫ k w ′ ) • k w 0 ) k-1 = ǫ • k-1 (w ′ ) • k-1 ǫ • k-1 (w 0
) holds for all w ′ , w 0 ∈ W k . Thus, using the definition of • k and ǫ k , the contractiveness of w ∈ W k , and the non-expansiveness of * ,

(ǫ k w • k+1 ǫ k w ′ )(w 0 ) = (w(ǫ • k-1 (ǫ • k (ǫ k w ′ ) • k w 0 ))) [k+1] * (w ′ (ǫ • k-1 w 0 )) [k+1] k = (w(ǫ • k-1 (w ′ ) • k-1 ǫ • k-1 (w 0 )) * w ′ (ǫ • k-1 w 0 )) [k+1] = (w • k w ′ )(ǫ • k-1 w 0 ) [k+1] ,
which is just ǫ k (w • k w ′ )(w 0 ). Since this approximate equality holds for all w 0 , the claim follows by definition of the sup-metric on W k . The second claim is proved similarly.

Part (8) of Lemma 5 states that diagram (21) forms a Cauchy tower [9], meaning that sup

w d k+1 (w, ǫ k (ǫ • k w)) as well as sup w d k (w, ǫ • k (ǫ k w)) become arbitrarily small as k increases. This ensures that W = {x ∈ k≥0 W k | ∀k ≥ 0. x k = ǫ • k (x k+1
)}, equipped with the sup-distance, is an object of CBUlt. Limits of Cauchy chains in W are given componentwise.

Monoid structure on the inverse limit

For all 0 ≤ k < l, we define the functions ǫ k,l :

W k → W l and ǫ • k,l : W l → W k by ǫ k,l = ǫ l-1 • . . . • ǫ k+1 • ǫ k ǫ • k,l = ǫ • k • ǫ • k+1 • . . . • ǫ • l-1
which are non-expansive by Lemma 5(1).

Next, we equip W with an operation • : W × W → W defined by

(x k ) k≥0 • (y k ) k≥0 = lim j>k ǫ • k,j (x j • j y j ) k≥0 .
Note that the limits exist: ǫ

• j (x j+1 • j+1 y j+1 ) j = ǫ • j (x j+1 ) • j ǫ • j (y j+1 ) =
x j • j y j by Lemma 5(9), and so (ǫ • k,j (x j • j y j )) j>k forms a Cauchy sequence in W k by the nonexpansiveness of ǫ • k,j . Moreover, we have ǫ Proof. From the definition of e and •, we have e • w = w • e = w for all w ∈ W . To see the associativity of •, suppose x, y, z ∈ W . Lemma 5(4) shows for all j: (x j • j y j ) • j z j j = x j • j (y j • j z j ). We obtain

• k (lim j>k+1 ǫ • k+1,j (x j • j y j )) = lim j>k+1 ǫ • k,j (x j • j y j )
x j • j (y • z) j = x j • j (lim l>j ǫ • j,l (y l • l z l )) = lim l>j x j • j ǫ • j,l (y l • l z l )) by non-expansiveness of • j j = lim l>j x j • j (ǫ • j,l (y l ) • j ǫ • j,l (z l )) by Lemma 5(9) = lim l>j x j • j (y j • j z j ) since y, z ∈ W j = lim l>j (x j • j y j ) • j z j by Lemma 5(4) j = (x • y) j • j z j .
Thus, for any real number ε > 0 there exists n ≥ 0 sufficiently large such that

∀j ≥ n. d Wj ((x • y) j • j z j , x j • j (y • z) j ) < ε.
Since ǫ • k,j is non-expansive, this yields for all k

((x • y) • z) k = lim j>k ǫ • k,j ((x • y) j • j z j ) = lim j>k ǫ • k,j (x j • j (y • z) j ) = (x • (y • z)) k which proves (x • y) • z = x • (y • z).
Finally, • is non-expansive since each • j and ǫ • k,j is non-expansive.

Isomorphism between W and monotone functions on W

As shown in the preceding Lemma 6, • is associative and has e as a unit. Therefore we can consider the induced preorder on W , w ⊑ w ′ ⇔ ∃w 0 . w ′ = w •w 0 . It remains to establish an isomorphism W ∼ = 1 2 • W → mon URel (Heap) in CBUlt (where the monotonicity refers to this preorder ⊑ on W ) that satisfies condition (3) from Theorem 4.

To this end, first note that if

w ′ = w • w ′′ then w ′ k k = w k • k w ′′
k for all k, and therefore we obtain

∀w, w ′ ∈ W. w ⊑ w ′ ⇒ ∀k. w k ⊑ k w ′ k . ( 22
)
Now note that for each k and for all sequences (w k ) k≥0 and (w ′ k ) k≥0 in W we have

w k+1 (w ′ k ) = ǫ • k+1 (w k+2 )(ǫ • k w ′ k+1 ) = (w k+2 (ǫ k (ǫ • k w ′ k+1 ))) [k+1] k+1 = w k+2 (w ′ k+1 )
by Lemma 5(8) and the contractiveness of w k+2 . Hence, (λw ′ .w k+1 (w ′ k )) k≥0 is a Cauchy sequence in 1 2 • W → URel (Heap). In fact, it is a sequence in the (complete) subspace of monotone maps, by ( 22) and the fact that each w k is monotone, and therefore this sequence has a limit in 1 2 • W → mon URel (Heap). We may thus define

ι • (w) = lim k (λw ′ ∈ W. w k+1 (w ′ k ))
For g ∈ 1 2 • W → mon URel (Heap) we define ι(g) k ∈ W k by the following two cases:

ι(g) 0 = ⋆ ι(g) k+1 = λw ∈ 1 2 • W k . (g lim l>max{i,k} ǫ • i,l (ǫ k,l w) i≥0 ) [k+1]
For this definition, one first checks that the sequence (lim l>max{i,k} ǫ • i,l (ǫ k,l w)) i≥0 is an element of W , so that g can be applied. Next, each ι(g) k+1 is monotone. To see this, let w 1 ⊑ k w 2 , so by definition of ⊑ k there exists w 0 ∈ W k such that w 2 and w 1 • k w 0 are k-equivalent in W k ; we must show that (ι g) k+1 (w 1 ) ⊆ (ι g) k+1 (w 2 ). Let

x j = (lim l>max{i,k} ǫ • i,l (ǫ k,l w j )) i≥0 for j = 0, 1, 2. Then, x 2 k = x 1 • x 0 holds in W . From
the non-expansiveness and monotonicity of g it follows that g(x 2 )

k+1 = g(x 1 • x 0 ) ⊇ g(x 1
), and therefore (g x 1 ) [k+1] ⊆ (g x 2 ) [k+1] , which yields the claimed monotonicity of ι(g) k+1 . Finally, ι g ∈ W holds since the definition of ι satisfies ǫ • k (ι g) k+1 = (ι g) k for all k.

Lemma 7. The assignment of g to ι(g) determines a non-expansive function from 1 2 • W → mon URel (Heap) to W , with a non-expansive inverse given by ι • .

Proof sketch The non-expansiveness of ι and ι • is easy to see. To show that ι • is a right-inverse to ι one first proves that (ι(ι • w)) n n = w n holds for all w ∈ W and n ∈ N. This yields the required equality, since

(ι(ι • w)) l = lim n>l ǫ • l,n ((ι(ι • w)) n ) = lim n>l ǫ • l,n (w n ) = w l
follows for each l by the non-expansiveness of the ǫ • n,l 's. That ι • is also a left-inverse to ι can be seen by a similar calculation.

To finish the proof of Theorem 4 we need to establish the relationship between the monoid multiplication and the isomorphism:

Lemma 8. For all w 1 , w 2 , w ∈ W , ι -1 (w 1 • w 2 )(w) = ι -1 (w 1 )(w 2 • w) * ι -1 (w 2 )(w).
Proof sketch One first shows that g(w) = lim k lim j>k+1 (ι g) j (ǫ • k,j-1 w k ) for all g in 1 2

• W → mon URel (Heap) and w ∈ W . Using this equation, the claim is then established by unfolding the definitions of • and ι -1 .

Hereditarily Monotone Recursive Worlds

In this section we present an alternative construction of a set of recursive worlds, which differs from the one defined in the previous section in some respects. Either set is suitable for the interpretation of the capability calculus.

Recursive worlds

The first step in this construction is the definition of recursive worlds without monotonicity condition. It is well-known that one can solve recursive domain equations in CBUlt, given by locally contractive functors, by an adaptation of the inverse-limit method from classical domain theory [2]. In particular, by considering the space of contractive but not necessarily monotone functions in the domain equation ( 18) above, America and Rutten's existence theorem applies.

Proposition 9. There exists a unique (up to isomorphism) metric space (X, d) ∈ CBUlt and an isomorphism ι from 1 2 • X → URel (Heap) to X.

Proof. X is obtained by America and Rutten's existence theorem for fixed points of locally contractive functors [2], applied to the functor F :

CBUlt op -→ CBUlt, F (X) = 1 2 • X → URel (Heap).
The next step is to define the composition operation • on X.

Lemma 10. There exists a non-expansive operation • : X × X → X such that

∀x 1 , x 2 , x ∈ X. ι -1 (x 1 • x 2 )(x) = ι -1 (x 1 )(x 2 • x) * ι -1 (x 2 )(x) ,
This operation is associative, and has emp = ι(I) as left and right unit, for I(w) = N × Heap the unit of the lifted separating conjunction described in Proposition 3.

Proof. The operation • can be defined by a straightforward application of Banach's fixed point theorem on the complete ultrametric space X × X → X. The proof that emp is a left and right unit is easy. For associativity one proves

x 1 • (x 2 • x 3 ) n = (x 1 • x 2 ) • x 3 for all n ∈ N by induction. See [30].
We define f ⊗ x, for f : 1 2 • X → URel (Heap) and x ∈ X, as the non-expansive function

1 2 • X → URel (Heap) given by (f ⊗ x)(x ′ ) = f (x • x ′ ).
Since • defines a monoid structure on X there is an induced preorder on X given by x ⊑ y ⇔ ∃x 0 . y = x • x 0 . We will now "carve out" a subset of functions in 1 2 • X → URel (Heap) that are monotonic with respect to this preorder. This subset needs to be defined recursively.

Relations on ultrametric spaces

For X ∈ CBUlt let R(X) be the collection of all non-empty and closed § relations R ⊆ X; we will just write R when X is clear from the context. We set

R [n] def = {y | ∃x ∈ X. x n = y ∧ x ∈ R} . for R ∈ R. Thus, R [n] is the set of all points within distance 2 -n of R. Note that R [n] ∈ R. In fact, ∅ = R ⊆ R [n]
holds by the reflexivity of n-equality, and if (y k ) k∈N is a sequence in R [n] with limit y in X then d(y k , y) ≤ 2 -n must hold for some k, i.e., y k n = y. So there exists x ∈ X with x ∈ R and x n = y k , and hence by transitivity

x n = y which then gives lim n y n ∈ R [n] .
We make some further observations that follow from the properties of n-equality on X. First, R ⊆ S implies R [n] ⊆ S [n] for any R, S ∈ R. Moreover, using the fact that the n-equalities become increasingly finer it follows that (R

[m] ) [n] = R [min(m,n)] for all m, n ∈ N, so in particular each (•) [n] is a closure operation on R. As a consequence, we have R ⊆ . . . ⊆ R [n] ⊆ . . . ⊆ R [1] ⊆ R [0] . By the 1-boundedness of X, R [0] = X for all R ∈ R. Finally, R = S if and only if R [n] = S [n] for all n ∈ N. Proposition 11. Let d : R × R → R be defined by d(R, S) = inf {2 -n | R [n] = S [n] }. Then (R, d) is a complete, 1-bounded, non-empty ultrametric space. The limit of a Cauchy chain (R n ) n∈N with d(R n , R n+1 ) ≤ 2 -n is given by n (R n ) [n] , and in particular R = n R [n] for any R ∈ R.
Proof. First, R is non-empty since it contains X itself, and d is well-defined since

R [0] = S [0] holds for any R, S ∈ R. Next, since R = S is equivalent to R [n] = S [n]
for all n ∈ N, it follows that d(R, S) = 0 if and only if R = S. That the ultrametric inequality d(R, S) ≤ max{d(R, T ), d(T, S)} holds is immediate by the definition of d, as is the fact that d is symmetric and 1-bounded.

To show completeness, assume that (R n ) n∈N is a Cauchy sequence in R. Without loss of generality we may assume that d(R n , R n+1 ) ≤ 2 -n holds for all n ∈ N, and therefore that (R n )

[n] = (R n+1 ) [n] for all n ≥ 0. Writing S n for (R n ) [n] , we define R ⊆ X by R def = n≥0 S n .
R is closed since each S n is closed. We now prove that R is non-empty, and therefore R ∈ R, by inductively constructing a sequence (x n ) n∈N with x n ∈ S n : Let x 0 be an arbitrary element in S 0 = X. Having chosen x 0 , . . . , x n , we pick some x n+1 ∈ S n+1 such that x n+1 n = x n ; this is always possible because S n = (S n+1 ) [n] by our assumption on the sequence (R n ) n∈N . Clearly this is a Cauchy sequence in X, and from S n ⊇ S n+1 it follows that (x n ) n≥k is in fact a sequence in S k for each k ∈ N. But then also lim n∈N x n is in S k for each k, and thus also in R.

We now prove that R is the limit of the sequence (R n ) n∈N . By definition of d it suffices § Recall that a relation is closed if it is closed under the limit operation.

to show that R

[k] = (R k ) [k] for all k ≥ 1, or equivalently, that R [k] = S k . From the definition of R, R ⊆ S k , which immediately entails R [k] ⊆ (S k ) [k] = S k .
To prove the other direction, i.e., S k ⊆ R [k] , assume that x ∈ S k . To show that x ∈ R [k] we inductively construct a Cauchy sequence (x n ) n≥k with x n ∈ S n , x k = x and x n+1 n = x n analogously to the one above. Then lim m x m is in S n for each n ≥ 0, and thus also in R. Since d X (x k , lim n≥k x n ) ≤ 2 -k by the ultrametric inequality,

x k ∈ R [k] , or equivalently, x ∈ R [k] .

Hereditarily monotone recursive worlds

We will now define the set of hereditarily monotonic functions W as a recursive predicate on the space X from Proposition 9. Let the function Φ : P(X) → P(X) on subsets of X be given by

Φ(R) = {ι(g) | ∀x, x 0 ∈ R. g(x) ⊆ g(x • x 0 )} .
The function restricts to a contractive function on R:

Lemma 12. If R ∈ R then Φ(R)

is non-empty and closed, and

R n = S implies Φ(R) n+1 = Φ(S). Proof. It is clear that Φ(R) = ∅ since ι(g) ∈ Φ(R) for every constant function g from 1 2 •X to URel (Heap). Limits of Cauchy chains in 1 2 •X → URel (Heap) are given pointwise, hence (lim n g n )(x) ⊆ (lim n g n )(x • x 0
) holds for all Cauchy chains (g n ) n∈N in Φ(R) and all x, x 0 ∈ R. This proves Φ(R) ∈ R.

We now show that Φ is contractive. To this end, let n ≥ 0 and assume R n = S. Let ι(g) ∈ Φ(R) [n+1] . We must show that ι(g) ∈ Φ(S) [n+1] . By definition of the closure operation there exists ι(f ) ∈ Φ(R) such that g and f are (n+1)-equal. Set h(w) = f (w) [n+1] . Then h and g are also (n+1)-equal, hence it suffices to show that ι(h) ∈ Φ(S). To establish the latter, let w 0 , w 1 ∈ S be arbitrary. By the assumption that R and S are n-equal there exist elements w ′ 0 , w ′ 1 ∈ R such that w ′ 0 n = w 0 and w ′ 1 n = w 1 holds in X, or equivalently, such that w ′ 0 and w 0 as well as w ′ 1 and w 1 are (n+1)-equal in 1 2 • X. By the non-expansiveness of •, this implies that also w

′ 0 • w ′ 1 and w 0 • w 1 are (n+1)-equal in 1 2 • X. Since f (w 0 ) n+1 = f (w ′ 0 ) ⊆ f (w ′ 0 • w ′ 1 ) n+1 = f (w 0 • w 1 )
holds by the non-expansiveness of f and the assumption that ι(f ) ∈ Φ(R), we obtain the required inclusion h(w 0 ) ⊆ h(w 0 • w 1 ) by definition of h.

By Proposition 11 and the Banach theorem we can now define the hereditarily monotonic functions W as the uniquely determined fixed point of Φ.

Theorem 13 (Existence of hereditarily monotone recursive worlds). There exists a non-empty and closed subset W ⊆ X satisfying the condition

w ∈ W ⇔ ∃g. w = ι(g) ∧ ∀w 1 , w 2 ∈ W. g(w 1 ) ⊆ g(w 1 • w 2 ) .
Note that W thus constructed does not quite satisfy the conditions stated in Theorem 4: we do not have an isomorphism between W and the non-expansive and monotonic functions from W (viewed as an ultrametric space itself), but rather between W and all functions from X that restrict to monotonic functions whenever applied to hereditarily monotonic arguments. Keeping this in mind, we abuse notation and write

1 2 • W → mon URel (A) = {g : 1 2 • X → URel (A) | ∀w 1 , w 2 ∈ W. g(w 1 ) ⊆ g(w 1 • w 2 )} .
Then, for our particular application of interest, we also have to ensure that all the operations restrict appropriately (cf. Section 7 below). Here, as a first step, we show that the composition operation • restricts to W .

Lemma 14. For all n ∈ N, if w 1 , w 2 ∈ W then w 1 • w 2 ∈ W [n] . In particular, since W = n W [n] it follows that w 1 , w 2 ∈ W implies w 1 • w 2 ∈ W .
Proof. The proof is by induction on n. The base case is immediate as W

[0] = X. Now suppose n > 0 and let w 1 , w 2 ∈ W ; we must prove that w 1 • w 2 ∈ W [n] . Let w ′ 1 be such that ι -1 (w ′ 1 )(w) = ι -1 (w 1 )(w) [n] . Observe that w ′ 1 ∈ W , that w ′ 1 and w 1 are n-equal, and that w ′ 1 is such that n-equality of w, w ′ in 1 2 •X already implies ι -1 (w ′ 1 )(w) = ι -1 (w ′ 1 )(w ′ ). Since w ′
1 and w 1 are n-equivalent, the non-expansiveness of the composition operation implies

w 1 • w 2 n = w ′ 1 • w 2 . Thus it suffices to show that w ′ 1 • w 2 ∈ W = Φ(W ).
To see the latter, let w, w 0 ∈ W be arbitrary, and note that by induction hypothesis we have

w 2 • w ∈ W [n-1] . This means that there exists w ′ ∈ W such that w ′ n = w 2 • w holds in 1 2 • X, hence ι -1 (w ′ 1 • w 2 )(w) = ι -1 (w ′ 1 )(w 2 • w) * ι -1 (w 2 )(w) by definition of • = ι -1 (w ′ 1 )(w ′ ) * ι -1 (w 2 )(w) by w ′ n = w 2 • w ⊆ ι -1 (w ′ 1 )(w ′ • w 0 ) * ι -1 (w 2 )(w • w 0 ) by hereditariness = ι -1 (w ′ 1 )((w 2 • w) • w 0 ) * ι -1 (w 2 )(w • w 0 ) by w ′ n = w 2 • w = ι -1 (w ′ 1 • w 2 )(w • w 0 ) by definition of •.
Since w, w 0 were chosen arbitrarily, this calculation establishes

w ′ 1 • w 2 ∈ W .
Moreover, the BI algebra structure that exists on 1 2 • X → URel (Heap) by Proposition 3 restricts to the hereditarily monotone functions.

Proposition 15. 1 2 •W → mon URel (Heap) forms a complete BI algebra where the operations are non-expansive. Meets and joins are given by the pointwise extension of intersection and union on URel (Heap), and f ⇒ g is defined by (f ⇒ g)(x) = x0∈X f (x•x 0 ) ⇒ g(x • x 0 ) . Separating conjunction f * g and its unit I are defined pointwise, and the separating implication f - * g is defined by (f - * g)(x) = x0∈X f (x • x 0 ) - * g(x • x 0 ) from the separating implication on URel (Heap).

Step-indexed Possible World Semantics of Capabilities

In this section we prove the soundness of the calculus of capabilities. After defining the semantic domains for the interpretation of types and capabilities, we give the full syntax and typing rules for the system presented in Section 2. Then, using the hereditarily monotone recursive worlds W , we construct a model of types and capabilities based on the operational semantics.

Alternatively, it is possible to use the monotone recursive worlds from Section 5 instead. This would require only minor and straightforward modifications of the interpretation below.

Semantic domains and constructors

Let X ∈ CBUlt denote the solution to the ultrametric equation X ∼ = 1 2 • X → URel (Heap) from Proposition 9, and let W ∈ R(X) denote the subset of hereditarily monotone recursive worlds (Theorem 13).

We define semantic domains for the capabilities and the value and memory types,

Cap = 1 2 • W → mon URel (Heap) VT = 1 2 • W → mon URel (Val ) MT = 1 2 • W → mon URel (Val × Heap) , so that g ∈ Cap if and only if ι(g) ∈ W .
To define operations on the semantic domains that correspond to the syntactic type and capability constructors, we consider the lifting of (memory) types from values to expressions.

Definition 16 (Expression typing). Consider

f : 1 2 • X → URel (Val × Heap). The function E(f ) : X → URel (Exp × Heap) is defined by (k, (t, h)) ∈ E(f )(x) iff ∀j ≤ k, t ′ , h ′ . (t | h) -→ j (t ′ | h ′ ) ∧ (t ′ | h ′ ) irreducible ⇒ (k-j, (t ′ , h ′ )) ∈ w∈W f (x • w) * ι -1 (x • w)(emp) .
Note that it is here where the indexing by natural numbers that allows one to measure the distance between uniform relations is linked to the operational semantics of the programming language.

Also note that in this definition, f is a contractive function on X whereas E(f ) is merely non-expansive. This is because the conclusion uses the world x as a heap predicate, qua ι -1 (x • w)(emp), i.e. the scaling by 1/2 is undone, and the number j of steps taken in the reduction sequence may in fact be 0.

Lemma 17. Let f : 1 2 • X → URel (Val × Heap). Then E(f ) is non-expansive, and for all x ∈ X, E(f )(x) ∈ URel (Exp × Heap). Moreover, the assignment of E(f ) to f is non-expansive. Proof. Observe that f n = f ′ and x n = x ′ in X implies f (x • w) n = f ′ (x ′ • w) and ι -1 (x•w)(emp) n = ι -1 (x ′ •w)(emp), for any w ∈ W , by the non-expansiveness of f, f ′ and •. Thus E(f )(x) n = E(f ′ )(x ′ ).
In particular, for f = f ′ we obtain the non-expansiveness of E(f ), and for x = x ′ we obtain the non-expansiveness of E by definition of the sup metric.

Definition 18 (Capability and type constructors). In addition to separating conjunction and its unit, given in Proposition 15, we define the following operations.

Invariant extension Let

g : 1 2 • X → URel (A) and w ∈ W . We define g ⊗ w : 1 2 • X → URel (A) by (g ⊗ w)(x) = g(w • x)
Separation Let p ∈ URel (A × Heap) and r ∈ URel (Heap). We define p * r ∈ URel (A × Heap) by

p * r = {(k, (a, h • h ′ )) | (k, (a, h)) ∈ p ∧ (k, h ′ ) ∈ r}
This operation can be lifted pointwise, (g * c)(x) = g(x) * c(x) for g : Heap). For notational convenience we will sometimes view r ∈ URel (Heap) as the constant function that maps any x ∈ X to r, and thus write g * r for this pointwise lifting.

1 2 • X → URel (A × Heap) and c : 1 2 • X → URel (
Singleton capabilities Let v ∈ Val and g : 1 2 • X → URel (Val × Heap). We define {v : g} : 1 2 • X → URel (Heap) by {v : g}(x) = {(k, h) | (k, (v, h)) ∈ g(x)} Name abstraction Let F : Val → ( 1 2 • X → URel (A))
, where Val is viewed as a discrete ultrametric space. Then ∃F :

1 2 • X → URel (A) is defined by (∃F )(x) = v∈Val F (v)(x)
Universal quantification Let S be a set (viewed as an object of CBUlt with discrete metric), and let

F : S → ( 1 2 • X → URel (A)). We define ∀F : 1 2 • X → URel (A) by (∀F )(x) = s∈S F (s)(x) Recursion Let F : ( 1 2 • X → URel (A)) → ( 1 2 • X → URel (A)) be a contractive function. We define fix F : 1 2 • X → URel (A) by fix F = the unique g : 1 2 • X → URel (A) such that g = F (g) which exists by the Banach fixed point theorem. Sum types Let g 1 , g 2 : 1 2 • X → URel (Val ). We define g 1 + g 2 : 1 2 • X → URel (Val ) by (g 1 + g 2 )(x) = {(k, inj i v) | ∀j < k. (j, v) ∈ g i (x)} Similarly, for g 1 , g 2 : 1 2 • X → URel (Val × Heap) we define g 1 + g 2 : 1 2 • X → URel (Val × Heap) by (g 1 + g 2 )(x) = {(k, (inj i v, h)) | ∀j < k. (j, (v, h)) ∈ g i (x)} Product types Let g 1 , g 2 : 1 2 • X → URel (Val ). We define g 1 × g 2 : 1 2 • X → URel (Val ) by (g 1 × g 2 )(x) = {(k, v 1 , v 2 ) | ∀j < k. (j, v 1 ) ∈ g 1 (x) ∧ (j, v 2 ) ∈ g 2 (x)} Similarly, for g 1 , g 2 : 1 2 • X → URel (Val × Heap) we define g 1 × g 2 : 1 2 • X → URel (Val × Heap) by (g 1 × g 2 )(x) = {(k, ( v 1 , v 2 , h 1 • h 2 )) | ∀j < k. (j, (v i , h i )) ∈ g i (x)} Arrow types Let g 1 , g 2 : 1 2 • X → URel (Val × Heap). We define g 1 → g 2 : 1 2 • X → URel (Val ) on x ∈ X by {(k, fun f (y) = t) | ∀j < k. ∀w ∈ W. ∀r ∈ URel (Heap). ∀v, h. (j, (v, h)) ∈ g 1 (x • w) * ι -1 (x • w)(emp) * r ⇒ (j, (t[f :=fun f (y) = t, y:=v], h)) ∈ E(g 2 * r)(x • w)} Reference types Let g : 1 2 • X → URel (Val × Heap). We define ref(g) in 1 2 • X → URel (Val × Heap) by ref(g)(x) = {(k, (l, h • [l → v])) | ∀j < k. (j, (v, h)) ∈ g(x)}
The case for arrow types realizes the key ideas of our model that we have described in Section 3 as follows. First, the universal quantification over w ∈ W and subsequent use of the world x • w builds in monotonicity, and intuitively means that g 1 → g 2 is parametric in (and hence preserves) invariants that have been added by the procedure's context. In particular, the definition states that procedure application preserves this invariant, when viewed as the predicate ι -1 (x • w)(emp). By also conjoining r as an invariant we "bake in" the first-order frame property, which results in a subtyping axiom χ 1 → χ 2 ≤ χ 1 * C → χ 2 * C in the type system. The existential quantification over w ′ , in the definition of E, allows us to "absorb" a part of the local heap description into the world. Finally, the quantification over indices j < k in the definition of g 1 → g 2 achieves that (g 1 → g 2 )(x) is uniform. There are three reasons why we require that j be strictly less than k. Technically, as for the definition of E, the use of ι -1 (x • w) in the definition undoes the scaling by 1/2, and j < k ensures the non-expansiveness of g 1 → g 2 as a function 1/2 • X → URel (Val ). Moreover, it lets us prove the typing rule for recursive functions by induction on k. Finally, it means that → is a contractive type constructor, which justifies the formal contractiveness assumption about arrow types that we made earlier. Intuitively, the use of j < k for the arguments suffices since application consumes a step. The use of j < k in sum, product, and reference types instead of j ≤ k ensures that these constructors are contractive in their arguments and not merely non-expansive.

The definition of ref(g) builds in separation. If the semantic memory type g describes a value v together with a heap fragment h, then the semantic memory type ref(g) describes a memory location l together with the heap fragment h

• [l → v]. By definition, the combination h • [l → v]
exists only if l is not in the domain of h. The definition of g 1 × g 2 , in the case of value/heap pairs, also builds in separation. Later ( §7.2), we use these definitions to interpret syntactic memory types, so (for instance) the syntactic memory type ref (ref int × ref int) describes a configuration that must consist of three distinct memory cells. In short, together, the memory type constructors ×, +, ref, and µ describe the (mutable) algebraic data structures without sharing or cycles.

This does not mean that the type system or the semantic model are unable to describe cyclic structures in the heap. A memory cell that contains its own address, for instance, can be described by the memory type ∃σ.([σ] * {σ : ref [σ]}). (It is not described by the recursive memory type µβ.ref β, which describes an infinite chain of pairwise distinct memory cells, and is therefore empty!) As illustrated by this example, singleton regions are a mechanism for describing situations where there is sharing. (They are inspired by earlier work on alias types [33].) What the present type system lacks is a mechanism for describing situations where there is aliasing, that is, situations where it is not statically known exactly whether two memory addresses are equal or distinct. As a simple example of such a situation, think of a circular list of references, where the length of the list is not statically known. In order to describe such a data structure, multiple possibilities exist: for instance, one could extend the system with Charguéraud and Pottier's group regions; or one could extend it with untagged unions, of the form θ 1 ∨ θ 2 , use untagged unions to define untagged list segments in the style of separation logic [29], and use a memory type of the form ∃σ.([σ] * {σ : listseg σ}) to describe a circular list of unknown length. The type system presented here offers neither of these features. However, our semantic model should be able to support them without difficulty.

Lemma 19 (Well-definedness). The operations given in Definition 18 are well-defined, i.e., each operation is a non-expansive function that maps into uniform relations of the right kind. Moreover, they restrict to non-expansive operations on monotonic functions:

-If g : 1 2 • W → mon URel (A) then g ⊗ w : 1 2 • W → mon URel (A)
. The operation g, w → g ⊗ w is non-expansive in g and contractive in w.

-If g : 1 2 • W → mon URel (A × Heap) and c ∈ Cap then g * c : 1 2 • W → mon URel (A × Heap). The operation g, c → g * c is non-expansive in g and c.

-If g ∈ MT then {v : g} ∈ Cap. The operation g → {v : g} is non-expansive.

-

If F : Val → ( 1 2 • W → mon URel (A)) then ∃F : 1 2 • W → mon URel (A). The operation F → ∃F is non-expansive. -If F : S → ( 1 2 • W → mon URel (A)) then ∀F : 1 2 • W → mon URel (A). The operation F → ∀F is non-expansive. -If F : ( 1 2 • W → mon URel (A)) → ( 1 2 • W → mon URel (A)) is contractive then fix F : 1 2 • W → mon URel (A). The operation F → fix F is non-expansive. -If g 1 , g 2 ∈ VT then g 1 + g 2 ∈ VT, and if g 1 , g 2 ∈ MT then g 1 + g 2 ∈ MT. The operations g 1 , g 2 → g 1 + g 2 are contractive in g 1 and g 2 . -If g 1 , g 2 ∈ VT then g 1 × g 2 ∈ VT, and if g 1 , g 2 ∈ MT then g 1 × g 2 ∈ MT. The operations g 1 , g 2 → g 1 × g 2 are contractive in g 1 and g 2 . -If g 1 , g 2 ∈ MT then g 1 → g 2 ∈ VT. The operation g 1 , g 2 → g 1 → g 2 is contractive in g 1 and g 2 . -If g ∈ MT then ref(g) ∈ MT. The operation g → ref(g) is contractive.
Proof. We consider the cases of invariant extension and sum types in detail.

-Let g : 1 2 • X → URel (A) and w ∈ W . Then, by definition, (g ⊗ w)(x) = g(w • x)
is a uniform relation on A for any x ∈ X. By the non-expansiveness of g and • (cf. Lemma 10), g ⊗ w is a non-expansive function.

Next, we show that ⊗ restricts to the monotone functions. Assume g : 1 2 • W → mon URel (A). To show g ⊗ w : 1 2 • W → mon URel (A) we must prove (g ⊗ w)(w 1 ) ⊆ (g ⊗ w)(w 1 • w 2 ) for all w 1 , w 2 ∈ W . Note that w ∈ W , and thus Lemma 14 shows w • w 1 ∈ W . Hence, g(w • w 1 ) ⊆ g(w • w 1 • w 2 ) by the assumption g : 1 2 • W → mon URel (A), and the claim follows from the definition of g ⊗ w.

We show that ⊗ is non-expansive in its first and contractive in its second argument. If

g n = g ′ then (g ⊗ w)(x) n = (g ′ ⊗ w)(x)
by definition of the sup-metric, which means that g → g ⊗ w is non-expansive. Finally, assuming that we have

w n = w ′ for w, w ′ ∈ W , then w • x n+1 = w ′ • x holds in 1
2 • X for any x ∈ X by the non-expansiveness of • and the scaling operation. Thus (g ⊗ w)(x) n+1 = (g ⊗ w ′ )(x) follows from the nonexpansiveness of g, and since x was chosen arbitrarily the definition of the sup-metric yields g ⊗ w

n+1 = g ⊗ w ′ which shows that w → g ⊗ w is contractive. -Let g 1 , g ′ 1 , g 2 , g ′ 2 : 1 2 • X → URel (Val ), and assume g 1 n = g ′ 1 and g 2 n = g ′ 2 .
Then, for any x, x ′ ∈ X such that x n = x ′ holds with respect to the metric on 1 2 • X, the non-expansiveness of g 1 , g 2 yields g 1 (x)

n = g 1 (x ′ ) and g 2 (x) n = g 2 (x ′ ). Hence, (j, v) ∈ g 1 (x) if and only if (j, v) ∈ g ′ 1 (x ′ ) for any j < n, and (j, v) ∈ g ′ 2 (x) if and only if (j, v) ∈ g ′ 2 (x ′ ) for any j < n. By definition of g 1 + g 2 and g ′ 1 + g ′ 2 it follows that (g 1 + g 2 )(x) [n+1] = (g ′ 1 + g ′ 2 )(x ′ ) [n+1] , i.e., that (g 1 + g 2 )(x) n+1 = (g 1 + g 2 )(x ′
). From this observation, taking g 1 = g ′ 1 and g 2 = g ′ 2 , it follows immediately that g 1 + g 2 is non-expansive. Moreover, taking x = x ′ , the definition of the sup-metric shows that the assignment g 1 , g 2 → g 1 + g 2 is contractive. Since g 1 (x) and g 2 (x) are uniform relations, it is easy to see that (k, v) ∈ (g 1 + g 2 )(x) implies (j, v) ∈ (g 1 + g 2 )(x) for all j ≤ k. Finally, from the definition of g 1 + g 2 it follows that g 1 , g 2 ∈ VT implies g 1 + g 2 ∈ VT.

The remaining cases are similar.

Type system and soundness

The syntax and typing rules of Charguéraud and Pottier's capability type system are given in Figures 7, 8 and9. In addition to the typing rules given earlier, the capability type system also features subtype and subcapability relations. Figure 10 shows some of the axioms that induce these relations. Axioms 23 and 24 allow eliminating a universal quantifier and introducing an existential quantifier. (We write [ξ := . . .] for a substitution that replaces the variable ξ with an object of the appropriate syntactic category, depending on the nature of ξ.) Axiom ( 25) is a variant of the first-order (shallow) frame rule from Figure 6. ¶ Axiom (26) allows us to "garbage-collect" capabilities for parts of the ¶ The deep variant of this axiom, Pottier [26] gives a counterexample based on this axiom and the anti-frame rule, and a similar counterexample that does not use the anti-frame rule can be constructed along the lines of [30, Proposition 1].

χ 1 → χ 2 ≤ (χ 1 • C) → (χ 2 • C), is not sound in the capability calculus.
heap that are no longer needed. This axiom only holds in a "non-tight" interpretation of assertions like we use it here. Axioms ( 27) and ( 28) permit to translate back and forth between a value type τ and a singleton type [σ] (together with a capability for σ). Many more axioms could be listed, which (we believe) can be proven sound with respect to the model and can conceivably be useful in practice. Attempting to provide an exhaustive list would be a somewhat tedious exercise; we refer the reader to the papers by Charguéraud and Pottier [11] and Pottier [27], where many axioms are given. The relation ≤ is defined inductively by inference rules (not shown here) which state that all type and capability constructors are covariant, with two exceptions: as usual, arrow types are contravariant in their first argument, and ⊗ is invariant in its second argument.

The rules that define the typing judgement for values (∆ ⊢ v : τ ) include a rule for introducing a universal quantifier, whereas the rules that define the typing judgement for terms (Γ t : χ) do not include such a rule. This is the value restriction [35]. Charguéraud and Pottier's system, without the anti-frame rule, does not require this restriction [11], but once the anti-frame rule is introduced, the restriction becomes necessary for soundness, as noted and proved by Pottier [26,27]. It is in a sense obvious why this restriction is required: the anti-frame rule allows encoding weak references, and it is well-known that the combination of weak references and unrestricted polymorphism is unsound [35]. For a more technical explanation why the restriction is necessary, one can check that our model does not validate a universal quantifier introduction rule for terms (because it would require commuting the existential quantifier over w in Definition 16 of semantic expression typing and the universal quantifier in Definition 18 of semantic universal quantification).

Using the operations given in Definition 18, the interpretation of capabilities and types is defined in Figure 11 by induction on the syntax. The interpretation depends on an environment η, which maps region names σ ∈ RegName to closed values η(σ) ∈ Val , capability variables γ to semantic capabilities η(γ) ∈ Cap, and type variables α and β to semantic types η(α) ∈ VT and η(β) ∈ MT. By Lemma 19 we obtain interpretations C η ∈ Cap, τ η ∈ VT, and θ η ∈ MT. Moreover, Lemma 19 shows that whenever C is formally contractive in ξ then g → C η[ξ:=g] is contractive (and similarly for formally contractive types τ and χ), which guarantees that the fixed points in Figure 11 are well-defined.

The structural equivalences given in Figure 5 can be verified with respect to this inter-

The references in Charguéraud and Pottier's system [11] are strong references. The type system regards reference types as affine memory types, not value types, and the system keeps explicit track of the ownership of reference cells. For this reason, the type system allows strong (type-changing) updates, and for the same reason, it allows reference types to be considered covariant. (If θ 1 is a subtype of θ 2 , then changing the type of a reference cell from ref θ 1 to ref θ 2 can be viewed as a particular case of a strong update, where no write instruction is required at runtime, because the content of the cell does not change.) The references in ML's type system, on the other hand, are weak references. They do not have an explicit owner: they are ordinary values, and can be duplicated. For this reason, they cannot admit strong updates, and must be invariant. In Pottier's encoding of weak references in terms of strong references and the anti-frame rule [24], the invariance requirement arises from the use of the anti-frame rule, which requires that the hidden state be described by an invariant.

(x : τ ) ∈ ∆ ∆ ⊢ x : τ ∆ ⊢ : 1 ∆ ⊢ v : τi ∆ ⊢ (inj i v) : (τ1 + τ2) ∆ ⊢ v1 : τ1 ∆ ⊢ v2 : τ2 ∆ ⊢ v1, v2 : (τ1 × τ2) ∆, f : χ1 → χ2, x : χ1 t : χ2 ∆ ⊢ fun f (x) = t : χ1 → χ2 ∀-Intro ∆ ⊢ v : τ ξ / ∈ ∆ ∆ ⊢ v : ∀ξ.τ Deep frame (val) ∆ ⊢ v : τ ∆ ⊗ C ⊢ v : τ ⊗ C Sub (val) ∆ ⊢ v : τ ′ τ ′ ≤ τ ∆ ⊢ v : τ
Lemma 20. For all C 1 , C 2 , C 3 , C 1 • (C 2 • C 3 ) = (C 1 • C 2 ) • C 3 .
Proof. We prove the following claim: for all

C, C ′ , ι C • C ′ = ι C • ι C ′ . It suffices to show C • C ′ η w = ι -1 (ι C η • ι C ′ η )(w)
for all η and w, and this follows from the defining equation for •:

ι -1 (ι C η • ι C ′ η )(w) = ι -1 (ι C η )(ι C ′ η • w) * ι -1 (ι C ′ η )(w) = ( C η ⊗ ι C ′ η )(w) * C ′ η (w) = C ⊗ C ′ * C ′ η (w) = C • C ′ η (w) To prove the lemma, it suffices to prove ι C 1 • (C 2 • C 3 ) = ι (C 1 • C 2 ) • C 3 .
By the above claim, this is a consequence of the associativity of • on X.

Most of the remaining equations in Figure 5 (as well as other equivalences that appear in [11,24]) are easy consequences of the pointwise definition of the operations in Definition 18. We consider the distribution axiom for arrow types, which is more involved: Proof. The lemma follows from the following claim.

Lemma 21. For all χ 1 , χ 2 and C, (χ 1 → χ 2 ) ⊗ C = (χ 1 • C) → (χ 2 • C) . Γ t : χ Sub (comp) Γ ′ t : χ ′ Γ ≤ Γ ′ χ ′ ≤ χ Γ t : χ
∀g 1 , g 2 ∈ MT. ∀c ∈ Cap. (g 1 → g 2 ) ⊗ ι(c) = (g 1 ⊗ ι(c) * c) → (g 2 ⊗ ι(c) * c)
We prove the inclusion from left to right. For the proof, let x ∈ X, k ∈ N and assume (k, (fun

f (y) = t)) ∈ ((g 1 → g 2 ) ⊗ ι(c))(x) = (g 1 → g 2 )(ι(c) • x). We must show that (k, (fun f (y) = t)) ∈ (g 1 ⊗ ι(c) * c) → (g 2 ⊗ ι(c) * c). To this end, let j < k, w ∈ W , Capabilities, C η : 1/2 • W →mon URel (Heap) C1 ⊗ C2 η = C1 η ⊗ ι( C2 η ) ∅ η = I C1 * C2 η = C1 η * C2 η {σ : θ} η = {η(σ) : θ η } γ η = η(γ) ∃σ.C η = ∃(λv ∈ Val . C η[σ:=v] ) µγ.C η = fix(λc ∈ Cap. C η[γ:=c] ) ∀σ.C η = ∀(λv ∈ Val . C η[σ:=v] ) Value types, τ η : 1/2 • W →mon URel (Val ) τ ⊗ C η = τ η ⊗ ι( C η ) 0 η = λw. ∅ 1 η = λw. N × { } int η = λw. N × {n | n ∈ Z} [σ] η = λw. N × {η(σ)} τ1 + τ2 η = τ1 η + τ2 η τ1 × τ2 η = τ1 η × τ2 η χ1 → χ2 η = χ1 η → χ2 η α η = η(α) µα.τ η = fix(λg ∈ VT. τ η[α:=g] ) ∀σ.τ η = ∀(λv ∈ Val . τ η[σ:=v] ) Memory types, θ η : 1/2 • W →mon URel (Val × Heap) θ ⊗ C η = θ η ⊗ ι( C η ) θ1 + θ2 η = θ1 η + θ2 η τ η = λw.{(k, (v, h)) | (k, v) ∈ τ η w} θ1 × θ2 η = θ1 η × θ2 η ref θ η = ref θ η θ * C η = θ η * C η β η = η(β) ∃σ.θ η = ∃(λv ∈ Val . θ η[σ:=v] ) µβ.θ η = fix(λg ∈ MT. θ η[β:=g] ) ∀σ.θ η = ∀(λv ∈ Val . θ η[σ:=v] ) Value contexts, ∆ η : 1/2 • W →mon URel (Env ) ∆ ⊗ C η = ∆ η ⊗ ι( C η ) ∅ η = λw.N × {[ ]} ∆, x:τ η = λw.{(k, ρ[x → v]) | (k, ρ) ∈ ∆ η w ∧ (k, v) ∈ τ η w} Affine contexts, Γ η : 1/2 • W →mon URel (Env × Heap) Γ ⊗ C η = Γ η ⊗ ι( C η ) ∅ η = λw.N × ({[ ]} × Heap) Γ, x:χ η w = λw.{(k, (ρ[x → v], h • h ′ )) | (k, (ρ, h)) ∈ Γ η w ∧ (k, (v, h ′ )) ∈ χ η w} Γ * C η = Γ η * C η
(j, (v, h)) ∈ (g 1 ⊗ ι(c) * c)(x • w) * ι -1 (x • w)(emp) * r = g 1 (ι(c) • x • w) * c(x • w) * ι -1 (x • w)(emp) * r = g 1 (ι(c) • x • w) * ι -1 (ι(c) • x • w)(emp) * r .
Then, by assumption, (j, (t[f :=fun f (y) = t, y:=v], h)) ∈ E(g 2 * r)(ι(c)•x•w). By unfolding the definition of E, the latter is seen to be equivalent to

(j, (t[f :=fun f (y) = t, y:=v], h)) ∈ E(g 2 ⊗ ι(c) * c * r)(x • w) ,
and thus (k, (fun

f (y) = t)) ∈ (g 1 ⊗ ι(c) * c) → (g 2 ⊗ ι(c) * c).
The other inclusion is proved similarly.

We give the semantics of typing judgements next. The semantics of a typing judgement for values simply establishes truth with respect to all worlds w, environments η, and indices k ∈ N:

|= (∆ ⊢ v : τ ) ⇐⇒ ∀η. ∀w. ∀k. ∀ρ. (k, ρ) ∈ ∆ η w ⇒ (k, ρ(v)) ∈ τ η w
Here ρ(v) means the application of the substitution ρ to v.

The semantics of the typing judgement for expressions mirrors the interpretation of the arrow case for value types, in that there is also a quantification over heap predicates r ∈ URel (Heap) and an existential quantification over w ′ ∈ W through the use of E: |= (Γ t : χ) ⇐⇒ ∀η. ∀w ∈ W. ∀k. ∀ρ. ∀h. ∀r ∈ URel (Heap).

(k, (ρ, h)) ∈ Γ η w * ι -1 (w)(emp) * r ⇒ (k, (ρ(t), h)) ∈ E( χ η * r)(w)
The universal quantification over worlds w ensures the soundness of the deep frame rule, and the universal quantification over heap predicates r validates the shallow frame rule. The existential quantifier plays an important part in the verification of the anti-frame rule below.

In the remainder of this section we prove soundness of the calculus of capabilities. Note that soundness in particular means that a well-typed closed program is safe to execute (does not go wrong).

Theorem 22 (Soundness).

-

If ∆ ⊢ v : τ then |= (∆ ⊢ v : τ ). -If Γ t : χ then |= (Γ t : χ).
In particular, if ∅ ⊢ t : χ is a closed program that does not contain any locations, and if

(t | h) -→ * (t ′ | h ′ ) where (t ′ | h ′ ) is irreducible, then t ′ is a value.
To prove the theorem, we show that each typing rule preserves the truth of judgements. The proof of the frame rules is straightforward.

Lemma 23 (Soundness of the shallow frame rule). Suppose |= (Γ t : χ). Then |= (Γ * C t : χ * C). Now observe that, for any w ′ , we have

χ ⊗ C * C η (w 1 • w ′ ) * ι -1 (w 1 • w ′ )(emp) = χ η (ι( C η ) • w 1 • w ′ ) * C η (w 1 • w ′ ) * ι -1 (w 1 • w ′ )(emp) = χ η (ι( C η ) • w 1 • w ′ ) * ι -1 (ι( C η ) • w 1 • w ′ )(emp) = χ η (ι(w • w 2 • w ′ ) * ι -1 (ι(w • w 2 • w ′ )(emp) since ι( C η ) • w 1 = w • w 2 . Setting w ′′ def = w 2 • w ′ one obtains that the last line equals χ η (w • w ′′ ) * ι -1 (w • w ′′ )(emp) .
Thus, (33) entails that (k-j, (t

′ , h ′ )) is in w ′′ χ η (w • w ′′ ) * ι -1 (w • w ′′ )(emp)
* r, and we are done.

Remark 27 (Monotonicity). Note that it is in the above proof for the anti-frame rule where the monotonicity condition of the recursive worlds is exploited to establish (31). Monotonicity of C is also used to prove the shallow frame rule in Lemma 23 (and the first-order frame axiom in Proposition 28 below). However, this is only necessary because of the existential quantifier that is implicitly used in the postcondition, via the definition of E(•). In a system without anti-frame rule, the quantifier can be dropped from the definition of E(•) and no monotonicity condition of C is needed [6,30].

We omit the proofs for the remaining typing rules. Using the model, we can also show that subtyping is sound. Recall that ≤ is an inductively defined relation on syntactic type expressions, defined by axioms (as shown in Figure 10) and rules that propagate those axioms through type constructors (omitted for brevity). One can show that syntactic subtyping is sound:

Proposition 28 (Soundness of subtyping). The three kinds of subtyping relations are sound. More precisely, for all η and w:

1 C ≤ C ′ implies C η w ⊆ C ′ η w, 2 τ ≤ τ ′ implies τ η w ⊆ τ ′ η w, 3 θ ≤ θ ′ implies θ η w ⊆ θ ′ η w.
Proof. The three statements are proved simultaneously by induction on the derivation of the subtyping judgement in question. One must show that the axioms in Figure 10 hold with respect to the interpretation given in Figure 11, and that all of the inference rules that define the subtyping judgements preserve these inclusions. We show three sample cases: Axiom (25) is sound. We have to show that for all η and w ∈

W , χ 1 → χ 2 η w ⊆ (χ 1 * C) → (χ 2 * C) η w. Assume (k, fun f (x) = t) ∈ χ 1 → χ 2 η w. To see that (k, fun f (x) = t) is also in the set (χ 1 * C) → (χ 2 * C) η w, suppose that j < k, w 0 ∈ W and r ∈ URel (Heap), and let (j, (v, h)) ∈ χ 1 * C η (w • w 0 ) * ι -1 (w • w 0 )(emp) * r = χ 1 η (w • w 0 ) * ι -1 (w • w 0 )(emp) * (r * C η (w • w 0 )) We must show that (j, (t[f :=fun f (x) = t, x:=v], h)) ∈ E( χ 2 * C η * r)(w•w 0 ). So assume that (t[f :=fun f (x) = t, x:=v] | h) -→ i (t ′ | h ′ ) for some i ≤ j and some irreducible configuration (t ′ | h ′ ). By unfolding the definition of χ 1 → χ 2 η w, we obtain (j, (t[f :=fun f (x) = t, x:=v], h)) ∈ E( χ 2 η * (r * C η (w • w 0 )))(w • w 0 )
and hence that there exists w 1 ∈ W such that

(j -i, (t ′ , h ′ )) ∈ χ 2 η (w • w 0 • w 1 ) * ι -1 (w • w 0 • w 1 )(emp) * r * C η (w • w 0 ) Since w • w 0 ⊑ w • w 0 • w 1 entails C η (w • w 0 ) ⊆ C η (w • w 0 • w 1 ) by monotonicity of C η , one obtains (j -i, (t ′ , h ′ )) ∈ χ 2 * C η (w • w 0 • w 1 ) * ι -1 (w • w 0 • w 1 )(emp) * r which yields (j, (t[f :=fun f (x) = t, x:=v], h)) ∈ E( χ 2 * C η * r)(w • w 0 ).
Axiom 26 is sound. We have to prove for all η and w ∈ W , C η w ⊆ ∅ η w. This follows simply from the definition ∅ η w = N × Heap.

The rule for covariant subtyping of ⊗, concluding τ ⊗ C ≤ τ ′ ⊗ C from τ ≤ τ ′ , is sound. Assume that τ η w ⊆ τ ′ η w holds for all η and w ∈ W . Then we have to show that τ ⊗ C η w ⊆ τ ′ ⊗ C η w for all η and w ∈ W . By definition, τ ⊗

C η w = τ η (ι C η • w) and τ ′ ⊗ C η w = τ ′ η (ι C η • w).
Thus, the statement follows by instantiating the universally quantified world in the assumption by ι C η • w.

The soundness of the subsumption rules in Figures 8 and9 is an immediate consequence of Proposition 28.

Generalized Frame and Anti-frame Rules

The frame and anti-frame rules allow for hiding of invariants. However, to hide uses of local state, say for a function, it is, in general, not enough only to allow hiding of global invariants that are preserved across arbitrary sequences of calls and returns. For instance, consider the function f with local reference cell r: termination. However, there could well be re-entrant calls to f such that {σ : ref (int 0)} is not an invariant for those calls.

Thus Pottier [25] proposed two extensions to the anti-frame rule that allow for hiding of families of invariants. The first idea is that each invariant in the family is a local invariant that holds for one level of the recursive call of a function. This extension allows us to hide "well-bracketed" [12] uses of local state. For instance, the N-indexed family of invariants I n = {σ : ref (int n)} can be used for (34); see the examples in [25]. The second idea is to allow each local invariant to evolve in some monotonic fashion; this allows us to hide even more uses of local state. For instance, for f defined by let r = ref 1 in fun f (g) = (set r, 0 ; g ; set r, 1 ; g ) we may wish to capture the fact that the cell r : [σ] stores 1 after f (g) returns. Intuitively, this holds since the calls to g may at most bump up the value of r from 0 to 1 (through recursive calls to f ), and this fact can be captured in the type system by considering the {0, 1}-indexed family of invariants I n = {σ : ref (int n)} once we allow that calls with I i may return with I j for j ≥ i. The idea is related to the notion of evolving invariants for local state in recent work on reasoning about contextual equivalence [1,12].

In summary, we want to allow the hiding of a family of capabilities (I i) i∈κ indexed over a preordered set (κ, ≤). The preorder is used to capture that the local invariants can evolve in a monotonic fashion, as expressed in the new definition of the action of ⊗ on function types (note that I on the right-hand side of ⊗ now has kind κ → cap):

(χ 1 → χ 2 ) ⊗ I = ∀i. (χ 1 ⊗ I) * I i → ∃j ≥ i. ((χ 2 ⊗ I) * I j) (35)
Observe how this definition captures the intuitive idea: if the invariant I i holds when the function is called then, upon return, we know that an invariant I j (for j ∈ κ, j ≥ i) holds. Different recursive calls may use different local invariants due to the quantification over i. The generalized frame and anti-frame rules are given in Figure 12. We now show how to extend our model of the type and capability calculus to accommodate hiding of such more expressive families of invariants. Naturally, the first step is to refine our notion of world, since the worlds are used to describe hidden invariants.

Generalized recursive worlds and generalized world extension

Suppose K is a (small) collection of preordered sets. We write K * for the finite sequences over K, ε for the empty sequence, and use juxtaposition to denote concatenation. For convenience, we will sometimes identify a sequence α = κ 1 , . . . , κ n over K with the preorder κ 1 × • • • × κ n . As in Section 6, we define the worlds for the Kripke model in two steps, starting from an equation without any monotonicity requirements: † † CBUlt has all non-empty coproducts, and there is a unique solution to the two equations

X ∼ = α∈K * X α , X κ1,...,κn = (κ 1 × • • • × κ n ) → ( 1 2 • X → URel (Heap)) , (36)
with isomorphism ι : α∈K * X α → X in CBUlt, where each κ ∈ K is equipped with the discrete metric. Each X α consists of the α-indexed families of (world-dependent) predicates so that, in comparison to Section 6, X consists of all these families rather than individual predicates. Note that, by definition of the metric on X, if x n = x ′ holds for n > 0 and x = ι α, g and x ′ = ι α ′ , g ′ , then α = α ′ and g i n = g ′ i for all i ∈ α. The composition operation • : X × X → X is now given by x 1 • x 2 = ι( α 1 α 2 , g ) where α i , g i = ι -1 (x i ), and where g ∈ X α1α2 is defined by

g(i 1 i 2 )(x) = g 1 (i 1 )(x 2 • x) * g 2 (i 2 )(x) . for i 1 ∈ α 1 , i 2 ∈ α 2 .
That is, the combination of an α 1 -indexed family g 1 and an α 2 -indexed family g 2 is a family g over α 1 α 2 , but there is no interaction between the index components i 1 and i 2 : they concern disjoint regions of the heap. The composition operation is defined as the fixed point of a contractive function as in Lemma 10, it can be shown associative, and it has a left and right unit given by emp = ι( ε, I ). For g

: 1 2 • X → URel (A) we define the extension operation (g ⊗ x)(x ′ ) = g(x • x ′ )

Generalized hereditarily monotone recursive worlds

We will proceed as in Section 6, and carve out a subset of recursive worlds that satisfy a monotonicity condition.

To prove soundness of the anti-frame rule, and more specifically to establish the existence of commutative pairs, we need to know that the order in which the invariant families appear is irrelevant for the semantics of types and capabilities. The requirement is made precise by considering a partial equivalence relation ∼ on X, where ι( α 1 α 2 , g ) ∼ ι( α 2 α 1 , h ) holds if g(i 1 i 2 )(x 1 ) = h(i 2 i 1 )(x 2 ) for all i 1 ∈ α 1 , i 2 ∈ α 2 and x 1 ∼ x 2 , and insisting that semantic operations respect this relation. Note that the relation ∼ is recursive; we define it as the fixed point of a function Ψ on the non-empty and closed subsets of X × X.

Definition 29. Let Ψ : R(X × X) → R(X × X) be defined as follows. For all x, y ∈ X where x = ι α, g and y = ι β, h , (x, y) ∈ Ψ(R) if and only if there exists n ∈ N and a permutation π of 1, . . . , n such that α = α 1 . . . α n and β = α π(1) . . . α π(n) ; and for all i

1 ∈ α 1 , . . . , i n ∈ α n and all z, z ′ ∈ X, if (z, z ′ ) ∈ R then g(i 1 . . . i n )(z) = h(i π(1) . . . i π(n) )(z ′ ).
The function Ψ is contractive, and we define ∼ ⊆ X × X as its unique fixed point in URel (X × X), by the Banach fixed point theorem.

Lemma 30. ∼ is a partial equivalence relation on X:

1 x ∼ y implies y ∼ x; 2 x ∼ y and y ∼ z implies x ∼ z.

Proof. Since (∼ [n]

) n is a Cauchy chain in R(X × X) with limit ∼ given as the intersection of the ∼ [n] , part (1) of the lemma follows from the claim:

∀n ∈ N. ∀xy ∈ X. x ∼ y ⇒ (y, x) ∈ ∼ [n] ,
which is proved by induction on n.

The case n = 0 is immediate since ∼ [0] = X × X. For the case n > 0 let x ∼ y. For simplicity, we assume x = ι α 1 α 2 , p and y = ι α 2 α 1 , q . To prove (y, x) ∈ ∼ [n] it suffices to show that y ′ ∼ x ′ holds for y ′ = ι α 2 α 1 , q ′ and x ′ = ι α 1 α 2 , p ′ with q ′ (i 2 i 1 )(z) = q(i 2 i 1 )(z) [n] and p ′ (i 1 i 2 )(z) = p(i 1 i 2 )(z) [n] , since (y, x) n = (y ′ , x ′ ). To this end, let i 2 ∈ α 2 , i 1 ∈ α 1 , and suppose that z ∼ z ′ ; we must prove q ′ (i 2 i 1 )(z) = p ′ (i 1 i 2 )(z ′ ). By induction hypothesis, (z ′ , z) ∈ ∼ [n-1] , i.e., there exists u ′ ∼ u with u ′ n-1 = z ′ and u n-1 = z in X. Note that this means u ′ n = z ′ and u n = z holds in 1 2 • X. Thus

q(i 2 i 1 )(z) n = q(i 2 i 1 )(u) = p(i 1 i 2 )(u ′ ) n = p(i 1 i 2 )(z ′ )
by the non-expansiveness of p, q, and by the assumption x ∼ y. It follows that q ′ (i 2 i 1 )(z) = q(i 2 i 1 )(z) Proof sketch Similar to the proof of Lemma 14: We prove by induction that for all n ∈ N, if x ∼ x ′ and y ∼ y ′ then (x • y, x ′ • y ′ ) ∈ ∼ [n] , and use that ∼ is the intersection of all the ∼ [n] .

Next, we define the hereditarily monotone worlds. We ensure that these worlds w respect ∼ by requiring that they be self-related. The set W ⊆ X of these worlds is again defined as fixed point of a contractive function, on the closed and non-empty subsets of X.

Definition 32 (Generalized hereditarily monotone worlds). Let Φ : R(X) → R(X) be defined as follows. For all w ∈ X where w = ι α, g , w ∈ Φ(R) if and only if w ∼ w; and for all i ∈ α and all w 1 , w 2 ∈ R, g(i)(w 1 ) ⊆ g(i)(w 1 • w 2 ).

The function Φ is contractive, and we define the hereditarily monotone functions W = fix(Φ) = Φ(W ) by the Banach fixed point theorem.

Using Lemmas 30 and 31 it is not difficult to see that W is closed under the relation ∼. Moreover, as in Section 6, the composition operation restricts to the subset of hereditary monotone worlds.

Lemma 33. If w 1 , w 2 ∈ W then w 1 • w 2 ∈ W .

Proof sketch As in the proof of Lemma 14, we show that x, y ∈ W implies x • y ∈ W [n] for all n ∈ N by induction on n. Lemma 31 is used to show the additional requirement that the composition of x, y ∈ W is self-related, x • y ∼ x • y.

Semantics of capabilities and types.

The semantic domains for the interpretation of capabilities and types, with respect to the generalized worlds, now consist of the world-dependent functions that are both monotonic (with respect to the generalized hereditarily monotone worlds) and respect the relation ∼. More precisely, for a preordered set A we define 1 2 • W → mon URel (A) to consist of all those g : 1 2 • X → URel (A) where -∀x, x ′ ∈ X. x ∼ x ′ ⇒ g(x) = g(x ′ ); -∀w 1 , w 2 ∈ W. g(w 1 ) ⊆ g(w 1 • w 2 ). To define the interpretation of types, we first consider the following extension of memory types from values to expressions. Compared to the corresponding Definition 16 in Section 7, the extension now depends on the parameter i ∈ α.

Then we write

Definition 34 (Expression typing). Let f in 1 2 • W → mon URel (Val × Heap). Let x ∈ X and α, p = ι -1 (x). Let i ∈ α. Then E(f, x, i) ⊆ Exp × Heap is defined by (k, (t, h)) ∈ E(f, x, i) if and only if

∀j ≤ k, t ′ , h ′ . (t | h) -→ j (t ′ | h ′ ) ∧ (t ′ | h ′ ) irreducible ⇒ (k-j, (t ′ , h ′ )) ∈ w∈W, αβ,q =ι -1 (x•w), i1≥i, i2∈β f (x • w) * q(i 1 i 2 )(emp) .
This definition is well-behaved, in the sense that E(f, x, i) ⊆ Exp × Heap is a uniform subset (with respect to the discrete order on Exp × Heap, that it is non-expansive as a function in x, and that x ∼ x ′ implies E(f, x, i) = E(f, x ′ , i ′ ) for a suitable reordering i ′ of the parameters i.

Corresponding to the distribution axiom (35), the interpretation of arrow types bakes in the property that state changes on local state are captured by the local invariants: given x ∈ X, (k, fun f (y) = t) ∈ (f 1 → f 2 )(x) if and only if ∀j < k. ∀w ∈ W where ι -1 (x • w) = α, p . ∀r ∈ URel (Heap). ∀i ∈ α. ∀v, h.

(j, (v, h)) ∈ f 1 (x • w) * p(i)(emp) * r ⇒ (j, t[f :=fun f (y) = t, y:=v], h)) ∈ E(f 2 * r, x • w, i) .

Semantic operations corresponding to the other capability and type constructors can be defined analogous to Definition 18. It is easy to see that these operations respect the relation ∼. In fact, the only case that makes direct use of the parameter x ∈ W is the case of arrow types above where one quantifies universally over the elements of all instances of its precondition p and (via E) existentially over the elements of instances of its postcondition q; by definition of ∼ all these instances do not depend on reordering of the parameter.

As in Section 7, (semantic variants of) the distribution axioms for generalized invariants can be justified with respect to these operations. In particular, the axiom (35) holds since, given c ∈ κ → Cap and setting w def = ι( κ, c ),

(f 1 → f 2 ) ⊗ w = ∀ i∈κ (f 1 ⊗ w) * c i) → ∃ j≥i ((f 2 ⊗ w) * c j)
where ∀ and ∃ denote the pointwise intersection and union of world-indexed uniform predicates.

The semantics of value judgements ∆ ⊢ v : τ looks as before. The semantics of the expression typing judgement mirrors the new interpretation of arrow types, in the sense that there is now also a universal quantification over all possible instances i of the invariant family p represented by a world w ∈ W : |= (Γ t : χ) ⇐⇒ ∀η. ∀w ∈ W where w = α, p . ∀k ∈ N. ∀i ∈ α. ∀r ∈ URel (Heap).∀(k, (ρ, h)) ∈ Γ η w * p(i)(emp) * r.

(k, (ρ(t), h)) ∈ E( χ η * r, w, i).

We can now prove soundness of the generalized rules.

Theorem 35 (Soundness). The generalized frame and anti-frame rules are sound.

In particular, this theorem shows that all the reasoning about the use of local state in the (non-trivial) examples considered by Pottier in [25] is sound.

Proof sketch The case of the generalized frame rule is similar to the proof of Lemma 24. The soundness proof for the generalized anti-frame rule rests again on the existence of commutative pairs. Compared to the earlier Lemma 25, however, we can only prove a variant which states that commutativity holds up to the relation ∼: Let w 0 , w 1 ∈ W be families indexed over α 0 and α 1 , i.e., ι -1 (w 0 ) = α 0 , p 0 and ι -1 (w 1 ) = α 1 , p 1 for some p 0 and p 1 . Then there exist w ′ 0 , w ′ 1 ∈ W such that w ′ 0 = ι α 0 , λi.(p 0 i) ⊗ w ′ 1 , w ′ 1 = ι α 1 , λi.(p 1 i) ⊗ w ′ 0 , and w 0 • w ′ 1 ∼ w 1 • w 0 .

Since we insisted that the interpretations of types and capabilities respect ∼, this variant is sufficient to prove the soundness of the generalized anti-frame rule analogously to the proof of Lemma 26.

Conclusion and Future Work

We have developed a soundness proof of the frame and anti-frame rules in the expressive type and capability system of Charguéraud and Pottier, by constructing a Kripke model of the system. For our model, we have presented two novel approaches to construct the recursively defined set of worlds. ‡ ‡ The first approach is a (tedious) construction of an inverse limit in the category of complete, 1-bounded ultrametric spaces. In the second approach one defines the worlds as a recursive subset of a recursively defined metric space. This construction is simpler than the inverse limit construction, but requires an additional argument to show that the semantic operations restrict to this subset.

We have demonstrated that this approach generalizes, by also extending the model to show soundness of Pottier's generalized frame and anti-frame rules. More generally, we believe that the recursive worlds constructed in Sections 5 and 6 can be used, possibly in variations, to model various type system and program logics with hidden (higher-order) state.

Future work includes exploring some of the orthogonal extensions of the basic type and capability system that have been proposed in the literature: group regions [11], and fates and predictions [22]. The model that we have presented suggests to include separation logic assertions in the syntax of capabilities, and it would be interesting to work out such a program logic in detail.

Recently, Pottier has given an alternative soundness proof for a slightly different language, which includes group regions as well as the anti-frame rule, but does not include the generalized frame and anti-frame rules. This proof is based on progress and preservation properties, and has been formalized in the Coq proof assistant [27]. While we have not attempted a formalization of our model, we believe that this is possible based on the results of Varming et al. [4].

Fig. 1 .

 1 Fig. 1. Syntax

  (r : [σ]) * I let lock ( ) = . . . in lock , unlock : ((lock γ) ⊗ I) * I By exploiting the definition of I, the law [σ] ⊗ I = [σ], and the fact that ⊗ distributes over * , the left-hand side of this judgement can be re-arranged in the following manner: (r : [σ] * {σ : ref (flag γ)}) ⊗ I let lock ( ) = . . . in lock , unlock : ((lock γ) ⊗ I) * I

  the supremum always exists since it is taken over a bounded set in R).The notation x n = y means that d(x, y) ≤ 2 -n . Each relation n = is an equivalence relation because of the ultrametric inequality, and we refer to this relation as "n-equality." Since the distances are bounded by 1, x 0 = y always holds, and the n-equalities become finer as n increases. If x n = y holds for all n then x = y; this observation allows us to prove equalities by induction on n.

  which shows that x • y is a sequence in W . We also define e def = (e k ) k≥0 ∈ W by e k = I. Lemma 6. (W, •, e) is a monoid with non-expansive multiplication •.

  Fig. 7. Syntax of capabilities and types

Fig. 8 .

 8 Fig. 8. Typing rules for values

Fig. 9 .

 9 Fig. 9. Typing rules for expressions

Fig. 11 .

 11 Fig. 11. Interpretation of capabilities and types

  Fig. 12. Generalized frame and anti-frame rules

  [n] = p(i 1 i 2 )(u ′ ) [n] = p ′ (i 1 i 2 )(z ′ )i.e., we have shown y ′ ∼ x ′ .Part (2) follows from a similar argument, proving that for all n, x ∼ y and y ∼ z implies (x, z) ∈ ∼[n] .The composition operation respects this partial equivalence relation.Lemma 31. If x ∼ x ′ and y ∼ y ′ then x • y ∼ x ′ • y ′ .

  Cap = 1 2 • W → mon URel (Heap) VT = 1 2 • W → mon URel (Val ) MT = 1 2 • W → mon URel (Val × Heap) .Note that with this definition, g ∈ κ → Cap if and only if ι( κ, g ) ∈ W .

† The fact that ML-style untracked references can be encoded from strong references with the antiframe rule [24] also indicates that a monotonicity condition is required: Kripke models of ML-style references involve monotonicity in the worlds[1, 8].

∆, f : χ1 → χ2, x : χ1 t : χ2∆ ⊢ fun f (x) = t : χ1 → χ2 ∆ ⊢ v : χ1 → χ2 ∆, Γ t : χ1 ∆, Γ (v t) : χ2 Γ v : τ Γ ref v : ∃σ.[σ] * {σ : ref τ }

∆ ⊢ v : τ ∆ v : τ ∆ ⊢ v : χ1 → χ2 ∆, Γ t : χ1 ∆, Γ (v t) : χ2 Γ v : τ1 × τ2 Γ proj i v : τi ∆ ⊢ v1 : (∃σ1.[σ1] * {σ : [σ1] + 0} * {σ1 : θ1} * C) → χ ∆ ⊢ v2 : (∃σ2.[σ2] * {σ : 0 + [σ2]} * {σ2 : θ2} * C) → χ ∆, Γ v : [σ] * {σ : θ1 + θ2} * C ∆, Γ case(v1, v2, v) : χ Γ v : τ Γ ref v : ∃σ.[σ] * {σ : ref τ } Γ v : [σ] * {σ : ref τ } Γ get v : τ * {σ : ref τ } Γ v : ([σ] × τ2) * {σ : ref τ1} Γ set v : 1 * {σ : ref τ2} ∃-Elim (comp) Γ, x : χ1 t : χ2 σ ∈ Γ, χ2 Γ, x : ∃σ.χ1 t : χ2 ∃-Elim (cap) Γ * C t : χ2 σ ∈ Γ, χ2 Γ * (∃σ.C) t : χ2 Shallow frame Γ t : χ Γ * C t : χ * C Deep frame (comp) Γ t : χ (Γ ⊗ C) * C t : (χ ⊗ C) * C Anti-frame Γ ⊗ C t : (χ ⊗ C) * C

† † We believe that a variant of the inverse-limit construction in Section 5 could also be used to construct the worlds, but we have not checked all the details.

Proof. Assume |= (Γ t : χ). We prove |= (Γ * C t : χ * C). Let η be an environment, let w ∈ W , k ∈ N, r ∈ URel (Heap) and assume (k, (ρ, h)) ∈ Γ * C η (w) * ι -1 (w)(emp) * r = Γ η (w) * C η (w) * ι -1 (w)(emp) * r .

We can now instantiate the universally quantified r in the assumption |= (Γ t : χ) with C η (w) * r, and obtain (k, (ρ(t)

Lemma 24 (Soundness of the deep frame rule for expressions). Suppose |= (Γ

Next, we consider the anti-frame rule. Our soundness proof of the anti-frame rule employs the technique of so-called commutative pairs. This idea was already present in Pottier's syntactic proof sketch [24], and has been worked out in more detail in [32]. The intuitive idea is that the pair denoted w ′ 0 and w ′ 1 below can be used to merge two invariants denoted w 0 and w 1 below such that all computations described in the first invariant w 0 preserve the second invariant w 1 , and vice-versa.

Lemma 25 (Existence of commutative pairs). For all worlds w 0 , w 1 ∈ W , there exist w ′ 0 , w ′ 1 ∈ W such that

Proof. Fix w 0 , w 1 ∈ W , and consider the function F on X × X defined by

Then, F is contractive, since ⊗ is contractive in its second argument. Also, F restricts to a function on the non-empty and closed subset W × W of X × X. Thus, by Banach's fixpoint theorem, F has a unique fixpoint (w ′ 0 , w ′ 1 ) ∈ W × W . This means that

Note that these are the first two equalities claimed by this lemma. The remaining claim is w 0 • w ′ 1 = w 1 • w ′ 0 , and it can be proved as follows. Let w ∈ X.

Since w was chosen arbitrarily, we have

, and the claim follows from the injectivity of ι -1 .

Lemma 26 (Soundness of the anti-frame rule).

Proof. We prove |= (Γ t : χ). Let w ∈ W , η an environment, r ∈ URel (Heap) and

We must prove (k, (ρ(t), h)) ∈ E( χ η * r)(w). By Lemma 25,

holds for some worlds w 1 , w 2 in W . First, we find a superset of the precondition Γ η (w) * ι -1 (w)(emp) * r in the assumption above, replacing the first two * -conjuncts as follows:

by monotonicity of Γ η and

Thus, by the monotonicity of separating conjunction, we have that

We need to show that (k, (ρ(t), h)) ∈ E( χ η * r)(w), so assume (ρ(t) | h) -→ j (t ′ | h ′ ) for some j ≤ k such that (t ′ | h ′ ) is irreducible. From (32) we then obtain