Object Capabilities and Lightweight Affinity in Scala

arXiv:1607.05609v2 [cs.PL] 25 Jul 2016

Implementation, Formalization, and Soundness
Philipp Haller

Alexandre Loiko

KTH Royal Institute of Technology, Sweden
phaller@kth.se

Google Stockholm, Sweden ∗
aleloi@google.com

Abstract
Aliasing is a known source of challenges in the context of
imperative object-oriented languages, which have led to important advances in type systems for aliasing control. However, their large-scale adoption has turned out to be a surprisingly difficult challenge. While new language designs show
promise, they do not address the need of aliasing control in
existing languages.
This paper presents a new approach to isolation and
uniqueness in an existing, widely-used language, Scala. The
approach is unique in the way it addresses some of the most
important obstacles to the adoption of type system extensions for aliasing control. First, adaptation of existing code
requires only a minimal set of annotations. Only a single
bit of information is required per class. Surprisingly, the
paper shows that this information can be provided by the
object-capability discipline, widely-used in program security. We formalize our approach as a type system and prove
key soundness theorems. The type system is implemented
for the full Scala language, providing, for the first time, a
sound integration with Scala’s local type inference. Finally,
we empirically evaluate the conformity of existing Scala
open-source code on a corpus of over 75,000 LOC.
Categories and Subject Descriptors D.3.3 [Programming
Languages]: Language Constructs and Features; F.3.3 [Logics and Meanings of Programs]: Studies of Program Constructs
Keywords Object capability model, uniqueness, implicits,
Scala

1.

Introduction

Uncontrolled aliasing in imperative object-oriented languages introduces a variety of challenges in large-scale software development. Among others, aliasing can increase the
difficulty of reasoning about program behavior and software
architecture [3], and it can introduce data races in concurrent programs. These observations have informed the development of a number of type disciplines aimed at providing
static aliasing properties, such as linear types [33, 51, 64],
∗ Work

done while at KTH.

region inference [62, 63], unique references [14, 18, 40, 48],
and ownership types [21, 50].
While there have been important advances in the flexibility and expressiveness of type systems for aliasing control,
large-scale adoption has been shown to be a much greater
challenge than anticipated. Recent efforts in the context of
new language designs like Rust [7] are promising, but they
do not address the increasing need for aliasing control in existing, widely-used languages.
One of the most important obstacles to the adoption of
a type system extension in a widely-used language with a
large ecosystem is the adaptation of existing code, including
third-party libraries. Typically, adaptation consists of adding
(type) annotations required by the type system extension.
With a large ecosystem of existing libraries, this may be prohibitively expensive even for simple annotations. A second,
and almost equally critical obstacle is robust support for the
entirety of an existing language’s type system in a way that
satisfies requirements for backward compatibility.
This paper presents a new approach to integrating a flexible type system for isolation and uniqueness into an existing, full-featured language, Scala. Our approach minimizes
the annotations necessary for reusing existing code in a context where isolation and uniqueness is required. In the presented system, a single bit of information is enough to decide whether an existing class supports isolation and uniqueness. A key insight of our approach is that this single bit
of information is provided by the object-capability discipline [27, 46]. The object capability model is an established
methodology in the context of program security, and has
been proven in large-scale industrial use for secure sandboxing of JavaScript applications [23, 47, 56].
This paper makes the following contributions:
• We present a new approach to separation and unique-

ness which aims to minimize the annotations necessary to
reuse existing code (Section 2). In our system, reusability is based on the object capability model. Thus, when
annotating existing code bases, only a single bit of information is required per class.
• We formalize our approach in the context of two object-

oriented core languages (Section 3). The first core lan-

guage formalizes a type-based notion of object capabilities. The second core language additionally provides external uniqueness via flow-insensitive permissions.

class ActorA extends Actor[Any] {
override def receive(msg: Any): Unit = msg match {
case s: Start =>
val newMsg = new Message

• We provide complete soundness proofs, formally estab-

newMsg.arr = Array(1, 2, 3, 4)
s.next.send(newMsg)
newMsg.arr(2) = 33
// ...
case other => // ...

lishing heap separation and uniqueness invariants for our
two core languages (Section 4). We have also mechanized
the operational semantics and type system of the first core
language in Coq (Section B).

}
}

• We implement our approach for the full Scala language

class ActorB extends Actor[Message] {
override def receive(msg: Message): Unit = {

as a compiler plugin (Section 5). To our knowledge, our
implementation of (external) uniqueness is the first to integrate soundly with local type inference in Scala. Moreover, the implementation leverages a unique combination
of previous proposals for (a) implicit parameters [24, 25],
and (b) closures with capture control [31, 45].

println(msg.arr.mkString(","))
}
}

class Message {
var arr: Array[Int] = _
def leak(): Unit = {
SomeObject.fld = arr

• We empirically evaluate the conformity of existing Scala

}

classes to the object capability model on a corpus of over
75,000 LOC of popular open-source projects (Section 6).
Results show that between 21% and 79% of the classes
of a project adhere to a strict object capability discipline.

}

object SomeObject {
var fld: Array[Int] = _
}

class Start {
var next: ActorRef[Message] = _
}

In the following we discuss the most closely related work,
and defer a discussion of other related work to Section 7. In
Section 8 we conclude.
Selected Related Work. Most closely related to our system are approaches based on permissions or capabilities.
Of particular relevance are Haller and Odersky’s capabilities for uniqueness [38] in Scala (“Cap4S”). While their
work shares our high-level goal of lightweight unique references in Scala, the two approaches are significantly different, with important consequences concerning soundness,
robustness, and compatibility. First, Cap4S is based on flowsensitive capabilities which are modeled using Scala’s annotations, similar to the use of extended type annotations
in Java 8 for pluggable type systems [29]. However, the interaction between Scala’s local type inference [53] and annotation propagation has been shown to be a source of unsoundness and implementation complexities for such pluggable type systems [58]; these challenges are exacerbated
in flow-sensitive type systems. In contrast, L AC ASA models
capabilities using Scala’s implicits [24], an intrinsic part of
type inference in Scala. In addition, foundations of implicits
have been studied [25], whereas Scala’s annotations remain
poorly understood. Second, L AC ASA fundamentally simplifies type checking: as long as a class conforms to the objectcapability model, L AC ASA’s constructs enable isolation and
uniqueness for instances of the class. This has two important
consequences: (a) a minimal set of additional annotations (a
single bit of information per class) enables reusing existing
code, and (b) type checking reusable class declarations is
simple and well-understood, following the object-capability
discipline, which we adapt for Scala.

Figure 1. Two communicating actors in Scala.

2.

A Brief Overview of L AC ASA

We proceed with an informal overview of L AC ASA: its programming model in Scala, and its type system.
A First Example. Consider the case of asynchronous communication between two concurrent processes. This style of
concurrency is well-supported by the actor model [2, 39]
for which multiple implementations exist for Scala [36, 37,
42]. Figure 1 shows the definition of two actor classes.1
The behavior of each actor is implemented by overriding
the receive method inherited from superclass Actor. The
receive method is invoked by the actor runtime system
whenever an actor is ready to process an incoming message.
In the example, whenever ActorA has received an instance
of class Start, it creates an instance of class Message, initializes the instance with an integer array, and sends the instance to the next actor.
Note that field next of class Start has type
ActorRef[Message] (line 27) instead of Actor[Message].
An ActorRef serves as an immutable and serializable handle to an actor. The public interface of ActorRef is minimal;
its only purpose is to provide methods for
asynchronously sending messages to the ActorRef’s
underlying actor (an instance of a subclass of Actor). The
purpose of ActorRef as a type separate from Actor is to
1 In

favor of clarity of explanation, Figure 1 shows hypothetical Scala code
which requires slight changes for compilation with the Akka [42] library.

class ActorA extends Actor[Any] {
override def receive(box: Box[Any])
(implicit acc: CanAccess { type C = box.C }) {

package lacasa
abstract class Actor[T] {
def receive(msg: Box[T])
(implicit acc: CanAccess { type C = msg.C })

box.open({
case s: Start =>
mkBox[Message] { packed =>
val access = packed.access
packed.box.open({ msg =>
msg.arr = Array(1, 2, 3, 4)

: Unit

final val self: ActorRef[T] = ...
...
}

abstract class ActorRef[T] {
def send(msg: Box[T])

}) (access)
s.next.send(packed.box)({
// ...

(cont: NullarySpore[Unit] {
type Excluded = msg.C
})
(implicit acc: CanAccess { type C = msg.C })
: Nothing

}) (access)
}

case other => // ...

...

}) (acc)

}

}

Figure 3. L AC ASA’s Actor and ActorRef classes.

}

class ActorB extends Actor[Message] {
override def receive(box: Box[Message])
(implicit acc: CanAccess { type C = box.C }) {
box.open({ msg =>
println(msg.arr.mkString(","))
}) (acc)

1. Actors send and receive boxes of type Box[T], rather
than direct object references. As explained in the following, L AC ASA’s type system enforces strong encapsulation properties for boxes.

}
}

Figure 2. Two communicating actors in L AC ASA.
provide a fault handling model similar to Erlang [8].2 In
this model, a faulty actor may be restarted in a way where
its underlying Actor instance is replaced with a new instance of the same class. Importantly, any ActorRef referring to the actor that is being restarted switches to using the
new Actor instance in a way that is transparent to clients
(which only depend on ActorRefs). This enables introducing fault-handling logic in a modular way (cf. Erlang’s OTP
library [32]).
The shown program suffers from multiple safety hazards: first, within the leak method (line 19), the array of
the current Message instance is stored in the global singleton object SomeObject (line 20); thus, subsequently, multiple actors could access the array through SomeObject concurrently. Second, after sending newMsg to ActorB (line 6),
ActorA mutates the array contained in newMsg (line 7); this
could lead to a data race, since ActorB may be accessing
newMsg.arr at this point.
L AC ASA prevents the two safety hazards of the example
using two complementary mechanisms: object capabilities
and affine access permissions. Figure 2 shows the same example written in L AC ASA.3 L AC ASA introduces two main
changes to the Actor and ActorRef library classes:
2 Scala’s

original actor implementation [37] only provided an Actor type;
the distinction between Actor and ActorRef was introduced with the
adoption of Akka as Scala’s standard actor implementation.
3 This example is also included in the L AC ASA open-source project available at: https://github.com/phaller/lacasa/

2. The type of the receive method is changed to additionally include an implicit permission parameter. (We explain implicit permissions in detail below.)
Due to these changes, L AC ASA provides its own versions of
the Actor and ActorRef library classes; Figure 3 shows the
main declarations.4
Boxes. A box of type Box[T] encapsulates a reference to
an object of type T. However, this reference is only accessible using an open method: box.open({ x => ... });
here, x is an alias of the encapsulated reference. For example, on line 22 ActorB opens the received box in order to
print the array of the Message instance. Note that the use
of open on lines 4–16 relies on Scala’s syntax for partial
functions: a block of case clauses
{

case pat1 => e1
...

case patn => en
}

creates a partial function with the same run-time semantics
as the function
x => x match {
case pat1 => e1
...
case patn => en
}

In combination with L AC ASA’s type system, boxes enforce constraints that directly prevent the first safety hazard in the previous example. Boxes may only encapsulate
4 In

ongoing work we are developing adapter classes to conveniently integrate L AC ASA and the Akka actor library.

instances whose classes follow the object-capability discipline. Roughly speaking, the object-capability discipline
prevents an object obj from obtaining references that were
not explicitly passed to obj via constructor or method calls;
in particular, it is illegal for obj to access shared, global singleton objects like SomeObject. As a result, the problematic
leak (line 20 in Figure 1) causes a compilation error.
Capture Control. In general, the requirement of boxes to
encapsulate object-capability safe classes is not sufficient to
ensure isolation, as the following example illustrates:
// box: Box[Message]

var a: Array[Int] = null
box.open({ msg =>
a = msg.arr
SomeObject.fld = msg.arr
})(acc)
next.send(box)({
a(2) = 33
})(acc)

In this case, by capturing variable a in the body of open,
and by making a an alias of the array in msg, it would be
possible to access the array even after sending it (inside msg
inside box) to next. To prevent such problematic leaks, the
body of open is not allowed to capture anything (i.e., it must
not have free variables). Furthermore, the body of open is
not allowed to access global singleton objects. Thus, both
the access to a on line 4 and the access to SomeObject on
line 5 cause compilation errors. Finally, the body of open
may only create instances of object-capability safe classes
to prevent indirect leaks such as on line 20 in Figure 1.
The second safety hazard illustrated in Figure 1, namely
accessing a box that has been transferred, is prevented using
a combination of boxes, capture control, and access permissions, which we discuss next.
Access Permissions. A box can only be accessed (e.g., using open) at points in the program where its corresponding
access permission is in scope. Box operations take an extra argument which is the permission required for accessing
the corresponding box. For example, the open invocation on
lines 22–24 in Figure 2 takes the acc permission as an argument (highlighted) in addition to the closure. Note that acc
is passed within a separate argument list. The main reason
for using an additional argument list instead of just an additional argument is the use of implicits to reduce the syntactic
overhead (see below).
The static types of access permissions are essential for
alias tracking. Importantly, the static types ensure that an access permission is only compatible with a single Box[T] instance. For example, the acc parameter in line 3 has type
CanAccess { type C = box.C } where box is a parameter of type Box[Any]. Thus, the type member C of the permission’s type is equal to the type member C of box.
In Scala, box.C is a path-dependent type [5, 6]; box.C
is equivalent to the type box.type#C which selects type C
from the singleton type box.type. The type box.type is

only compatible with singleton types x.type where the type
checker can prove that x and box are always aliases. (Thus,
in a type box.type, box may not be re-assignable.) Access
permissions in L AC ASA leverage this aliasing property of
singleton types: since it is impossible to create a box b such
that b.C is equal to the type member C of an existing box, it
follows that an access permission is only compatible with at
most one instance of Box[T].
The only way to create an access permission is by creating a box using an mkBox expression. For example, the
mkBox expression on line 6 in Figure 2 creates a box of
type Box[Message] as well as an access permission. Besides a type argument, mkBox also receives a closure of the
form { packed => ... }. The closure’s packed parameter encapsulates both the box and the access permission,
since both need to be available in the scope of the closure.
Certain operations consume access permissions, causing
associated boxes to become unavailable. For example, the
message send on line 11 consumes the access permission of
packed.box to prevent concurrent accesses from the sender
and the receiver. As a result, packed.box is no longer accessible in the continuation of send.
Note that permissions in L AC ASA are flow-insensitive by
design. Therefore, the only way to change the set of available permissions is by entering scopes that prevent access
to consumed permissions. In L AC ASA, this is realized using continuation closures: each operation that changes the
set of available permissions also takes a closure that is the
continuation of the current computation; the changed set of
permissions is only visible in the continuation closure. Furthermore, by discarding the call stack following the execution of a continuation closure, L AC ASA enforces that scopes
where consumed permissions are visible (and therefore “accessible”) are never re-entered. The following L AC ASA operations discard the call stack: mkBox, send, swap (see below). In contrast, open does not discard the call stack, since
it does not change the set of permissions.
In the example, the send operation takes a continuation
closure (line 11–13) which prevents access to the permission
of packed.box; furthermore, the call stack is discarded,
making the code from line 14 unreachable.
Implicit Permissions. To make sure access permissions
do not have to be explicitly threaded through the program, they are modeled using implicits [24, 25]. For example, consider the receive method in line 2–3. In addition to its regular box parameter, the method has an acc
parameter which is marked as implicit. This means at
invocation sites of receive the argument passed to the
implicit parameter is inferred (or resolved) by the type
checker. Importantly, implicit resolution fails if no typecompatible implicit value is in scope, or if multiple ambiguous type-compatible implicit values are in scope.5 The ben5 See

the Scala language specification [54] for details of implicit resolution.

class ActorA(next: ActorRef[C])
extends Actor[Container] {
def receive(msg: Box[Container])
(implicit acc: CanAccess { type C = msg.C }) {
mkBox[C] { packed =>
// ...
msg.swap(_.part1)(_.part1 = _, b)(
spore { pack =>
implicit val acc = pack.access
pack.box.open({ part1Obj =>
println(part1Obj.arr.mkString(","))
part1Obj.arr(0) = 1000
})(acc)
next.send(pack.box)({
// ...
})(acc)
}
)
}
}
}

class Container {
var part1: Box[C] = _
var part2: Box[C] = _
}

class C {
var arr: Array[Int] = _
}

Figure 4. An actor accessing a unique field via swap.

efit of marking acc as implicit is that within the body of
receive, acc does not have to be passed explicitly to methods requiring access permissions, including L AC ASA expressions like open. Figure 2 makes all uses of implicits
explicit (shaded). This explicit style also requires making
parameter lists explicit; for example, consider lines 22–
24: box.open({ x => ... })(acc). In contrast, passing the access permission acc implicitly enables the more
lightweight Scala syntax box open { x => ... }.
Stack Locality. It is important to note that the above safety
measures with respect to object capabilities, capture control,
and access permissions could be circumvented by creating
heap aliases of boxes and permissions. Therefore, boxes and
permissions are confined to the stack by default. This means,
without additional annotations they cannot be stored in fields
of heap objects or passed as arguments to constructors.
Unique Fields. Strict stack confinement of boxes would
be too restrictive in practice. For example, an actor might
have to store a box in the heap to maintain access across
several invocations of its message handler while enabling a
subsequent ownership transfer. To support such patterns L A C ASA enables actors and boxes to have unique fields which
store boxes. Access is restricted to maintain external uniqueness [18] of unique fields (see Section 3 for a formalization
of the uniqueness and aliasing guarantees of unique fields).

Figure 4 shows an actor receiving a box of type
Box[Container] where class Container declares two
unique fields, part1 and part2 (line 23–24). In L AC ASA,
these fields, which are identified as unique fields through
their box types, have to be accessed using a swap expression. swap “removes” the box of a unique field and replaces
it with another box. For example, in line 7, swap extracts
the part1 field of the msg box and replaces it with some
other box b. The extracted box is accessible via the pack
parameter of the subsequent “spore.”

3.

Formalization

In this section we formalize the main concepts of L A C ASA in the context of typed object-oriented core languages.
Our approach, however, extends to the whole of Scala (see
Section 5).
Our technical development proceeds in two steps. In the
first step, we formalize simple object capabilities. In combination with L AC ASA’s boxes and its open construct object capabilities enforce an essential heap separation invariant (Section 3.2).
In the second step, we extend our first core language with
lightweight affinity based on flow-insensitive permissions.
The extended core language combines permissions and continuation terms to enable expressing (external) uniqueness,
ownership transfer, and unique fields.
Soundness, isolation, and uniqueness invariants are established based on small-step operational semantics and syntaxdirected type rules.
3.1

Object Capabilities

This section introduces C ORE L AC ASA1 (CLC1 ), a typed,
object-oriented core language with object capabilities.
Syntax Figure 5 and Figure 6 show the syntax of CLC1 .
A program consists of a sequence of class definitions, cd, a
sequence of global variable declarations, vd, and a “main”
term t. Global variables model top-level, stateful singleton
objects of our realization in Scala (see Section 5). A class
C has exactly one superclass D and a (possibly empty)
sequence of fields, vd, and methods, md. The superclass
may be AnyRef, the superclass of all classes. To simplify the
presentation, methods have exactly one parameter x; their
body is a term t. There are three kinds of types: class types
C, box types Box[C], and the Null type. Null is a subtype
of all class types; it is used to assign a type to null.
In order to simplify the presentation of the operational semantics, programs are written in A-normal form [34] (ANF)
which requires all subexpressions to be named. We enforce
ANF by introducing two separate syntactic categories for
terms and expressions, shown in Figure 6. Terms are either
variables or let bindings. Let bindings introduce names for
intermediate results. Most expressions are standard, except
that the usual object-based expressions, namely field selections, field assignments, and method invocations, have only

p ::= cd vd t
cd ::= class C extends D {vd md}
vd ::= var f : C
md ::= def m(x : σ) : τ = t
σ, τ ::=
C, D
| Box[C]
| Null

program
class
variable
method
type
class type
box type
null type

Figure 5. CLC1 syntax. C, D range over class names, f ,
m, x range over term names.
t ::=
x
| let x = e in t

terms
variable
let binding

e ::=
expressions
null
null reference
|x
variable
| x.f
selection
| x.f = y
assignment
| new C
instance creation
| x.m(y)
invocation
| box[C]
box creation
| x.open {y ⇒ t}
open box

H, hL, let x = null in til
−→ H, hL[x 7→ null], til

(E-N ULL)

H, hL, let x = y in til
−→ H, hL[x 7→ L(y)], til

(E-VAR)

H(L(y)) = hC, F M i
f ∈ dom(F M )
(E-S ELECT)
H, hL, let x = y.f in til
−→ H, hL[x 7→ F M (f )], til
L(y) = o
H(o) = hC, F M i
H 0 = H[o 7→ hC, F M [f 7→ L(z)]i]
(E-A SSIGN)
H, hL, let x = y.f = z in til
−→ H 0 , hL, let x = z in til
o∈
/ dom(H)
f ields(C) = f
H 0 = H[o 7→ hC, f 7→ nulli]
H, hL, let x = new C in til
−→ H 0 , hL[x 7→ o], til

(E-N EW)

o∈
/ dom(H)
f ields(C) = f
H 0 = H[o 7→ hC, f 7→ nulli]
H, hL, let x = box[C] in til
−→ H 0 , hL[x 7→ b(o)], til

(E-B OX)

Figure 7. CLC1 frame transition rules.

Figure 6. CLC1 terms and expressions.
variables as trivial subexpressions. The instance creation expression (new) does not take arguments: all fields of newlycreated objects are initialized to null.
Two kinds of expressions are unique to our core language:
box[C] creates a box containing a new instance of class
C. The expression box[C] has type Box[C]. The expression
x.open {y ⇒ t} provides temporary access to box x.
3.1.1

Dynamic Semantics

We formalize the dynamic semantics as a small-step operational semantics based on two reduction relations, H, F −→
H 0 , F 0 , and H, F S  H 0 , F S 0 . The first relation reduces
single (stack) frames F in heap H, whereas the second relation reduces entire frame stacks F S in heap H.
A heap H maps references o ∈ dom(H) to run-time
objects hC, F M i where C is a class type and F M is a field
map that maps field names to values in dom(H) ∪ {null}.
F S is a sequence of stack frames F ; we use the notation
F S = F ◦ F S 0 to indicate that in stack F S frame F is the
top-most frame which is followed by frame stack F S 0 .
A single frame F = hL, til consists of a variable environment L = env(F ), a term t, and an annotation l. The
variable environment L maps variable names x to values
v ∈ dom(H) ∪ {null} ∪ {b(o) | o ∈ dom(H)}. A value
b(o) is a box reference created using CLC1 ’s box[C] expression. A box reference b(o) prevents accessing the members

of o using regular selection, assignment, and invocation expressions; instead, accessing o’s members requires the use
of an open expression to temporarily “borrow” the encapsulated reference. As is common, L0 = L[x 7→ v] denotes
the updated mapping where L0 (y) = L(y) if y 6= x and
L0 (y) = v if y = x. A frame annotation l is either empty
(or non-existant), expressed as l = , or equal to a variable
name x. In the latter case, x is the name of a variable in the
next frame which is to be assigned the return value of the
current frame.
As is common [41], f ields(C) denotes the fields of class
C, and mbody(C, f ) = x → t denotes the body of a method
def m(x : σ) : τ = t.
Reduction of a program p = cd vd t begins in an initial
environment H0 , F0 ◦  such that
H0 = {og 7→ hCg , F Mg i} (initial heap), F0 = hL0 , ti
(initial frame), L0 = {global 7→ og }, F Mg = {x 7→
null | var x : C ∈ vd}, and og a fresh object identifier;
Cg is a synthetic class defined as:
class Cg extends AnyRef {vd}. Thus, a global variable
var x : C is accessed using global.x; we treat global as
a reserved variable name.
Single Frame Reduction. Figure 7 shows single frame
transition rules. Thanks to the fact that terms are in ANF
in our core language, the reduced term is a let binding in
each case. This means reduction results can be stored immediately in the variable environment, avoiding the intro-

H(L(y)) = hC, F M i
mbody(C, m) = x → t0
L0 = L0 [this 7→ L(y), x 7→ L(z)]
(E-I NVOKE)
H, hL, let x = y.m(z) in til ◦ F S
 H, hL0 , t0 ix ◦ hL, til ◦ F S
H, hL, xiy ◦ hL0 , t0 il ◦ F S
(E-R ETURN 1)
 H, hL0 [y 7→ L(x)], t0 il ◦ F S
H, hL, xi ◦ hL0 , t0 il ◦ F S
(E-R ETURN 2)
 H, hL0 , t0 il ◦ F S
L(y) = b(o)
L0 = [z 7→ o]
(E-O PEN)
H, hL, let x = y.open {z ⇒ t0 } in til ◦ F S
 H, hL0 , t0 i ◦ hL[x 7→ L(y)], til ◦ F S
Figure 8. CLC1 frame stack transition rules.

p ` cd

p ` Γ0

Γ0 ;  ` t : σ

p ` cd vd t

(WF-P ROGRAM)

C ` md
D = AnyRef ∨ p ` class D . . .
∀ (def m . . .) ∈ md. override(m, C, D)
/ f ields(D)
∀ var f : σ ∈ f d. f ∈
p ` class C extends D {f d md}
(WF-C LASS)
mtype(m, D) not defined ∨ mtype(m, D) = mtype(m, C)
override(m, C, D)
(WF-OVERRIDE)
Γ0 , this : C, x : σ ;  ` t : τ 0
τ 0 <: τ
(WF-M ETHOD)
C ` def m(x : σ) : τ = t
Figure 9. Well-formed CLC1 programs.

duction of locations or references in the core language syntax. Rule E-B OX is analogous to rule E-N EW, except that
variable x is bound to a box reference b(o). As a result,
fields of the encapsulated object o are not accessible using regular field selection and assignment, since rules ES ELECT and E-A SSIGN would not be applicable. Apart from
E-B OX the transition rules are similar to previous stackbased formalizations of class-based core languages with objects [11, 12, 55].
Frame Stack Reduction. Figure 8 shows the frame stack
transition rules. Rule E-I NVOKE creates a new frame, annotated with x, that evaluates the body of the called method.
Rule E-R ETURN 1 uses the annotation y of the top-most
frame to return the value of x to its caller’s frame. Rule
E-R ETURN 2 enables returning from an -annotated frame.
Rule E-O PEN creates such an -annotated frame. In the new
frame, the object encapsulated by box y is accessible under alias z. In contrast to E-I NVOKE, the new frame does
not include the global environment L0 ; instead, z is the only
variable in the (domain of the) new environment.
3.1.2

Static Semantics

Type Assignment. A judgement of the form Γ ; a ` t : σ
assigns type σ to term t in type environment Γ under effect
a. When assigning a type to the top-level term of a program
the effect a is  which is the unrestricted effect. In contrast,
the body of an open expression must be well-typed under
effect ocap which requires instantiated classes to be ocap.
Well-Formed Programs. Figure 9 shows the rules for wellformed programs. (We write . . . to omit unimportant parts of
a program.) A program is well-formed if all its class definitions are well-formed and its top-level term is well-typed in
type environment Γ0 = {global : Cg } (WF-P ROGRAM);
class Cg is defined as: class Cg extends AnyRef {vd}.
Rule WF-C LASS defines well-formed class definitions. In a
well-formed class definition (a) all methods are well-formed,

ocap(AnyRef)
(O CAP -A NY R EF)
p ` class C extends D {f d md}
C `ocap md
ocap(D)
∀ var f : E ∈ f d. ocap(E)
(O CAP -C LASS)
ocap(C)
this : C, x : σ ; ocap ` t : τ 0
τ 0 <: τ
(O CAP -M ETHOD)
C `ocap def m(x : σ) : τ = t
Figure 10. Object capability rules.
(b) the superclass is either AnyRef or a well-formed class
in the same program, and (c) method overriding (if any) is
well-formed; fields may not be overridden. We use a standard function f ields(D) [41] to obtain the fields in class D
and superclasses of D. Rule WF-OVERRIDE defines wellformed method overriding: overriding of a method m in
class C with superclass D is well-formed if D (transitively)
does not define a method m or the type of m in D is the
same as the type of m in C. A method m is well-typed in
class C if its body is well-typed with type τ 0 under effect 
in environment Γ0 , this : C, x : σ, where σ is the type of
m’s parameter x, such that τ 0 is a subtype of m’s declared
result type τ (WF-M ETHOD).
Object Capabilities. For a class C to satisfy the constraints
of the object-capability discipline, written ocap(C), it must
be well-formed according to the rules shown in Figure 10.
Essentially, for a class C we have ocap(C) if its superclass
is ocap, the types of its fields are ocap, and its methods
are well-formed according to `ocap . Rule O CAP -M ETHOD
looks a lot like rule WF-M ETHOD, but there are two essential differences: first, the method body must be well-typed
in a type environment that does not contain the global environment Γ0 ; thus, global variables are inaccessible. Second,

Γ ; a ` null : Null
(T-N ULL)

x ∈ dom(Γ)
(T-VAR)
Γ ; a ` x : Γ(x)

Γ; a`e:τ
Γ, x : τ ; a ` t : σ
Γ ; a ` let x = e in t : σ

(T-L ET)

Γ; a`x:C
f type(C, f ) = D
(T-S ELECT)
Γ ; a ` x.f : D
Γ; a`x:C
f type(C, f ) = D
Γ ; a ` y : D0
D0 <: D
(T-A SSIGN)
Γ ; a ` x.f = y : D
a = ocap =⇒ ocap(C)
Γ ; a ` new C : C

(T-N EW)

Γ; a`x:C
mtype(C, m) = σ → τ
Γ ; a ` y : σ0
σ 0 <: σ
(T-I NVOKE)
Γ ; a ` x.m(y) : τ
ocap(C)
Γ ; a ` box[C] : Box[C]

(T-B OX)

Γ ; a ` x : Box[C]
y : C ; ocap ` t : σ
(T-O PEN)
Γ ; a ` x.open {y ⇒ t} : Box[C]
Figure 11. CLC1 term and expression typing.
the method body must be well-typed under effect ocap; this
means that within the method body only ocap classes may
be instantiated.
Subclassing and Subtypes. In CLC1 , the subtyping relation <:, defined by the class table, is identical to that of
FJ [41] except for two additional rules:

L(x) = null ∨
typeof (H, L(x)) <: Γ(x)
H ` Γ; L; x

(WF-VAR)

dom(Γ) ⊆ dom(L)
∀x ∈ dom(Γ). H ` Γ; L; x
(WF-E NV)
H ` Γ; L
Γ; a`t:σ
H `  (T-E MP FS)
H ` Γ; L
(T-F RAME 1)
H ` hL, til : σ
Γ, x : τ ; a ` t : σ
H ` Γ; L
(T-F RAME 2)
H `τx hL, til : σ
H ` F : σ
H `τx F  : σ
H ` FS
H ` FS
(T-FS-NA)
(T-FS-NA2)
H ` F ◦ FS
H `τx F  ◦ F S
H ` Fx : τ
H `σy F x : τ
τ
H `x F S
H `τx F S
(T-FS-A)
(T-FS-A2)
H ` Fx ◦ FS
H `σy F x ◦ F S
Figure 12. Well-formed environments, frames, and frame
stacks.
its term t is well-typed in some environment Γ such that Γ, L
are well-formed in H (T-F RAME 1, T-F RAME 2). A frame
stack is well-formed if all its frames are well-typed. Rules TFS-NA and T-FS-NA2 are required for -annotated frames.
Well-typed heaps are defined as follows.
Definition 1 (Object Type). For an object identifier o ∈
dom(H) where H(o) = hC, F M i, typeof (H, o) := C
Definition 2 (Well-typed Heap). A heap H is well-typed,
written ` H : ? iff
∀o ∈ dom(H). H(o) = hC, F M i =⇒

C <: D
(<:-B OX)
Box[C] <: Box[D]

Null <: σ (<:-N ULL)

(dom(F M ) = f ields(C) ∧
∀f ∈ dom(F M ). F M (f ) = null ∨
typeof (H, F M (f )) <: f type(C, f ))

Term and Expression Typing. Figure 11 shows the inference rules for typing terms and expressions. The type rules
are standard except for T-N EW, T-B OX, and T-O PEN. Under
effect ocap T-N EW requires the instantiated class to be ocap.
An expression box[C] has type Box[C] provided ocap(C)
holds (T-B OX). Finally, T-O PEN requires the body t of open
to be well-typed under effect ocap and in a type environment
consisting only of y : C. The type of the open expression itself is Box[C] (it simply returns box x).
Well-Formedness. Frames, frame stacks, and heaps must
be well-formed. Figure 12 shows the well-formedness rules
for environments, frames, and frame stacks. Essentially, Γ, L
are well-formed in heap H if for all variables x ∈ dom(Γ)
the type of L(x) in H is a subtype of the static type of x in Γ
(WF-VAR, WF-E NV). A frame hL, til is well-typed in H if

To formalize the heap structure enforced by CLC1 we use
the following definitions.
Definition 3 (Separation). Two object identifiers o and o0
are separate in heap H, written sep(H, o, o0 ), iff
∀q, q 0 ∈ dom(H).
reach(H, o, q) ∧ reach(H, o0 , q 0 ) =⇒ q 6= q 0 .
Definition 4 (Box Separation). For heap H and frame F ,
boxSep(H, F ) holds iff
F = hL, til ∧ ∀x 7→ b(o), y 7→ b(o0 ) ∈ L.
o 6= o0 =⇒ sep(H, o, o0 )

boxSep(H, F )
boxObjSep(H, F )
boxOcap(H, F )
a = ocap =⇒ globalOcapSep(H, F )
H ; a ` F ok
H ; a ` F ok
H ; a ` F ◦  ok

x 7→ b(o) ∈ L
boxRoot(o, hL, til )
(F- OK)

boxRoot(o, F )
boxRoot(o, F ◦ )

(S ING FS- OK)

H ; b(` F l ok
H ; a ` F S ok
ocap if a = ocap ∨ l = 
b=

otherwise
boxSeparation(H, F, F S)
uniqueOpenBox(H, F, F S)
openBoxP ropagation(H, F l , F S)
(FS- OK)
H ; b ` F l ◦ F S ok
Figure 13. Separation invariants of frames and frame
stacks.
Definition 5 (Box-Object Separation). For heap H and
frame F , boxObjSep(H, F ) holds iff
F = hL, til ∧ ∀x 7→ b(o), y 7→ o0 ∈ L. sep(H, o, o0 )
Definition 6 (Box Ocap Invariant). For heap H and frame
F , boxOcap(H, F ) holds iff
F = hL, til ∧ ∀x 7→ b(o) ∈ L, o0 ∈ dom(H).
reach(H, o, o0 ) =⇒ ocap(typeof (H, o0 ))
In a well-formed frame, (a) two box references that are not
aliases are disjoint (Def. 4), (b) box references and non-box
references are disjoint (Def. 5), and (c) all types reachable
from box references are ocap (Def. 6).
Definition 7 (Global Ocap Separation). For heap H and
frame F , globalOcapSep(H, F ) holds iff
F = hL, til ∧ ∀x 7→ o ∈ L, y 7→ o0 ∈ L0 .
ocap(typeof (H, o)) ∧ sep(H, o, o0 )
In addition, in a well-formed frame that is well-typed under
effect ocap, non-box references have ocap types, and they
are disjoint from the global variables in L0 (Def. 7).
The judgement H ; a ` F ok combines these invariants
as shown in Figure 13; the corresponding judgement for
frame stacks uses the following additional invariants.
Definition 8 (Box Separation). For heap H, frame F , and
frame stack F S, boxSeparation(H, F, F S) holds iff
∀o, o0 ∈ dom(H). boxRoot(o, F ) ∧ boxRoot(o0 , F S) ∧
o 6= o0 =⇒ sep(H, o, o0 )
Def. 8 uses auxiliary predicate boxRoot shown in Figure 14. boxRoot(o, F ) holds iff there is a box reference
to o in frame F ; boxRoot(o, F S) holds iff there is a
box reference to o in one of the frames F S. Informally,
boxSeparation(H, F, F S) holds iff non-aliased boxes are
disjoint.

boxRoot(o, F ) ∨ boxRoot(o, F S)
boxRoot(o, F ◦ F S)
boxRoot(o, F S)
x 7→ o0 ∈ L
reach(H, o, o0 )
openbox(H, o, hL, til , F S)
Figure 14. Auxiliary predicates.
Definition 9 (Unique Open Box). For heap H, frame F , and
frame stack F S, uniqueOpenBox(H, F, F S) holds iff
∀o, o0 ∈ dom(H). openbox(H, o, F, F S) ∧
openbox(H, o0 , F, F S) =⇒ o = o0
Def. 9 uses auxiliary predicate openbox shown in Figure 14.
openbox(H, o, F, F S) holds iff boxRoot(o, F S) and there
is a local variable in frame F which points to an object
reachable from o (box o is “open” in frame F ). Informally,
uniqueOpenBox(H, F, F S) holds iff at most one box is
open (i.e., accessible via non-box references) in frame F .
Definition 10 (Open Box Propagation). For heap H, frame
F l , and frame stack F S, openBoxP ropagation(H, F l , F S)
holds iff
l 6=  ∧ F S = G ◦ GS ∧ openbox(H, o, F, F S) =⇒
openbox(H, o, G, GS)
Informally, openBoxP ropagation(H, F l , F S) holds iff
frame F l preserves the open boxes in the top-most frame
of frame stack F S.
According to rule FS- OK shown in Figure 13, wellformed frame stacks ensure (a) non-aliased boxes are disjoint (Def. 8), (b) at most one box is open (i.e., accessible
via non-box references) per frame (Def. 9), and (c) method
calls preserve open boxes (Def. 10).
3.2

Soundness and Heap Separation

Type soundness of CLC1 follows from the following preservation and progress theorems. Instead of proving these theorems directly, we prove corresponding theorems for an extended core language (Section 4).
Theorem 1 (Preservation). If ` H : ? then:
1. If H ` F : σ, H ; a ` F ok, and H, F −→ H 0 , F 0
then ` H 0 : ?, H 0 ` F 0 : σ, and H 0 ; a ` F 0 ok.
2. If H ` F S, H ; a ` F S ok, and H, F S  H 0 , F S 0
then ` H 0 : ?, H 0 ` F S 0 , and H 0 ; b ` F S 0 ok.

Theorem 2 (Progress). If ` H : ? then:
If H ` F S and H ; a ` F S ok then either H, F S 
H 0 , F S 0 or F S = hL, xil ◦  or F S = F ◦ GS where
F = hL, let x = t in t0 il , t ∈ {y.f, y.f = z, y.m(z),
y.open {z ⇒ t00 }}, and L(y) = null.
The following corollary expresses an essential heap separation invariant enforced by CLC1 . Informally, the corollary states that objects “within a box” (reachable from a box
reference) are never mutated unless their box is “open” (a
reference to the box entry object is on the stack).
Corollary 1 (Heap Separation). If ` H : ? then:
If H ` F S, H ; a ` F S ok, H, F S  H 0 , F S 0 ,
F S = F ◦ GS, F = hL, let x = y.f = z in til , L(y) =
o0 , boxRoot(o, F S), and reach(H, o, o0 ), then w 7→ o ∈
env(G) where G ∈ F S.

p ::= cd vd t

program

cd ::= class C extends D { f d md} class
vd ::= var f : C
variable
ud ::= var f : Box[C]
unique field
f d ::= vd | ud

field

md ::= def m(x : σ) : C = t
σ, τ ::=
C, D
| Box[C]
| Null
π ::=
σ, τ
Q . Box[C]

method
surface type
class type
box type
null type
type
surface type
guarded type

⊥

bottom type

Proof sketch. First, by H ; a ` F S ok, FS- OK, and F S =
F ◦ GS we have H ; a ` F ok. By F- OK we have
boxObjSep(H, F ). By def. 5 this means u 7→ b(o) ∈
/ L
and therefore ¬boxRoot(o, F ). Given that L(y) = o0 ,
reach(H, o, o0 ), and boxRoot(o, F S) it must be that
boxRoot(o, GS). Given that boxRoot(o, GS) by def. boxRoot
(Figure 14), there is a frame G0 ∈ GS such that u 7→ b(o) ∈
env(G0 ). Well-formedness of F S implies well-formedness
of all its frames (FS- OK). Therefore, G0 is well-formed
and by F- OK, o is disjoint from other boxes (def. 4) and
other objects (def. 5) reachable in G0 , including the global
variable. By the transition rules, box reference u 7→ b(o)
prevents field selection; as a result, between frames F and
G0 there must be a frame created by opening b(o). By EO PEN, this means there is a frame G ∈ F S such that
w 7→ o ∈ env(G).

Figure 15. CLC2 syntax. C, D range over class names, f ,
m, x range over term names. Q ranges over abstract types.

3.3

3. A term swap(x.f, y) {z ⇒ t} extracts the value of the
unique field x.f and makes it available as the value of
a box z in the continuation t; in addition, the value of
box y replaces the previous value of x.f . Finally, y’s
permission is consumed.

Lightweight Affinity

This section introduces the C ORE L AC ASA2 language
(CLC2 ) which extends CLC1 with affinity, such that boxes
may be consumed at most once. Access to boxes is controlled using permissions. Permissions themselves are neither flow-sensitive nor affine. Consequently, they can be
maintained in the type environment Γ. Our notion of affinity is based on continuation terms: consumption of permissions, and, thus, boxes, is only possible in contexts where an
explicit continuation is provided. The consumed permission
is then no longer available in the continuation.
Syntax Figure 15 and Figure 16 show the syntactic differences between CLC2 and CLC1 : first, field types are either
class types C or box types Box[C]; second, we introduce a
bottom type ⊥ and guarded types Q.Box[C] where Q ranges
over a countably infinite supply of abstract types; third, we
introduce continuation terms.
In CLC2 types are divided into surface types which can
occur in the surface syntax, and general types, including
guarded types, which cannot occur in the surface syntax;
guarded types are only introduced by type inference (see

Section 3.3.2). The bottom type ⊥ is the type of continuation
terms tc ; these terms come in three forms:
1. A term box[C] {x ⇒ t} creates a box containing a new
instance of class type C, and makes that box accessible
as x in the continuation t. Note that in CLC1 boxes are
created using expressions of the form box[C]. In CLC2
we require the continuation term t, because creating a
box in addition creates a permission only available in t.
2. A term capture(x.f, y) {z ⇒ t} merges two boxes x
and y by assigning the value of y to the field f of the
value of x. In the continuation t (a) y’s permission is no
longer available, and (b) z refers to box x.

Given that only continuation terms can create boxes in
CLC2 , method invocations cannot return boxes unknown
to the caller. As a result, any box returned by a method
invocation must have been passed as the single argument in
the invocation. However, a method that takes a box as an
argument, and returns the same box can be expressed using a
combination of open and a method that takes the contents of
the box as an argument. Therefore, method return types are
always class types in CLC2 , simplifying the meta-theory.
3.3.1

Dynamic Semantics

CLC2 extends the dynamic semantics compared to CLC1
with dynamically changing permissions. A dynamic access
to a box requires its associated permission to be available.
For this, we extend the reduction relations compared to
CLC1 with permission sets P . Thus, a frame hL, t, P il com-

t ::=
x
| let x = e in t
| tc

terms
variable
let binding
continuation term

e ::=
null
|x
| x.f
| x.f = y
| new C
| x.m(y)
| x.open {y ⇒ t}

expressions
null reference
variable
selection
assignment
instance creation
invocation
open box

tc ::=
box[C] {x ⇒ t}

continuation term
box creation

| capture(x.f, y) {z ⇒ t}

capture

| swap(x.f, y) {z ⇒ t}

swap

H(L(y)) = hC, F M i
mbody(C, m) = x → t0
0
L = L0 [this 7→ L(y), x 7→ L(z)]
P 0 = ∅ ∨ (L(z) = b(o, p) ∧ p ∈ P ∧ P 0 = {p})
H, hL, let x = y.m(z) in t, P il ◦ F S
 H, hL0 , t0 , P 0 ix ◦ hL, t, P il ◦ F S
(E-I NVOKE)
H, hL, x, P iy ◦ hL0 , t0 , P 0 il ◦ F S
(E-R ETURN 1)
 H, hL0 [y 7→ L(x)], t0 , P 0 il ◦ F S
H, hL, x, P i ◦ hL0 , t0 , P 0 il ◦ F S
(E-R ETURN 2)
 H, hL0 , t0 , P 0 il ◦ F S
L(y) = b(o, p)
p∈P
L0 = [z 7→ o]
H, hL, let x = y.open {z ⇒ t0 } in t, P il ◦ F S
 H, hL0 , t0 , ∅i ◦ hL[x 7→ L(y)], t, P il ◦ F S
(E-O PEN)
o∈
/ dom(H)
f ields(C) = f
p fresh
H = H[o 7→ hC, f 7→ nulli]
(E-B OX)
H, hL, box[C] {x ⇒ t}, P il ◦ F S
 H 0 , hL[x 7→ b(o, p)], t, P ∪ {p}i ◦ 
0

Figure 16. CLC2 terms and expressions.
bines a variable environment L and term t with a set of permissions P . (As before, the label l is used for transferring
return values from method invocations.)
The transition rules of CLC2 for single frames are identical to the corresponding transition rules of CLC1 ; the permission sets do not change.6 In contrast, the transition rules
for frame stacks affect the permission sets of frames.
The extended transition rules of CLC2 are shown in Figure 17. Rule E-I NVOKE additionally requires permission p
to be available in P in case the argument of the invocation
is a box protected by p; in this case permission p is also
transferred to the new frame (the “activation record”). Reduction gets stuck if permission p is not available. Rules ER ETURN 1 and E-R ETURN 2 do not affect permission sets
and are otherwise identical to the corresponding rules of
CLC1 . Rule E-O PEN requires that permission p of the boxto-open b(o, p) is one of the currently available permissions
P . The permission set of the new frame is empty. Rule EB OX creates a box b(o, p) accessible in continuation t using fresh permission p. Note that rule E-B OX discards frame
stack F S in favor of the continuation t.
Figure 18 shows CLC2 ’s two new transition rules. EC APTURE merges box b(o, p) and box b(o0 , p0 ) by assigning
o0 to field f of object H(o). The semantics of capture is
thus similar to that of a regular field assignment. However,
capture additionally requires both permissions p and p0 to
be available; moreover, in continuation t permission p0 is no
longer available, effectively consuming box b(o0 , p0 ). Like
E-B OX, E-C APTURE discards frame stack F S. Finally, ES WAP provides access to a unique field f of an object in box
6 Therefore, the transition rules (trivially) extended with permission sets are

only shown in Appendix A.2.

Figure 17. CLC2 frame stack transition rules.
L(x) = b(o, p)
L(y) = b(o0 , p0 )
{p, p0 } ⊆ P
0
H(o) = hC, F M i
H = H[o 7→ hC, F M [f 7→ o0 ]i]
H, hL, capture(x.f, y) {z ⇒ t}, P il ◦ F S
 H 0 , hL[z 7→ L(x)], t, P \ {p0 }i ◦ 
(E-C APTURE)
L(x) = b(o, p)
L(y) = b(o0 , p0 )
{p, p0 } ⊆ P
00
H(o) = hC, F M i
F M (f ) = o
p00 fresh
0
0
H = H[o 7→ hC, F M [f 7→ o ]i]
H, hL, swap(x.f, y) {z ⇒ t}, P il ◦ F S
0
 H , hL[z 7→ b(o00 , p00 )], t, (P \ {p0 }) ∪ {p00 }i ◦ 
(E-S WAP)
Figure 18. Transition rules for capture and swap.
b(o, p): in continuation t variable z refers to the previous
object o00 in f ; the object o0 in box b(o0 , p0 ) replaces o00 . Like
E-C APTURE, E-S WAP requires both permissions p and p0 to
be available, and in continuation t permission p0 is no longer
available, consuming box b(o0 , p0 ).
3.3.2

Static Semantics

Well-Formed Programs. CLC2 adapts method
well-formedness for the case where static permissions are
propagated to the callee context: the body of a method with a
parameter of type Box[D] is type-checked in an environment
Γ which includes a static permission Perm[Q] where Q is a
fresh abstract type; furthermore, the parameter has a guarded
type Q . Box[D]. This environment Γ ensures the method
body has full access to the argument box.

Γ0 , this : C, x : D ;  ` t : E 0
E 0 <: E
(WF-M ETHOD 1)
C ` def m(x : D) : E = t
Γ = Γ0 , this : C, x : Q . Box[D], Perm[Q]
Q fresh
Γ ;  ` t : E0
E 0 <: E
C ` def m(x : Box[D]) : E = t
(WF-M ETHOD 2)
2
Figure 19. Well-formed CLC methods.
Γ; a`x:C
mtype(C, m) = σ → τ
Γ ; a ` y : σ0
σ 0 <: σ ∨
(σ = Box[D] ∧ σ 0 = Q . Box[D] ∧ Perm[Q] ∈ Γ)
Γ ; a ` x.m(y) : τ
(T-I NVOKE)
a = ocap =⇒ ocap(C)
∀ var f : σ ∈ f d. ∃ D. σ = D

(T-N EW)

Γ ; a ` new C : C
Perm[Q] ∈ Γ
Γ ; a ` x : Q . Box[C]
y : C ; ocap ` t : σ
Γ ; a ` x.open {y ⇒ t} : Q . Box[C]
ocap(C)

(T-O PEN)

Q fresh

Γ, x : Q . Box[C] , Perm[Q] ; a ` t : σ
Γ ; a ` box[C] {x ⇒ t} : ⊥

(T-B OX)

Figure 20. CLC2 term and expression typing.
The O CAP -* rules for CLC2 treat box-typed method
parameters analogously, and are left to the appendix.
Subclassing and Subtypes. In CLC2 , the subtyping relation <: is identical to that of CLC1 except for one additional
rule for the ⊥ type:
⊥ <: π (<:-B OT)
The <:-B OT rule says that ⊥ is a subtype of any type
π. (Note that type Null is a subtype of any surface type,
whereas π ranges over all types including guarded types.)

Γ ; a ` x : Q . Box[C]
Γ ; a ` y : Q0 . Box[D]
0
{Perm[Q], Perm[Q ]} ⊆ Γ
D <: f type(C, f )
Γ \ {Perm[Q0 ]}, z : Q . Box[C] ; a ` t : σ
Γ ; a ` capture(x.f, y) {z ⇒ t} : ⊥
(T-C APTURE)
Γ ; a ` x : Q . Box[C]
Γ ; a ` y : Q0 . Box[D0 ]
0
{Perm[Q], Perm[Q ]} ⊆ Γ
f type(C, f ) = Box[D]
D0 <: D
R fresh
Γ \ {Perm[Q0 ]}, z : R . Box[D], Perm[R] ; a ` t : σ
Γ ; a ` swap(x.f, y) {z ⇒ t} : ⊥
(T-S WAP)
Figure 21. Typing CLC2 ’s capture and swap.
swap.) T-O PEN requires the static permission Perm[Q] corresponding to the guarded type Q . Box[C] of the opened
box x to be available in Γ; this ensures consumed boxes
are never opened. Finally, T-B OX assigns a guarded type
Q . Box[C] to the newly created box x where Q is a fresh
abstract type; the permission Perm[Q] is available in the type
context of the continuation term t. The box expression itself
has type ⊥, since reduction never “returns”; t is the (only)
continuation.
Figure 21 shows the type rules for CLC2 ’s two new
expressions. Both rules require x and y to have guarded
types such that the corresponding permissions are available
in Γ. In both cases the permission of y is removed from the
environment used to type-check the continuation t; thus, box
y is consumed in each case. In its continuation, capture
provides access to box x under alias z; thus, z’s type is
equal to x’s type. In contrast, swap extracts the value of a
unique field and provides access to it under alias z in its
continuation. CLC2 ensures the value extracted from the
unique field is externally unique. Therefore, the type of z
is a guarded type R . Box[D] where R is fresh; permission
Perm[R] is created for use in continuation t.
Well-Formedness. CLC2 extends CLC1 with unique fields
of type Box[C] (see Figure 15); the following refined definition of well-typed heaps in CLC2 reflects this extension:
Definition 11 (Well-typed Heap). A heap H is well-typed,
written ` H : ? iff
∀o ∈ dom(H). H(o) = hC, F M i =⇒
(dom(F M ) = f ields(C) ∧
∀f ∈ dom(F M ). F M (f ) = null ∨

Term and Expression Typing. Figure 20 shows the changes
in the type rules. In T-I NVOKE, if the method parameter
has a type Box[D] then the argument y must have a type
Q . Box[D] such that the static permission Perm[Q] is available in Γ. (Otherwise, box y has been consumed.) T-N EW
checks that none of the field types are box types. This makes
sure classes with box-typed fields are only created using
box expressions. (Box-typed fields are then accessible using

(typeof (H, F M (f )) <: D ∧
f type(C, f ) ∈ {D, Box[D]}))

The most interesting additions of CLC2 with respect to
well-formedness concern (a) separation invariants and (b)
field uniqueness. In CLC1 , two boxes x and y are separate

as long as x is not an alias of y. In CLC2 , the separation
invariant is more complex, because capture merges two
boxes, and swap replaces the value of a unique field. The key
idea is to make separation conditional on the availability of
permissions.
Box separation for frames in CLC2 is defined as follows:
Definition 12 (Box Separation). For heap H and frame F ,
boxSep(H, F ) holds iff
F = hL, t, P il ∧ ∀x 7→ b(o, p), y 7→ b(o0 , p0 ) ∈ L. p 6=
0
p ∧ {p, p0 } ⊆ P =⇒ sep(H, o, o0 )
Two box references are disjoint if they are guarded by
two different permissions which are both available. As
soon as a box is consumed, e.g., via capture, box separation no longer holds, as expected. In other invariants like
boxObjSep, box permissions are not required. Similarly, the
differences in boxOcap and globalOcapSep are minor, and
therefore left to the appendix.
CLC2 ’s addition of unique fields requires a new field
uniqueness invariant for well-formed frames:
Definition 13 (Field Uniqueness). For heap H and frame
F = hL, t, P il , f ieldU niqueness(H, F ) holds iff
∀x 7→ b(o, p) ∈ L, o0 , ô ∈ dom(H).
p ∈ P ∧ reach(H, o, ô) ∧ H(ô) = hC, F M i ∧
f type(C, f ) = Box[D] ∧ reach(H, F M (f ), o0 ) =⇒
domedge(H, ô, f, o, o0 )
This invariant expresses the fact that all reference paths from
a box b(o, p) to an object o0 reachable from a unique field
f of object ô must “go through” that unique field. In other
words, in all reference paths from o to o0 , the edge (ô, f ) is a
dominating edge. (A precise definition of domedge appears
in the appendix.)
Frame Stack Invariants. The frame stack invariants of
CLC2 are extended to take the availability of permissions
into account. For example, box separation is now only preserved for boxes (a) that are not controlled by the same permission, and (b) whose permissions are available:
Definition 14 (Box Separation). Frame F and frame stack
F S satisfy the box separation property in H, written
boxSep(H, F, F S) iff
∀o, o0 ∈ dom(H). boxRoot(o, F, p) ∧
boxRoot(o0 , F S, p0 ) ∧ p 6= p0 =⇒ sep(H, o, o0 )
Note that the availability of permissions is required indirectly by the boxRoot predicate (its other details are uninteresting, and therefore omitted).

4.

Soundness

Theorem 3 (Preservation). If ` H : ? then:
1. If H ` F : σ, H ; a ` F ok, and H, F −→ H 0 , F 0
then ` H 0 : ?, H 0 ` F 0 : σ, and H 0 ; a ` F 0 ok.
2. If H ` F S, H ; a ` F S ok, and H, F S  H 0 , F S 0
then ` H 0 : ?, H 0 ` F S 0 , and H 0 ; b ` F S 0 ok.

σ, τ ::=
...
| Proc[C]

surface type
process type

e ::=
expression
...
| proc {(x : Box[C]) ⇒ t}
process creation
tc ::=
...
| send(x, y) {z ⇒ t}

continuation term
message send

Figure 22. Syntax extensions for concurrency.
Proof. Part (1) is proved by induction on the derivation of
H, F −→ H 0 , F 0 . Part (2) is proved by induction on
the derivation of H, F S  H 0 , F S 0 and part (1). (See
Appendix A.2 for the full proof.)
Theorem 4 (Progress). If ` H : ? then:
If H ` F S and H ; a ` F S ok then either H, F S 
H 0 , F S 0 or F S = hL, x, P il ◦  or F S = F ◦ GS where
• F = hL, let x = t in t0 , P il , t ∈ {y.f, y.f =

z, y.m(z), y.open {z ⇒ t00 }}, and L(y) = null; or
• F = hL, capture(x.f, y) {z ⇒ t}, P il where L(x) =
null ∧ L(y) = null; or
• F = hL, swap(x.f, y) {z ⇒ t}, P il where L(x) =
null ∧ L(y) = null.
Proof. By induction on the derivation of H ` F S. (See
Appendix A.3 for the full proof.)
Importantly, for a well-formed frame configuration,
CLC2 ensures that all required permissions are dynamically
available; thus, reduction is never stuck due to missing permissions.
4.1

Isolation

In order to state an essential isolation theorem, in the following we extend CLC2 with a simple form of messagepassing concurrency. This extension enables the statement
of Theorem 5 which expresses the fact that the type system
of CLC2 enforces data-race freedom in the presence of a
shared heap and efficient, by-reference message passing.
Figure 22 summarizes the syntax extensions. An expression of the form proc {(x : Box[C]) ⇒ t} creates a concurrent process which applies the function {(x : Box[C]) ⇒ t}
to each received message. A continuation term of the form
send(x, y) {z ⇒ t} asynchronously sends box y to process
x and then applies the continuation closure {z ⇒ t} to x.
Dynamic semantics. CLC3 extends the dynamic semantics of CLC2 such that the configuration of a program consists of a shared heap H and a set of processes P. Each pro-

F = hL, let x = proc {(y : Box[C]) ⇒ t0 } in t, P il
F 0 = hL[x 7→ o0 ], t, P il o0 fresh
H 0 = H[o0 7→ hBox[C], ∅, y → t0 i]
H, {(F ◦ F S)o } ∪ P

0

H 0 , {(F 0 ◦ F S)o , o } ∪ P
(E-P ROC)

F = hL, send(x, y) {z ⇒ t}, P il L(x) = o
H(o) = hBox[C], M, f i L(y) = b(o0 , p0 ) p0 ∈ P
F 0 = hL[z 7→ o], t, P \ {p0 }i
0
H = H[o 7→ hBox[C], M ∪ {o0 }, f i]
H, F ◦ F S  H 0 , F 0 ◦ 
(E-S END)
H(o) = hBox[C], M, x → ti M = M 0 ] {o0 }
F = hL, y, P il F 0 = h∅[x 7→ b(o0 , p)], t, {p}i p fresh
H 0 = H[o 7→ hBox[C], M 0 , x → ti]
H, {(F ◦ )o } ∪ P
H 0 , {(F 0 ◦ )o } ∪ P
(E-R ECEIVE)
3
Figure 23. CLC process transition rules.
cess F S o is a frame stack F S labelled with an object identifier o. A heap H maps the object identifier o of a process
F S o to a process record hBox[C], M, x → ti where Box[C]
is the type of messages the process can receive, M is a set
of object identifiers representing (buffered) incoming messages, and x → t is the message handler function. CLC3 introduces a third reduction relation H, P
H 0 , P 0 which
reduces a set of processes P in heap H.
Figure 23 shows the process transition rules. Rule EP ROC creates a new process by allocating a process record
with an empty received message set and the message type
and handler function as specified in the proc expression.
0
The new process o starts out with an empty frame stack,
since it is initially idle. Rule E-S END sends the object identifier in box y to process x. The required permission p0 of
box y is consumed in the resulting frame F 0 . The call stack
is discarded, since send is a continuation term. In rule ER ECEIVE process o is ready to process a message from its
non-empty set of incoming messages M , since (the term in)
frame F cannot be reduced further and there are no other
frames on the frame stack. (The ] operator denotes disjoint
set union.) Frame F 0 starts message processing with the parameter bound to a box reference with a fresh permission.
Static semantics. Figure 24 shows the well-formedness
rules that CLC3 introduces for (sets of) processes. A set
of processes is well-formed if each process is well-formed
(WF-S OUP). A process is well-formed if its frame stack is
well-formed (WF-P ROC).
Figure 25 shows the typing of process creation and message sending. Rule T-P ROC requires the body of a new process to be well-typed in an environment that only contains
the parameter of the message handler and a matching access permission which is fresh. Importantly, body term t is

H ` F So H ` P
H ` {F S o } ∪ P

(WF-S OUP)

H ` F S H ; a ` F S ok
H ` F So

(WF-P ROC)

Figure 24. CLC3 well-formedness rules.
x : Q . Box[C], Perm[Q] ; ocap ` t : π
Q fresh
(T-P ROC)
Γ ; a ` proc {(x : Box[C]) ⇒ t} : Proc[C]
Γ ; a ` x : Proc[C]
Γ ; a ` y : Q . Box[D]
Perm[Q] ∈ Γ
D <: C
Γ \ {Perm[Q]}, z : Proc[C] ; a ` t : π
(T-S END)
Γ ; a ` send(x, y) {z ⇒ t} : ⊥
Figure 25. CLC3 typing rules.
x 7→ o ∈ L ∨ (x 7→ b(o, p) ∈ L ∧ p ∈ P )
(ACC -F)
accRoot(o, hL, t, P il )
accRoot(o, F ) ∨ accRoot(o, F S)
(ACC -FS)
accRoot(o, F ◦ F S)
∀o, o0 ∈ dom(H). (accRoot(o, F S)
∧accRoot(o0 , F S 0 )) ⇒ sep(H, o, o0 )
(I SO -FS)
isolated(H, F S, F S 0 )
H(o) = hBox[C], M, f i
H(o0 ) = hBox[D], M 0 , gi
∀q ∈ M, q 0 ∈ M 0 . sep(H, q, q 0 )
isolated(H, F S, GS)
0

isolated(H, F S o , GS o )

(I SO -P ROC)

Figure 26. CLC3 process and frame stack isolation.
type-checked under effect ocap. This means that t may only
instantiate ocap classes. As a result, it is impossible to access global variables from within the newly created process.
Rule T-S END requires the permission Perm[Q] of sent box y
to be available in context Γ. The body t of the continuation
closure must be well-typed in a context where Perm[Q] is no
longer available. As with all continuation terms, the type of
a send term is ⊥.
Figure 26 defines a predicate isolated to express isolation
of frame stacks and processes. Isolation of frame stacks
builds on an accRoot predicate: identifier o is an accessible
root in frame F , written accRoot(o, F ), iff env(F ) contains
a binding x 7→ o or x 7→ b(o, p) where permission p is
available in F (ACC -F); o is an accessible root in frame stack
F S iff accRoot(o, F ) holds for any frame F ∈ F S (ACC FS). Two frame stacks are then isolated in H iff all their
accessible roots are disjoint in H (I SO -FS). Finally, two

processes are isolated iff their message queues and frame
stacks are disjoint (I SO -P ROC).
Theorem 5 (Isolation). If ` H : ? then:
If H ` P, ∀P, P 0 ∈ P. P 6= P 0 =⇒ isolated(H, P, P 0 ),
and H, P
H 0 , P 0 then ` H 0 : ?, H 0 ` P 0 , and
0
0
∀Q, Q ∈ P . Q 6= Q0 =⇒ isolated(H 0 , Q, Q0 ).
Theorem 5 states that
preserves isolation of welltyped processes. Isolation is preserved even when boxes are
transferred by reference between concurrent processes. Informally, the validity of this statement rests on the preservation of well-formedness of frames, frame stacks, and processes; well-formedness guarantees the separation of boxes
with available permissions (def. 12 and def. 14), and the
separation of boxes with available permissions from objects
“outside” of boxes (def. 15 and def. 17 in A.1).

5.

Implementation

L AC ASA is implemented as a combination of a compiler
plugin for the current Scala 2 reference compiler and a runtime library. The plugin extends the compilation pipeline
with an additional phase right after regular type checking. Its
main tasks are (a) object-capability checking, (b) checking
the stack locality of boxes and permissions, and (c) checking the constraints of L AC ASA expressions. In turn, (c) requires object-capability checking: type arguments of mkBox
invocations must be object-capability safe, and open bodies
may only instantiate object-capability safe classes. Certain
important constraints are implemented using spores [45].
Object-Capability Checking in Scala. Our empirical study
revealed the importance of certain Scala-specific “tweaks”
to conventional object-capability checking. We describe the
most important one. The Scala compiler generates so-called
“companion” singleton objects for case classes and custom
value classes if the corresponding companions do not already exist. For a case class such a synthetic companion object provides, e.g., factory and extractor [30] methods. Synthetic companion objects are object-capability safe.
Leveraging Spores. We leverage constraints supported by
spores in several places in L AC ASA. We provide two examples where spores are used in our implementation.
The first example is the body of an open expression.
According to the rules of L AC ASA, it is not allowed to have
free variables (see Section 2). Using spores, this constraint
can be expressed in the type of the open method as follows:
def open(fun: Spore[T, Unit])(implicit
acc: CanAccess { type C = self.C },
noCapture: OnlyNothing[fun.Captured]): Unit

Besides the implicit access permission, the method also
takes an implicit parameter of type
OnlyNothing[fun.Captured]. The generic OnlyNothing
type is a trivial type class with only a single instance, namely
for type Nothing, Scala’s bottom type. Consequently, for

an invocation of open, the compiler is only able to resolve
the implicit parameter noCapture in the case where type
fun.Captured is equal to Nothing. In turn, spores ensure
this is only the case when the fun spore does not capture
anything.
The second example where L AC ASA leverages spores is
permission consumption in swap:
def swap[S](select: T => Box[S])
(assign: (T, Box[S]) => Unit, b: Box[S])
(fun: Spore[Packed[S], Unit] {
type Excluded = b.C
})
(implicit acc: CanAccess { type C = b.C }): Unit

Besides the field accessor functions select and assign
(see Section 2), swap receives a box b to be put into the
unique field. The implicit acc parameter ensures the availability of b’s permission. Crucially, b’s permission is consumed by the assignment to the unique field. Therefore, b
must not be accessed in the continuation spore, which is expressed using the spore’s Excluded type member. As a result, fun’s body can no longer capture the permission.
5.1

Discarding the stack using exceptions

Certain L AC ASA operations require discarding the stack
of callers in order to ensure consumed access permissions
become unavailable. For example, recall the message send
shown in Figure 2 (see Section 2):
s.next.send(packed.box)({
// continuation closure
})(access)
// unreachable

Here, the send invocation consumes the access permission:
the permission is no longer available in the continuation.
This semantics is enforced by ensuring (a) the access permission is unavailable within the explicit continuation closure (line 2), and (b) code following the send invocation
(line 4) is unreachable. The former is enforced analogously
to swap discussed above. The latter is enforced by discarding the stack of callers.
Discarding the call stack is a well-known technique in
Scala, and has been widely used in the context of eventbased actors [37] where the stack of callers is discarded
when an actor suspends with just a continuation closure.7
The implementation consists of throwing an exception which
unwinds the call stack up to the actor’s event-loop, or up to
the boundary of a concurrent task.
Prior to throwing the stack-unwinding exception, operations like send invoke their continuation closure which is
provided explicitly by the programmer:
def send(msg: Box[T])(cont: NullarySpore[Unit] {...})
(implicit acc: CanAccess {...}): Nothing = {
7 See

https://github.com/twitter-archive/kestrel/blob/
3e64b28ad4e71256213e2bd6e8bd68a9978a2486/src/main/scala/
net/lag/kestrel/KestrelHandler.scala for a usage example in a
large-scale production system.

// continuation closure
})(access)
} catch {
case c: ControlThrowable => // do nothing
}
other.send(packed.box)({
...
})(access)

class MessageHandlerTask(
receiver: Actor[T],
packed: Packed[T]) extends Runnable {
def run(): Unit = {
// process message in ‘packed‘ object
try {
// invoke ‘receive‘ method of ‘receiver‘ actor
receiver.receive(packed.box)(packed.access)
} catch {
case nrc: NoReturnControl => /* do nothing */
}
// check for next message
...
}
...
}

Figure 27. Handling NoReturnControl within actors.
...
cont()

// enqueue message
// invoke continuation closure
throw new NoReturnControl // discard stack
}

The thrown NoReturnControl exception is caught either
within the main thread where the main method is wrapped
in a try-catch (see below), or within a worker thread
of the actor system’s thread pool. In the latter case, the
task that executes actor code catches the NoReturnControl
exception, as shown in Figure 27. Note that the exception
handler is at the actor’s “top level:” after processing the
received message (in packed) the receiver actor is ready
to process the next message (if any).
Scala’s standard library provides a special
ControlThrowable type for such cases where exceptions
are used to manage control flow. The above
NoReturnControl type extends ControlThrowable. The
latter is defined as follows:
trait ControlThrowable extends Throwable
with NoStackTrace

Mixing in the NoStackTrace trait disables the generation
of JVM stack traces, which is expensive but not required.
The ControlThrowable type enables exception handling
without disturbing exception-based control-flow transfers:
try { ... } catch {
case c: ControlThrowable => throw c // propagate
case e: Exception => ...
}

Crucially, exceptions of a subtype of ControlThrowable
are propagated in order not to influence the in-progress control flow transfer. Patterns such as the above are unchecked
in Scala. However, in the case of L AC ASA, failure to propagate ControlThrowables could result in unsoundness. For
example, consider the following addition of a try-catch
to the previous example (shown at the beginning of Section 5.1):
try {
s.next.send(packed.box)({

By catching and not propagating the ControlThrowable,
the access permission remains accessible from line 8, enabling sending the same object (packed.box) twice.
In order to prevent such soundness issues, the L A C ASA compiler plugin checks try-catch expressions: a
valid catch clause either (a) does not match any
ControlThrowable, or (b) is preceeded by a catch clause
that matches and propagates ControlThrowable exceptions. Furthermore, to support trusted L AC ASA code, a
marker method permits unsafe catches. For example, the
main method of a L AC ASA program is wrapped in the following trusted try-catch:
try { /* main method body */ } catch {
case nrc: NoReturnControl => uncheckedCatchControl
}

6.

Empirical Evaluation

The presented approach to object isolation and uniqueness
is based on object capabilities. Isolation is enforced only
for instances of ocap classes, i.e., classes adhering to the
object-capability discipline. Likewise, ownership transfer is
supported only for instances of ocap classes. Therefore, it is
important to know whether the object-capability discipline
imposes an undue burden on developers; or whether, on the
contrary, developers tend to design classes and traits in a
way that naturally follows the object-capability discipline.
Specifically, our empirical evaluation aims to answer the
following question: How many classes/traits in medium to
large open-source Scala projects already satisfy the objectcapability constraints required by L AC ASA?
Methodology For our empirical analysis we selected Scala’s
standard library, a large and widely-used class library, as
well as two medium to large open-source Scala applications. In total, our corpus comprises 78,617 source lines of
code (obtained using [26]). Determining the prevalence of
ocap classes and traits is especially important in the case of
Scala’s standard library, since it tells us for which classes/traits L AC ASA supports isolation and ownership transfer
“out of the box,” i.e., without code changes. (We will refer
to both classes and traits as “classes” in the following.)
The two open-source applications are Signal/Collect
(S/C) and GeoTrellis. S/C [61] is a distributed graph processing framework with applications in machine learning and the
semantic web, among others. Concurrency and distribution
are implemented using the Akka actor framework [42]. Consequently, S/C could also benefit from L AC ASA’s additional

Project
Scala Standard Library
Signal/Collect
GeoTrellis
-engine
-raster
-spark
Total

Version
2.11.7
8.0.6
0.10.0-RC2

SLOC
33,107
10,159

GitHub stats
5,795
257
123
11
400
38

#classes/traits
1,505
236

#ocap (%)
644 (43%)
159 (67%)

#dir. insec. (%)
212/861 (25%)
60/77 (78%)

190
670
326
2,927

40 (21%)
233 (35%)
101 (31%)
1,177 (40%)

124/150 (83%)
325/437 (74%)
167/225 (74%)
888/1,750 (51%)

3,868
22,291
9,192
78,617

Figure 28. Evaluating the object-capability discipline in real Scala projects. Each project is an active open-source project
hosted on GitHub. represents the number of “stars” (or interest) a repository has on GitHub, and
represents the number
of contributors of the project.
safety. GeoTrellis is a high performance data processing engine for geographic data, used by the City of Asheville [17]
(NC, USA) and the U.S. Army, among others. Like S/C,
GeoTrellis utilizes actor concurrency through Akka.
In each case we performed a clean build with the L A C ASA compiler plugin enabled. We configured the plugin to
check ocap constraints for all compiled classes. In addition,
we collected statistics on classes that directly violate ocap
constraints through accesses to global singleton objects.
Results Figure 28 shows the collected statistics.
For Scala’s standard library we found that 43% of all
classes follow the object-capability discipline. While this
number might seem low, it is important to note that a
strict form of ocap checking was used: accesses to toplevel singleton objects were disallowed, even if these singletons were themselves immutable and object-capability safe.
Thus, classes directly using helper singletons were marked
as insecure. Interestingly, only 25% of the insecure classes
directly access top-level singleton objects. This means, the
majority of insecure classes is insecure due to dependencies
on other insecure classes. These results can be explained
as follows. First, helper singletons (in particular, “companion objects”) play an important role in the architecture of
Scala’s collections package [52]. In turn, with 22,958 SLOC
the collections package is by far the library’s largest package, accounting for 69% of its total size. Second, due to the
high degree of reuse enabled by techniques such as the type
class pattern [24], even a relatively small number of classes
that directly depend on singletons leads to an overall 57% of
insecure classes.
In S/C 67% of all classes satisfy strict ocap constraints, a
significantly higher percentage than for the Scala library. At
the same time, the percentage of classes that are not ocap due
to direct accesses to top-level singletons is also much higher
(78% compared to 25%). This means there is less reuse of insecure classes in S/C. All analyzed components of GeoTrellis have a similarly high percentage of “directly insecure”
classes. Interestingly, even with its reliance on “companion
objects” and its high degree of reuse, the proportion of ocap
classes in the standard library is significantly higher compared to GeoTrellis where it ranges between 21% and 35%.

Immutability and object capabilities Many singleton objects in Scala’s standard library (a) are deeply immutable,
(b) only create instances of ocap classes, and (c) never access global state. Such singletons are safe to access from
within ocap classes.8 To measure the impact of such singletons on the proportion of ocap classes, we reanalyzed S/C
with knowledge of safe singletons in the standard library. As
a result, the percentage of ocap classes increased from 67%
to 79%, while the proportion of directly insecure classes remained identical. Thus, knowledge of “safe singleton objects” is indeed important for object capabilities in Scala.

7.

Other Related Work

A number of previous approaches leverages permissions or
capabilities for uniqueness or related notions. Approaches
limited to tree-shaped object structures for unique references
include [15, 16, 51, 57, 64, 65]. In contrast, L AC ASA provides external uniqueness [18], which allows internallyaliased object graphs. Permissions in L AC ASA indicate
which objects (“boxes”) are accessible in the current scope.
In contrast, the deny capabilities of the Pony language [22]
indicate which operations are denied on aliases to the same
object. By distinguishing read/write as well as (actor-)local
and global aliases, Pony derives a fine-grained matrix of
reference capabilities, which are more expressive than the
presented system. While Pony is a new language design, L A C ASA integrates affine references into an existing language,
while minimizing the effort for reusing existing classes.
The notion of uniqueness provided by our system is
similar to UTT [49], an extension of Universe types [28]
with ownership transfer. Overall, UTT is more flexible,
whereas L AC ASA requires fewer annotations for reusing
existing code; it also integrates with Scala’s local type inference. Active ownership [19] shares our goal of providing a
minimal type system extension, however it requires ownerpolymorphic methods and existential owners whose integration with local type inference is not clear. A more general
overview of ownership-based aliasing control is provided
in [20]. There is a long line of work on unique object ref8 Analogous

rules have been used for static fields in Joe-E [44], an objectcapability secure subset of Java.

erences [4, 10, 14, 40, 48] which are more restrictive than
external uniqueness; a recurring theme is the interaction between unique, immutable, and read-only references, which
is also exploited in a variant of C# for systems programming [35]. Several systems combine ownership with concurrency control to prevent data races. RaceFree Java [1]
associates fields with locks, and an effect system ensures
correct lock acquisition. Boyapati et al. [13] and Zhao [67]
extend type system guarantees to deadlock prevention.
Our system takes important inspiration from Loci [66], a
type system for enforcing thread locality which requires very
few source annotations. However, L AC ASA supports ownership transfer, which is outside the domain of Loci. Kilim [60]
combines type qualifiers with an intra-procedural shape
analysis to ensure isolation of Java-based actors. To simplify
the alias analysis and annotation system, messages must be
tree-shaped. Messages in L AC ASA are not restricted to trees;
moreover, L AC ASA uses a type-based approach rather than
static analysis. StreamFlex [59] and FlexoTasks [9] are implicit ownership systems for stream-based programming;
like L AC ASA, they allow reusing classes which pass certain sanity checks, but the systems are more restrictive than
external uniqueness.

8.

Conclusion

This paper presents a new approach to integrating isolation
and uniqueness into an existing full-featured language. A
key novelty of the system is its minimization of annotations
necessary for reusing existing code. Only a single bit of information per class is required to determine its reusability.
Interestingly, this information is provided by the object capability model, a proven methodology for applications in security, such as secure sandboxing. We present a complete
formal account of our system, including proofs of key soundness theorems. We implement the system for the full Scala
language, and evaluate the object capability model on a corpus of over 75,000 LOC of popular open-source projects.
Our results show that between 21% and 79% of the classes
of a project adhere to a strict object capability discipline. In
summary, we believe our approach has the potential to make
a flexible form of uniqueness practical on a large scale and
in existing languages with rich type systems.

References
[1] M. Abadi, C. Flanagan, and S. N. Freund. Types for safe
locking: Static race detection for Java. ACM Trans. Program.
Lang. Syst, 28(2):207–255, 2006.
[2] G. A. Agha. ACTORS: A Model of Concurrent Computation
in Distributed Systems. Series in Artificial Intelligence. The
MIT Press, Cambridge, Massachusetts, 1986.
[3] J. Aldrich, V. Kostadinov, and C. Chambers. Alias annotations
for program understanding. In OOPSLA, pages 311–330,
2002.

[4] P. S. Almeida. Balloon types: Controlling sharing of state in
data types. In ECOOP, pages 32–59, 1997.
[5] N. Amin, T. Rompf, and M. Odersky. Foundations of pathdependent types. In OOPSLA, pages 233–249, 2014.
[6] N. Amin, S. Grütter, M. Odersky, T. Rompf, and S. Stucki.
The essence of dependent object types. In A List of Successes
That Can Change the World, pages 249–272. Springer, 2016.
[7] B. Anderson, L. Bergstrom, D. Herman, J. Matthews,
K. McAllister, M. Goregaokar, J. Moffitt, and S. Sapin. Experience report: Developing the servo web browser engine using
rust. CoRR, abs/1505.07383, 2015.
[8] J. Armstrong, R. Virding, C. Wikström, and M. Williams.
Concurrent Programming in Erlang. Prentice Hall, 1996.
[9] J. S. Auerbach, D. F. Bacon, R. Guerraoui, J. H. Spring, and
J. Vitek. Flexible task graphs: a unified restricted thread
programming model for Java. In LCTES, pages 1–11, 2008.
[10] H. G. Baker. ’use-once’ variables and linear objects - storage management, reflection and multi-threading. SIGPLAN
Notices, 30(1):45–52, 1995.
[11] G. Bierman, M. Parkinson, and A. Pitts. MJ: An imperative
core calculus for Java and Java with effects. Technical Report UCAM-CL-TR-563, University of Cambridge, Computer
Laboratory, Apr. 2003.
[12] G. M. Bierman, C. V. Russo, G. Mainland, E. Meijer, and
M. Torgersen. Pause ’n’ play: Formalizing asynchronous C#.
In ECOOP, pages 233–257, 2012.
[13] C. Boyapati, R. Lee, and M. C. Rinard. Ownership types for
safe programming: preventing data races and deadlocks. In
OOPSLA, pages 211–230, 2002.
[14] J. Boyland. Alias burying: Unique variables without destructive reads. Softw, Pract. Exper, 31(6):533–553, 2001.
[15] J. Boyland. Checking interference with fractional permissions. In SAS, pages 55–72, 2003.
[16] L. Caires and J. C. Seco. The type discipline of behavioral
separation. In POPL, pages 275–286, 2013.
[17] City of Asheville, NC, USA. Priority Places project. http:
//priorityplaces.ashevillenc.gov/.
[18] D. Clarke and T. Wrigstad. External uniqueness is unique
enough. In ECOOP, pages 176–200, 2003.
[19] D. Clarke, T. Wrigstad, J. Östlund, and E. B. Johnsen. Minimal ownership for active objects. In APLAS, pages 139–154,
2008.
[20] D. Clarke, J. Östlund, I. Sergey, and T. Wrigstad. Ownership
types: A survey. In D. Clarke, J. Noble, and T. Wrigstad,
editors, Aliasing in Object-Oriented Programming, volume
7850 of Lecture Notes in Computer Science, pages 15–58.
Springer, 2013.
[21] D. G. Clarke, J. Potter, and J. Noble. Ownership types for
flexible alias protection. In OOPSLA, pages 48–64, 1998.
[22] S. Clebsch, S. Drossopoulou, S. Blessing, and A. McNeil.
Deny capabilities for safe, fast actors. In AGERE!@SPLASH,
pages 1–12. ACM, 2015.
[23] D. Crockford. ADsafe. http://www.adsafe.org, 2011.

[24] B. C. d. S. Oliveira, A. Moors, and M. Odersky. Type classes
as objects and implicits. In OOPSLA, pages 341–360, 2010.
[25] B. C. d. S. Oliveira, T. Schrijvers, W. Choi, W. Lee, and
K. Yi. The implicit calculus: a new foundation for generic
programming. In PLDI, pages 35–44, 2012.
[26] A. Danial and contributors.
cloc.
http://cloc.
sourceforge.net/, 2006. Accessed: 2016-03-20.
[27] J. B. Dennis and E. C. V. Horn. Programming semantics for
multiprogrammed computations. Commun. ACM, 9(3):143–
155, 1966.
[28] W. Dietl and P. Müller. Universes: Lightweight ownership for
JML. Journal of Object Technology, 4(8):5–32, 2005.
[29] W. Dietl, S. Dietzel, M. D. Ernst, K. Muslu, and T. W. Schiller.
Building and using pluggable type-checkers. In ICSE, pages
681–690, 2011.
[30] B. Emir, M. Odersky, and J. Williams. Matching objects with
patterns. In ECOOP, pages 273–298, 2007.
[31] J. Epstein, A. P. Black, and S. L. P. Jones. Towards Haskell in
the cloud. In Haskell, pages 118–129, 2011.
[32] Ericsson AB. Erlang/OTP. https://github.com/erlang/
otp, 2010. Accessed: 2016-07-10.
[33] M. Fähndrich and R. DeLine. Adoption and focus: Practical
linear types for imperative programming. In PLDI, pages 13–
24, 2002.
[34] C. Flanagan, A. Sabry, B. F. Duba, and M. Felleisen. The
essence of compiling with continuations. In PLDI, pages 237–
247, 1993.
[35] C. S. Gordon, M. J. Parkinson, J. Parsons, A. Bromfield, and
J. Duffy. Uniqueness and reference immutability for safe
parallelism. In OOPSLA, pages 21–40, 2012.
[36] P. Haller. On the integration of the actor model in mainstream
technologies: the Scala perspective. In AGERE!@SPLASH,
pages 1–6, 2012.
[37] P. Haller and M. Odersky. Scala actors: Unifying thread-based
and event-based programming. Theor. Comput. Sci, 410(2-3):
202–220, 2009.
[38] P. Haller and M. Odersky. Capabilities for uniqueness and
borrowing. In ECOOP, pages 354–378, 2010.

[45] H. Miller, P. Haller, and M. Odersky. Spores: A type-based
foundation for closures in the age of concurrency and distribution. In ECOOP, pages 308–333, 2014.
[46] M. S. Miller. Robust Composition: Towards a Unified Approach to Access Control and Concurrency Control. PhD thesis, Johns Hopkins University, May 2006.
[47] M. S. Miller, M. Samuel, B. Laurie, I. Awad, and M. Stay.
Caja: Safe active content in sanitized JavaScript. Google, Inc.,
Tech. Rep, 2008.
[48] N. H. Minsky. Towards alias-free pointers. In ECOOP, pages
189–209, 1996.
[49] P. Müller and A. Rudich. Ownership transfer in universe
types. In OOPSLA, pages 461–478, 2007.
[50] J. Noble, J. Vitek, and J. Potter. Flexible alias protection. In
ECOOP, pages 158–185, 1998.
[51] M. Odersky. Observers for linear types. In ESOP, pages 390–
407, 1992.
[52] M. Odersky and A. Moors. Fighting bit rot with types (experience report: Scala collections). In FSTTCS, pages 427–451,
2009.
[53] M. Odersky, C. Zenger, and M. Zenger. Colored local type
inference. In POPL, pages 41–53, 2001.
[54] M. Odersky, P. Altherr, V. Cremet, G. Dubochet, B. Emir,
P. Haller, S. Micheloud, N. Mihaylov, A. Moors, L. Rytz,
M. Schinz, E. Stenman, and M. Zenger. The Scala language
specification version 2.11. http://www.scala-lang.org/
files/archive/spec/2.11/, Apr. 2014.
[55] J. Östlund and T. Wrigstad. Welterweight Java. In TOOLS,
pages 97–116, 2010.
[56] J. G. Politz, S. A. Eliopoulos, A. Guha, and S. Krishnamurthi.
ADsafety: Type-based verification of JavaScript sandboxing.
CoRR, abs/1506.07813, 2015.
[57] F. Pottier and J. Protzenko. Programming with permissions in
Mezzo. In ICFP, pages 173–184, 2013.
[58] L. Rytz. A Practical Effect System for Scala. PhD thesis,
EPFL, Lausanne, Switzerland, Sept. 2013.

[39] C. Hewitt. Viewing control structures as patterns of passing
messages. Artif. Intell, 8(3):323–364, 1977.

[59] J. H. Spring, J. Privat, R. Guerraoui, and J. Vitek. Streamflex:
high-throughput stream programming in Java. In OOPSLA,
pages 211–228, 2007.

[40] J. Hogg. Islands: Aliasing protection in object-oriented languages. In OOPSLA, pages 271–285, 1991.

[60] S. Srinivasan and A. Mycroft. Kilim: Isolation-typed actors
for Java. In ECOOP, pages 104–128, 2008.

[41] A. Igarashi, B. C. Pierce, and P. Wadler. Featherweight Java: a
minimal core calculus for Java and GJ. ACM Trans. Program.
Lang. Syst, 23(3):396–450, 2001.

[61] P. Stutz, A. Bernstein, and W. W. Cohen. Signal/Collect:
Graph algorithms for the (semantic) web. In ISWC, pages
764–780, 2010.

[42] Lightbend, Inc. Akka. http://akka.io/, 2009. Accessed:
2016-03-20.

[62] M. Tofte and J.-P. Talpin. Implementation of the typed callby-value lambda-calculus using a stack of regions. In POPL,
pages 188–201, 1994.

[43] J. Mackay, H. Mehnert, A. Potanin, L. Groves, and
N. Cameron. Encoding Featherweight Java with assignment
and immutability using the Coq proof assistant. In FTfJP,
pages 11–19, 2012.
[44] A. Mettler, D. Wagner, and T. Close. Joe-E: A securityoriented subset of Java. In NDSS, 2010.

[63] M. Tofte and J.-P. Talpin. Region-based memory management. Inf. Comput, 132(2):109–176, 1997.
[64] P. Wadler. Linear types can change the world! In Programming Concepts and Methods, pages 561–581. North Holland,
1990.

[65] E. M. Westbrook, J. Zhao, Z. Budimlic, and V. Sarkar. Practical permissions for race-free parallelism. In ECOOP, pages
614–639, 2012.
[66] T. Wrigstad, F. Pizlo, F. Meawad, L. Zhao, and J. Vitek. Loci:
Simple thread-locality for Java. In ECOOP, pages 445–469,
2009.
[67] Z. Y. Concurrency Analysis Based On Fractional Permission
System. PhD thesis, University of Wisconsin–Milwaukee,
2007.

x 7→ b(o, p) ∈ L
p∈P
boxRoot(o, hL, t, P il )

p ` class C extends D {f d md}
C `ocap md
ocap(D)
∀ var f : σ ∈ f d. ocap(σ) ∨ σ = Box[E] ∧ ocap(E)
ocap(C)
(O CAP -C LASS)

boxRoot(o, F )
boxRoot(o, F ◦ )

this : C, x : D ; ocap ` t : E 0
E 0 <: E
C `ocap def m(x : D) : E = t
(O CAP -M ETHOD 1)

boxRoot(o, F ) ∨ boxRoot(o, F S)
boxRoot(o, F ◦ F S)
x 7→ b(o, p) ∈ L
p∈P
boxRoot(o, hL, t, P il , p)

Γ = this : C, x : Q . Box[D], Perm[Q]
Q fresh
Γ ; ocap ` t : E 0
E 0 <: E
C `ocap def m(x : Box[D]) : E = t
(O CAP -M ETHOD 2)
Figure 29. Well-formed ocap classes.
γ : permT ypes(Γ) −→ P injective
∀x ∈ dom(Γ),
Γ(x) = Q . Box[C] ∧ L(x) = b(o, p) ∧ Perm[Q] ∈ Γ =⇒
γ(Q) = p
` Γ; L; P
(WF-P ERM)
L(x) = null ∨
L(x) = o ∧ typeof (H, o) <: Γ(x) ∨
L(x) = b(o, p) ∧ Γ(x) = Q . Box[C] ∧
typeof (H, o) <: C
(WF-VAR)
H ` Γ; L; x
Γ; a`t:σ
H ` Γ; L

l 6=  =⇒ σ <: C
H ` Γ; L; P

H ` hL, t, P il : σ
Γ, x : τ ; a ` t : σ
H ` Γ; L

l 6=  =⇒ σ <: C
H ` Γ; L; P

H `τx hL, t, P il : σ

(T-F RAME 1)

(T-F RAME 2)

boxSep(H, F )
boxObjSep(H, F )
boxOcap(H, F )
a = ocap =⇒ globalOcapSep(H, F )
f ieldU niqueness(H, F )
(F- OK)
H ; a ` F ok
Figure 30. Frame and frame stack typing.

boxRoot(o, F, p)
boxRoot(o, F ◦ , p)
boxRoot(o, F, p) ∨ boxRoot(o, F S, p)
boxRoot(o, F ◦ F S, p)
x 7→ o0 ∈ env(F )
reach(H, o, o0 )
openbox(H, o, F, F S)
Figure 31. Auxiliary predicates.

boxRoot(o, F S)

Definition 15 (Box-Object Separation). Frame F satisfies
the box-object separation invariant in H, written
boxObjSep(H, F ), iff
F = hL, t, P il ∧∀x 7→ b(o, p), y 7→ o0 ∈ L. sep(H, o, o0 )
Definition 16 (Box Ocap Invariant). Frame F satisfies the
box ocap invariant in H, written boxOcap(H, F ), iff
F = hL, t, P il ∧ ∀x 7→ b(o, p) ∈ L, o0 ∈ dom(H). p ∈
P ∧ reach(H, o, o0 ) =⇒ ocap(typeof (H, o0 ))
Definition 17 (Global Ocap Separation). Frame F satisfies the global ocap separation invariant in H, written
globalOcapSep(H, F ), iff
F = hL, t, P il ∧ ∀x 7→ o ∈ L, y 7→ o0 ∈ L0 .
ocap(typeof (H, o)) ∧ sep(H, o, o0 )
Definition 18 (Dominating Edge). Field f of ô is a dominating edge for paths from o to o0 in H, written
domedge(H, ô, f, o, o0 ), iff
∀P ∈ path(H, o, o0 ). P = o . . . ô, F M (f ) . . . o0
where H(ô) = hC, F M i and f ∈ dom(F M ).
Definition 19. permT ypes(Γ) is the set of permissions in a
typing context Γ,
permT ypes(Γ) = {Q | Perm[Q] ∈ Γ}

A.

Full Proofs

A.2

A.1

Additional Rules and Definitions

Lemma 1. If ` H : ? then:
If H ` F : σ, H ; a ` F ok, and H, F −→ H 0 , F 0 then
` H 0 : ?, H 0 ` F 0 : σ, and H 0 ; a ` F 0 ok.

Figure 29 shows CLC2 ’s O CAP -* rules. Figure 30 shows
the updated rules for frame and frame stack typing in
CLC2 . Figure 31 shows the auxiliary predicates boxRoot
and openbox.

Proof of Theorem 3

Proof. By induction on the derivation of H, F −→ H 0 , F 0 .
- Case E-Null

H, hL, let x = null in t, P il
−→ H, hL[x 7→ null], t, P il

(E-N ULL)

H, hL, let x = y in t, P il
−→ H, hL[x 7→ L(y)], t, P il

(E-VAR)

H(L(y)) = hC, F M i
f ∈ dom(F M )
(E-S ELECT)
H, hL, let x = y.f in t, P il
−→ H, hL[x 7→ F M (f )], t, P il
L(y) = o
H(o) = hC, F M i
H 0 = H[o 7→ hC, F M [f 7→ L(z)]i]
(E-A SSIGN)
H, hL, let x = y.f = z in t, P il
−→ H 0 , hL, let x = z in t, P il
o∈
/ dom(H)
f ields(C) = f
H 0 = H[o 7→ hC, f 7→ nulli]
H, hL, let x = new C in t, P il
−→ H 0 , hL[x 7→ o], t, P il

(E-N EW)

Figure 32. CLC2 frame transition rules.

1. By the assumptions
(a) ` H : ?
(b) H ` F : σ
(c) H ; a ` F ok
(d) H, F −→ H, F 0
(e) F = hL, let x = null in t, P il
(f) F 0 = hL[x 7→ null], t, P il
2. By 1.b), 1.e), and T-Frame1
(a) Γ ; b ` let x = null in t : σ
(b) l 6=  =⇒ σ <: C
(c) H ` Γ; L
(d) ` Γ; L; P
3. By 2.a) and T-Let
(a) Γ ; b ` null : τ
(b) Γ, x : τ ; b ` t : σ
4. Define
(a) Γ0 := Γ, x : τ
(b) L0 := L[x 7→ null]
5. By 4.a-b) and WF-Var, H ` Γ0 ; L0 ; x
6. By 2.c), 4.a-b), 5., and WF-Env, H ` Γ0 ; L0
7. By 4.a-b),
(a) permT ypes(Γ0 ) = permT ypes(Γ)
(b) ∀(x, o, p), L(x) = b(o, p) ⇐⇒ L0 (x) = b(o, p)
8. By 2.d), 7.a-b), WF-Perm, ` Γ0 ; L0 ; P
9. By 2.b), 3.b), 4.a-b), 6., 8., and T-Frame1, H ` F 0 : σ
10. By 1.c), 1.e-f), and F-ok, H ; a ` F 0 ok
11. 1.a), 7., and 9. conclude this case.
- Case E-Select
1. By the assumptions
(a) ` H : ?

(b) H ` F : σ
(c) H ; a ` F ok
(d) H, F −→ H, F 0
2. By 1.d) and E-Select
(a) F = hL, let x = y.f in t, P il
(b) H(L(y)) = hC, F M i
(c) f ∈ dom(F M )
(d) F 0 = hL[x 7→ F M (f )], t, P il
3. By 1.b), 2.a), and T-Frame1
(a) Γ ; b ` let x = y.f in t : σ
(b) l 6=  =⇒ σ <: E 0
(c) H ` Γ ; L
(d) ` Γ; L; P
4. By 3.a) and T-Let
(a) Γ ; b ` y.f : τ
(b) Γ, x : τ ; b ` t : σ
5. By 4.a) and T-Select
(a) Γ ; b ` y : D
(b) f type(D, f ) = E
(c) τ = E
6. By 5.a) and T-Var, Γ(y) = D
7. By 3.c), 6., and WF-Env, H ` Γ; L; y
8. By 2.b), 6., 7., and WF-Var, C = typeof (H, L(y)) <:
D
9. By 8., <:-Ext, and WF-Class, f type(C, f ) = f type(D, f )
10. By 1.a), 2.b-c), and def. 2, F M (f ) = null ∨
typeof (H, F M (f )) <: f type(C, f )
11. Define
(a) Γ0 := Γ, x : E
(b) L0 := L[x 7→ F M (f )]
12. By 5.b), 9., 10., and 11.b), L0 (x) = null ∨
typeof (H, L0 (x)) <: E
13. By 11.a-b), 12., and WF-Var, H ` Γ0 ; L0 ; x
14. By 3.c), 11.a-b), 13., and WF-Env, H ` Γ0 ; L0
15. By 4.b), 5.c), and 11.a), Γ0 ; b ` t : σ
16. By 10., 11.a-b),
(a) permT ypes(Γ0 ) = permT ypes(Γ)
(b) ∀(x, o, p), L(x) = b(o, p) ⇐⇒ L0 (x) = b(o, p)
17. By 3.d), 16.a-b), WF-Perm, ` Γ0 ; L0 ; P
18. By 2.d), 3.b), 14., 15., 17 and T-Frame1, H ` F 0 : σ
19. By 1.c), 2.a-d), and F-ok, H ; a ` F 0 ok
20. 1.a), 18., and 19. conclude this case.
- Case E-Assign
1. By the assumptions
(a) ` H : ?
(b) H ` F : σ
(c) H ; a ` F ok
(d) H, F −→ H 0 , F 0
2. By 1.d) and E-Assign
(a) F = hL, let x = y.f = z in t, P il

(b) L(y) = o
25. By 1.c), 2.a-e), 17., 19., 24., and F-ok, H 0 ; a ` F 0 ok
(c) H(o) = hC, F M i
26. By 5.c), 11., and <:-Trans, L(z) = null ∨
typeof (H, L(z)) <: f type(D, f )
(d) H 0 = H[o 7→ hC, F M [f 7→ L(z)]i]
27. By 5.a) and T-Var, Γ(y) = D
(e) F 0 = hL, let x = z in t, P il
28. By 3.c), 27., and WF-Env, H ` Γ; L; y
3. By 1.b), 2.a), and T-Frame1
29.
By 2.b), 27., 28., and WF-Var, typeof (H, L(y)) <:
(a) Γ ; b ` let x = y.f = z in t : σ
0
D
(b) l 6=  =⇒ σ <: E
30. By 2.b-c), 29., and def. 2, C <: D
(c) H ` Γ; L
31. By 30., <:-Ext, and WF-Class, f type(C, f ) = f type(D, f )
(d) ` Γ; L; P
32. By 26. and 31., L(z) = null ∨ typeof (H, L(z)) <:
4. By 3.a) and T-Let
f type(C, f )
(a) Γ ; b ` y.f = z : τ
33.
By 2.c-d) and 32., L(z) = null∨typeof (H 0 , L(z)) <:
(b) Γ, x : τ ; b ` t : σ
f type(C, f )
5. By 4.a) and T-Assign
34. By 1.a), 2.c-d), 33., and def. 2, ` H 0 : ?
(a) Γ ; b ` y : D
35. 8., 25., and 34. conclude this case.
(b) Γ ; b ` z : E
(c) E <: f type(D, f )
(d) τ = E
6. By 4.b), 5.b), 5.d), and T-Let, Γ ; b ` let x = z in t :
Lemma 2. If ` H : ? then:
σ
If H ` F S, H ; a ` F S ok, and H, F S  H 0 , F S 0
0
then ` H 0 : ?, H 0 ` F S 0 , and H 0 ; b ` F S 0 ok.
7. By 2.c-d), 3.c), and WF-Env, H ` Γ; L
0
0
8. By 3.b), 3.d), 6., 7., and T-Frame1, H ` F : σ
Proof. By induction on the derivation of H, F S  H 0 , F S 0
9. By 5.b) and T-Var, Γ(z) = E
10. By 3.c), 9., and WF-Env, H ` Γ; L; z
- Case E-Invoke.
11. By 9., 10., and WF-Var, L(z) = null ∨ L(z) =
1. By the assumptions
o0 ∧ typeof (H, o0 ) <: E
(a) ` H : ?
12. By 1.c) and F-ok, ∀x 7→ b(o, p), y 7→ o0 ∈ L. sep(H, o, o0 )
(b)
H ` FS
13. By 11. and 12., L(z) = null ∨ ∀w 7→ b(o00 , p00 ) ∈
(c) H ; a ` F S ok
L. sep(H, L(z), o00 )
(d)
H, F S  H, F S 0
14. By 2.b) and 12., ∀w 7→ b(o00 , p00 ) ∈ L. sep(H, L(y), o00 )
(e) F S = F ◦ GS
15. By 2.c-d), 13., and 14., ∀w 7→ b(o00 , p00 ) ∈ L.
(f) F = hL, let x = y.m(z) in t, P il
sep(H 0 , L(y), o00 )
2. By 1.d-f) and E-Invoke
16. By 2.c-d) and 13., L(z) = null ∨ ∀w 7→ b(o00 , p00 ) ∈
(a) F S 0 = G0 ◦ G ◦ GS
0
00
L. sep(H , L(z), o )
(b) G0 = hL0 , t0 , P 0 ix
17. By 12., 15., and 16., ∀w 7→ b(o00 , p00 ), ŵ 7→ ô ∈
(c) G = hL, t, P il
L. sep(H 0 , o00 , ô)
(d) L0 = L0 [this 7→ L(y), x 7→ L(z)]
18. By 1.c) and F-ok, a = ocap =⇒ ∀x 7→ o ∈
(e) H(L(y)) = hC, F M i
L. ocap(typeof (H, o))
0
(f) mbody(C,
19. By 2.c-d) and 18., a = ocap =⇒ ∀x 7→ o ∈
( m) = x → t
L. ocap(typeof (H 0 , o))
{p} if L(z) = b(o, p)
(g) P 0 =
20. By 1.c) and F-ok, a = ocap =⇒ ∀x 7→ o ∈ L, y 7→
∅
otherwise
o0 ∈ L0 . sep(H, o, o0 )
3. By 1.b), 1.e), T-FS-A, and T-FS-NA
21. By 2.b) and 20., a = ocap =⇒ ∀ŵ 7→ ô ∈
(a) H ` F : σ
L0 . sep(H, o, ô)
(b) l =  =⇒ H ` GS ∧ l = y =⇒ H `σy GS
22. By 11. and 20., a = ocap =⇒ L(z) = null ∨
4. By 1.f), 3.a), and T-Frame1
∀ŵ 7→ ô ∈ L0 . sep(H, o0 , ô)
(a) Γ ; b ` let x = y.m(z) in t : σ
23. By 2.b-d), 21., and 22.
(b) H ` Γ; L
(a) a = ocap =⇒ ∀ŵ 7→ ô ∈ L0 . sep(H 0 , o, ô)
(c) l 6=  =⇒ σ <: C 0
(b) a = ocap =⇒ L(z) = null ∨ ∀ŵ 7→ ô ∈
(d) ` Γ; L; P
L0 . sep(H 0 , o0 , ô)
5. By 4.a) and T-Let
24. By 2.b-d), 20., and 23., a = ocap =⇒ ∀x 7→ o ∈
(a) Γ ; b ` y.m(z) : τ
L, y 7→ o0 ∈ L0 . sep(H 0 , o, o0 )
(b) Γ, x : τ ; b ` t : σ

(d) boxSeparation(H, F, GS)
6. By 4.b-c), 5.b), and T-Frame2, H `τx hL, t, P il : σ
τ
l
(e) uniqueOpenBox(H, F, GS)
7. By 3.b), 6., T-FS-A2, and T-FS-NA2, H `x hL, t, P i ◦
GS
(f) openBoxP ropagation(H, F, GS)
8. By 5.a) and T-Invoke
29. By 28.d) and def. boxSeparation,
boxSeparation(H, G, GS)
(a) Γ ; b ` y : D
0
30.
By 2.a-e), 2.g), and 29., boxSeparation(H, G0 , G ◦
(b) mtype(D, m) = τ → τ
0
GS)
(c) Γ ; b ` z : σ
31. By 28.e) and 2.d), uniqueOpenBox(H, G0 , G ◦ GS)
(d) τ 0 = E =⇒ σ 0 = E 0 for some E 0 <: E
0
0
0
32. By 2.d) and 28.f), openBoxP ropagation(H, G0 , G ◦
(e) τ = Box[E] =⇒ σ = Q . Box[E ] ∧ Perm[Q] ∈
0
GS)
Γ for some Q, E <: E
33. By 1.c) and FS-ok, H ; a ` G ◦ GS ok
9. By 8.a) and T-Var, Γ(y) = D
34. By 2.d), 2.g), and 28.a), H ; a ` G0 ok
10. By 2.e), 4.b), 9., WF-Env, and WF-Var, C <: D
0
11. By 8.b), 10., WF-Class, and WF-Override, mtype(C, m) = 35. By 30., 31., 32., 33., 34., and FS-ok, H ; a ` F S ok
0
36. 1.a), 27., and 35. conclude this case.
mtype(D, m)= τ → τ
0
Case E-Return1.

this
:
C,
x
:
E
if
τ
=
E

0
12. Define Γ := this : C, x : Q . Box[E], Perm[Q] otherwise , 1. By the assumptions


(a) ` H : ?
Q fresh
(b)
H ` FS
13. By 2.f), 11., 12., WF-Method1, and WF-Method2,
0
0
0
(c)
H ; a ` F S ok
Γ ; a `t :τ
0
(d)
H, F S  H, F S 0
14. By 8.c) and T-Var, Γ(z) = σ
(e) F S = F ◦ F 0 ◦ GS
15. By 4.b), 14., and WF-Env, H ` Γ; L; z
(f) F = hL, x, P iy
16. By 8.d-e), 14., 15., and WF-Var, L(z) = null ∨
(g) F 0 = hL0 , t0 , P 0 il
(τ 0 = E ∧ Γ(z) = E 0 ∧ L(z) = o ∧ typeof (H, o) <:
2. By 1.d-g) and E-Return1
E 0 for some E 0 <: E) ∨
(a) F S 0 = G0 ◦ GS
(τ 0 = Box[E] ∧ Γ(z) = Q . Box[E 0 ] ∧ Perm[Q] ∈
Γ ∧ L(z) = b(o, p) ∧ typeof (H, o) <: E 0 for some
(b) G0 = hL0 [y 7→ L(x)], t0 , P 0 il
E 0 <: E)
3. By 1.b), 1.e-f), and T-FS-A
17. By 2.d), 12., 16., and <:-Trans, L0 (x) = null ∨
(a) H ` F : σ
(τ 0 = E ∧ Γ0 (x) = E ∧ L0 (x) = o ∧ typeof (H, o) <:
(b) H `σy F 0 ◦ GS
E) ∨
4. By 1.f), 3.a), and T-Frame1
(τ 0 = Box[E]∧Γ0 (x) = Q.Box[E]∧Perm[Q] ∈ Γ0 ∧
(a) Γ ; b ` x : σ
L0 (x) = b(o, p) ∧ typeof (H, o) <: E)
(b)
H ` Γ; L
18. By 17. and WF-Var, H ` Γ0 ; L0 ; x
(c) σ <: C
19. By 4.b), 9., and WF-Env, H ` Γ; L; y
(d) ` Γ; L; P
20. By 9., 19., and WF-Var, L(y) = null ∨ Γ(y) =
5. By 4.a), 4.c), and T-Var, Γ(x) = σ <: C
0
0
D ∧ L(y) = o ∧ typeof (H, o ) <: D
6. By 4.b), 5., and WF-Env, H ` Γ; L; x
21. By 2.e), 20., and <:-Refl, L(y) = null ∨ Γ(y) =
7. By 1.g), 3.b), T-FS-A2, and T-FS-NA2
D ∧ L(y) = o0 ∧ typeof (H, o0 ) <: C
(a) H `σy F 0 : τ
22. By 2.d), 12., and 21., L0 (this) = null∨Γ0 (this) =
(b) l =  =⇒ H ` GS ∧ l = z =⇒ H `τz GS
C ∧ L0 (this) = o0 ∧ typeof (H, o0 ) <: C
8. By 1.g), 7.a), and T-Frame2
23. By 22. and WF-Var, H ` Γ0 ; L0 ; this
(a) Γ0 , y : σ; b0 ` t0 : τ
0
0
24. By 2.d) and 12., dom(Γ ) ⊆ dom(L )
(b) H ` Γ0 ; L0
25. By 18., 23., 24., and WF-Env, H ` Γ0 ; L0
(c) l 6=  =⇒ τ <: D
26. By 4.d), 8.b), 13., 25., WF-Method1, WF-Method2,
0 0
0 x
(d)
` Γ0 ; L0 ; P 0
and T-Frame1, H ` hL , t , P i : τ
9. By 6., 8.b), and WF-Env, H ` (Γ0 , y : σ); L0 [y 7→
27. By 7., 26., and T-FS-A, H ` F S 0
L(x)]
28. By 1.c) and FS-ok
10.
By 2.b), 8.a), 8.c), 8.d), 9., and T-Frame1, H ` G0 : τ
(a) H ; a ` F ok
11. By 7.b), 10., T-FS-A, and T-FS-NA, H ` F S 0
(b) H ; c(` GS ok
12. By 1.c), 1.e-f), and FS-ok
ocap if c = ocap ∨ label(F ) = 
(c) a =
(a) H ; a ` F ok

otherwise
(b) H ; c ` F 0 ◦ GS ok

(
ocap if c = ocap
(c) a =

otherwise
(d) boxSeparation(H, F, F 0 ◦ GS)
(e) uniqueOpenBox(H, F, F 0 ◦ GS)
(f) openBoxP ropagation(H, F, F 0 ◦ GS)
13. By 12.b) and FS-ok
(a) H ; c ` F 0 ok
(b) H ; (
d ` GS ok
ocap if d = ocap ∨ l = 
(c) c =

otherwise
(d) boxSeparation(H, F 0 , GS)
(e) uniqueOpenBox(H, F 0 , GS)
(f) openBoxP ropagation(H, F 0 , GS)
14. By 13.a) and F-ok, L(x) = null =⇒ H ; c `
G0 ok
15. By 5., 6., and WF-Var, L(x) = null ∨ L(x) =
o ∧ typeof (H, o) <: C
16. By 13.a) and F-ok, ∀z 7→ b(o0 , p0 ) ∈ L0 .
¬openbox(H, o0 , F 0 , GS)
17. By 12.f) and 16., ∀z 7→ b(o0 , p0 ) ∈ L0 .
¬openbox(H, o0 , F, F 0 ◦ GS)
18. By 17. and def. openbox, L(x) = o =⇒ ∀z 7→
b(o0 , p0 ) ∈ L0 . sep(H, L(x), o0 )
19. By 12.a), 12.c), and F-ok, c = ocap =⇒ L(x) =
o =⇒ ocap(typeof (H, L(x)))
20. By 1.g), 2.b), 13.a), and F-ok, f ieldU niqueness(H, G0 )
21. By 2.b), 13.a), 14., 15., 18., 19., 20., and F-ok, H ; c `
G0 ok
22. By 13.d), 15., and 18., boxSeparation(H, G0 , GS)
23. By 13.e), 15., and 18., uniqueOpenBox(H, G0 , GS)
24. By 13.f), 15., and 18., openBoxP ropagation(H, G0 , GS)
25. By 13.b), 13.c), 21., 22., 23., 24., and FS-ok, H ; c `
F S 0 ok
26. 1.a), 11., and 25. conclude this case.
- Case E-Open.
1. By the assumptions
(a) ` H : ?
(b) H ` F S
(c) H ; a ` F S ok
(d) H, F S  H, F S 0
(e) F S = F ◦ GS
(f) F = hL, let x = y.open {z ⇒ t0 } in t, P il
2. By 1.d-f) and E-Open
(a) F S 0 = G0 ◦ G ◦ GS
(b) G0 = hL0 , t0 , ∅i
(c) G = hL[x 7→ L(y)], t, P il
(d) L(y) = b(o, p)
(e) p ∈ P
(f) L0 = [z 7→ o]
3. By 1.b), 1.e-f), T-FS-A, and T-FS-NA

(a) H ` F : σ
(b) l =  =⇒ H ` GS ∧ l = w =⇒ H `σw GS
4. By 1.f), 3.a), and T-Frame1
(a) Γ ; b ` let x = y.open {z ⇒ t0 } in t : σ
(b) l 6=  =⇒ σ <: C
(c) H ` Γ; L
(d) ` Γ; L; P
5. By 4.a) and T-Let
(a) Γ ; b ` y.open {z ⇒ t0 } : τ
(b) Γ, x : τ ; b ` t : σ
6. By 5.a) and T-Open
(a) Γ ; b ` y : Q . Box[D]
(b) Perm[Q] ∈ Γ
(c) z : D ; ocap ` t0 : τ 0
(d) τ = Q . Box[D]
7. By 6.a) and T-Var, Γ(y) = Q . Box[D]
8. By 4.c), 7., and WF-Env, H ` Γ; L; y
9. By 2.d), 7., 8., and WF-Var, typeof (H, o) <: D
10. By 9. and WF-Var, H ` (z : D); [z 7→ o]; z
11. By 10. and WF-Env, H ` (z : D); [z 7→ o]
12. By 6.c), 11., and T-Frame1, H ` G0 : τ 0
13. By 2.d), 6.d), 9., and WF-Var, H ` Γ, x : τ ; L[x 7→
L(y)]; x
14. By 4.c), 13., and WF-Env, H ` Γ, x : τ ; L[x 7→ L(y)]
15. By 4.b), 4.d), 5.b), 14., and T-Frame1, H ` G : σ
16. By 3.b), 15., T-FS-A, and T-FS-NA, H ` G ◦ GS
17. By 12., 16., and T-FS-NA, H ` F S 0
18. By 1.c) and FS-ok
(a) H ; a ` F ok
(b) H ; c(` GS ok
ocap if c = ocap ∨ l = 
(c) a =

otherwise
(d) boxSeparation(H, F, GS)
(e) uniqueOpenBox(H, F, GS)
(f) openBoxP ropagation(H, F, GS)
19. By 18.a) and F-ok
(a) boxSep(H, F )
(b) boxObjSep(H, F )
(c) boxOcap(H, F )
(d) a = ocap =⇒ globalOcapSep(H, F )
(e) f ieldU niqueness(H, F )
20. By 2.d-e) and 19.c), ocap(typeof (H, o))
21. By 2.b) and 2.f)
(a) boxSep(H, G0 )
(b) boxObjSep(H, G0 )
(c) boxOcap(H, G0 )
(d) f ieldU niqueness(H, G0 )
22. By 1.f), 2.b,d,f), 19.b), and 20., c = ocap =⇒
globalOcapSep(H, G0 )
23. By 21.a-d), 22., and F-ok, H ; c ` G0 ok

24. By 1.f), 2.c), 18.a), and F-ok, H ; a ` G ok
25. By 1.f), 2.c), 18., 24., and FS-ok, H ; a ` G ◦ GS ok
26. By 2.a-b), 23., 25., and FS-ok, H ; c ` F S 0 ok
27. 1.a), 17., and 26. conclude this case.
- Case E-Box.
1. By the assumptions
(a) ` H : ?
(b) H ` F S
(c) H ; a ` F S ok
(d) H, F S  H 0 , F S 0
(e) F S = F ◦ GS
(f) F = hL, box[C] {x ⇒ t}, P il
2. By 1.d-f) and E-Box
(a) F S 0 = G ◦ 
(b) G = hL[x 7→ b(o, p)], t, P ∪ {p}i
(c) o ∈
/ dom(H)
(d) f ields(C) = f
(e) p fresh
(f) H 0 = H[o 7→ hC, f 7→ nulli]
3. By 1.b), 1.e-f), T-FS-A, and T-FS-NA
(a) H ` F : σ
(b) l =  =⇒ H ` GS ∧ l = w =⇒ H `σw GS
4. By 1.f), 3.a), and T-Frame1
(a) Γ ; b ` box[C] {x ⇒ t} : σ
(b) l 6=  =⇒ σ <: C
(c) H ` Γ; L
(d) ` Γ; L; P
5. By 4.a) and T-Box
(a) ocap(C)
(b) Γ, x : Q . Box[C], Perm[Q] ; b ` t : τ , Q fresh
(c) σ = ⊥
6. By 2.c), 2.f), 4.c), and WF-Env, H 0 ` Γ; L
7. By 2.f) and <:-Refl, typeof (H 0 , o) <: C
8. Define
(a) Γ0 := Γ, x : Q . Box[C], Perm[Q]
(b) L0 := L[x 7→ b(o, p)]
9. By 7., 8.a-b), and WF-Var, H 0 ` Γ0 ; L0 ; x
10. By 6., 8.a-b), 9., and WF-Env, H 0 ` Γ0 ; L0
11. By 2.b), 4.d), 5.b), 8.a-b), 10., with γ 0 = γ[Q 7→ p],
and T-Frame1, H 0 ` G : τ
12. By 11., T-EmpFS, and T-FS-NA, H 0 ` F S 0
13. By 1.c) and FS-ok
(a) H ; a ` F ok
(b) H ; c(` GS ok
ocap if c = ocap ∨ l = 
(c) a =

otherwise
(d) boxSeparation(H, F, GS)
(e) uniqueOpenBox(H, F, GS)
(f) openBoxP ropagation(H, F, GS)
14. By 2.f) and 5.a), ocap(typeof (H 0 , o))

15. By 1.f), 2.b,c,f), 13.a), 14., and F-ok, H 0 ; a ` G ok
16. By 15. and SingFS-ok, H 0 ; a ` F S 0 ok
17. By 1.a), 2.d,f), and def. well-typed heap, ` H 0 : ?
18. 12., 16., and 17. conclude this case.
- Case E-Capture.
1. By the assumptions
(a) ` H : ?
(b) H ` F S
(c) H ; a ` F S ok
(d) H, F S  H 0 , F S 0
(e) F S = F ◦ GS
(f) F = hL, capture(x.f, y) {z ⇒ t}, P il
2. By 1.d-f) and E-Capture
(a) F S 0 = F 0 ◦ 
(b) F 0 = hL[z 7→ L(x)], t, P \ {p0 }i
(c) L(x) = b(o, p)
(d) L(y) = b(o0 , p0 )
(e) {p, p0 } ⊆ P
(f) H(o) = hC, F M i
(g) H 0 = H[o 7→ hC, F M [f 7→ o0 ]i]
3. By 1.b), 1.e-f), T-FS-A, and T-FS-NA
(a) H ` F : σ
(b) l =  =⇒ H ` GS ∧ l = w =⇒ H `σw GS
4. By 1.f), 3.a), and T-Frame1
(a) Γ ; b ` capture(x.f, y) {z ⇒ t} : σ
(b) l 6=  =⇒ σ <: C
(c) H ` Γ; L
(d) ` Γ; L; P
5. By 4.a) and T-Capture
(a) Γ ; b ` x : Q . Box[C]
(b) Γ ; b ` y : Q0 . Box[D0 ]
(c) {Perm[Q], Perm[Q0 ]} ⊆ Γ
(d) D0 <: f type(C, f )
(e) Γ \ {Perm[Q0 ]}, z : Q . Box[C] ; b ` t : τ
(f) σ = ⊥
6. By 5.a-b) and T-Var
(a) Γ(x) = Q . Box[C]
(b) Γ(y) = Q0 . Box[D0 ]
7. By 2.c), 2.f-g), 6.a), WF-Var, and WF-Env, H 0 ` Γ; L
8. Define
(a) Γ0 := Γ \ {Perm[Q0 ]}, z : Q . Box[C]
(b) L0 := L[z 7→ L(x)]
9. By 2.c), 2.g), 8.a-b), <:-Refl, and WF-Var, H 0 `
Γ0 ; L0 ; z
10. By 7., 9., and WF-Env, H 0 ` Γ0 ; L0
11. By 2.b), 4.d), 5.e), 8.a), 10., and T-Frame1, H 0 ` F 0 :
τ
12. By 2.a), 11., T-EmpFS, and T-FS-NA, H 0 ` F S 0
13. By 1.c) and FS-ok
(a) H ; a ` F ok

(b) H ; c(` GS ok
ocap if c = ocap ∨ l = 
(c) a =

otherwise
(d) boxSeparation(H, F, GS)
(e) uniqueOpenBox(H, F, GS)
(f) openBoxP ropagation(H, F, GS)
14. By 13.a) and F-ok
(a) boxSep(H, F )
(b) boxObjSep(H, F )
(c) boxOcap(H, F )
(d) a = ocap =⇒ globalOcapSep(H, F )
(e) f ieldU niqueness(H, F )
15. By 2.c-g), 8.b), and 14.a), boxSep(H, F 0 )
16. By 2.c-g), 8.b), and 14.b), boxObjSep(H 0 , F 0 )
17. By 2.c-d) and 14.c)
(a) ∀o1 ∈ dom(H).
reach(H, o, o1 ) =⇒ ocap(typeof (H, o1 ))
(b) ∀o2 ∈ dom(H).
reach(H, o0 , o2 ) =⇒ ocap(typeof (H, o2 ))
18. By 2.g) and 17.a-b), ∀o1 ∈ dom(H 0 ).
reach(H 0 , o, o1 ) =⇒ ocap(typeof (H 0 , o1 ))
19. By 2.c,e,g), 8.b), 14.c), and 18., boxOcap(H 0 , F 0 )
20. By 2.c-g), 8.b), 14.b,d), a = ocap =⇒ ∀x1 7→
o1 ∈ L0 , x2 7→ o2 ∈ L0 . ocap(typeof (H 0 , o1 )) ∧
sep(H 0 , o1 , o2 )
21. By 1.f), 2.b-g), and 14.e), f ieldU niqueness(H 0 , F 0 )
22. By 2.b), 8.b), 15., 16., 19., 20., 21., and F-ok, H 0 ; a `
F 0 ok
23. By 2.a), 22., and SingFS-ok, H 0 ; a ` F S 0 ok
24. By 2.d), 4.c), 6.b), and WF-Env, H ` Γ; L; y
25. By 2.d), 6.b), 24., and WF-Var, typeof (H, o0 ) <: D0
26. By 5.d), 25., and <:-Trans, typeof (H, o0 ) <: f type(C, f )
27. By 2.g) and 26., typeof (H 0 , o0 ) <: f type(C, f )
28. By 1.a), 2.f-g), 27., and def. well-typed heap, ` H 0 : ?
29. 12., 23., 28., and 29. conclude this case.
- Case E-Swap.
1. By the assumptions
(a) ` H : ?
(b) H ` F S
(c) H ; a ` F S ok
(d) H, F S  H 0 , F S 0
(e) F S = F ◦ GS
(f) F = hL, swap(x.f, y) {z ⇒ t}, P il
2. By 1.d-f) and E-Swap
(a) F S 0 = F 0 ◦ 
(b) F 0 = hL[z 7→ b(o00 , p00 )], t, P ∪ {p00 } \ {p0 }i
(c) L(x) = b(o, p)
(d) L(y) = b(o0 , p0 )
(e) {p, p0 } ⊆ P
(f) H(o) = hC, F M i

(g) H 0 = H[o 7→ hC, F M [f 7→ o0 ]i]
(h) p00 fresh
3. By 1.b), 1.e-f), T-FS-A, and T-FS-NA
(a) H ` F : σ
(b) l =  =⇒ H ` GS ∧ l = w =⇒ H `σw GS
4. By 1.f), 3.a), and T-Frame1
(a) Γ ; b ` swap(x.f, y) {z ⇒ t} : σ
(b) l 6=  =⇒ σ <: C
(c) H ` Γ; L
(d) ` Γ; L; P
5. By 4.a) and T-Swap
(a) Γ ; b ` x : Q . Box[C]
(b) Γ ; b ` y : Q0 . Box[D0 ]
(c) {Perm[Q], Perm[Q0 ]} ⊆ Γ
(d) Box[D] = f type(C, f )
(e) Γ\{Perm[Q0 ]}, z : R.Box[D], Perm[R] ; b ` t : τ
(f) σ = ⊥
(g) D0 <: D
(h) R fresh
6. By 5.a-b) and T-Var
(a) Γ(x) = Q . Box[C]
(b) Γ(y) = Q0 . Box[D0 ]
7. By 2.c), 2.f-g), 6.a), WF-Var, and WF-Env, H 0 ` Γ; L
8. Define
(a) Γ0 := Γ \ {Perm[Q0 ]}, z : R . Box[D], Perm[R]
(b) L0 := L[z 7→ b(o00 , p00 )]
9. By 2.c), 2.g), 8.a-b), <:-Refl, and WF-Var, H 0 `
Γ0 ; L0 ; z
10. By 7., 9., and WF-Env, H 0 ` Γ0 ; L0
11. By 2.b), 4.d), 5.e), 8.a), 10., and T-Frame1, H 0 ` F 0 :
τ
12. By 2.a), 11., T-EmpFS, and T-FS-NA, H 0 ` F S 0
13. By 1.c) and FS-ok
(a) H ; a ` F ok
(b) H ; c(` GS ok
ocap if c = ocap ∨ l = 
(c) a =

otherwise
(d) boxSeparation(H, F, GS)
(e) uniqueOpenBox(H, F, GS)
(f) openBoxP ropagation(H, F, GS)
14. By 13.a) and F-ok
(a) boxSep(H, F )
(b) boxObjSep(H, F )
(c) boxOcap(H, F )
(d) a = ocap =⇒ globalOcapSep(H, F )
(e) f ieldU niqueness(H, F )
15. (Removed.)
16. By 2.c), 2.e-f), 2.i), 5.d), 14.e), and def. f ieldU niqueness,
domedge(H, o, f, o, o00 )
17. By 1.f), 2.c-e), 14.a), and def. boxSep, sep(H, o, o0 )

18. By 2.b-h), 16., 17., and def. boxSep, boxSep(H 0 , F 0 )
3. By 1.c) and FS-ok, H ; a ` F ok
0
0
19. By 2.c-g), 8.b), and 14.b), boxObjSep(H , F )
4. By 1.a), 1.e), 2.a), 3., and Lemma 1
20. By 2.c-d) and 14.c)
(a) ` H 0 : ?
(a) ∀o1 ∈ dom(H).
(b) H 0 ` F 0 : σ
reach(H, o, o1 ) =⇒ ocap(typeof (H, o1 ))
(c) H 0 ; a ` F 0 ok
(b) ∀o2 ∈ dom(H).
(d) ` Γ; L; P
reach(H, o0 , o2 ) =⇒ ocap(typeof (H, o2 ))
5. By 3. and F-ok
21. By 2.g) and 17.a-b), ∀o1 ∈ dom(H 0 ).
(a) boxSep(H, F )
reach(H 0 , o, o1 ) =⇒ ocap(typeof (H 0 , o1 ))
(b) boxObjSep(H, F )
22. By 2.c,e,g), 8.b), 14.c), and 18., boxOcap(H 0 , F 0 )
(c) boxOcap(H, F )
23. By 2.c-g), 8.b), 14.b,d), a = ocap =⇒ ∀x1 7→
(d) a = ocap =⇒ globalOcapSep(H, F )
o1 ∈ L0 , x2 7→ o2 ∈ L0 . ocap(typeof (H 0 , o1 )) ∧
(e) f ieldU niqueness(H, F )
sep(H 0 , o1 , o2 )
6.
By 1.f), 2.a), and T-Frame1
24. By 2.f-g) and 17., ∀ô ∈ dom(H 0 ). reach(H 0 , o0 , ô) =⇒
(a) Γ ; b ` let x = y.f = z in t : σ
domedge(H 0 , o, f, o, ô)
(b) l 6=  =⇒ σ <: Ĉ
25. By 1.f), 2.c-e), 14.e), and def. f ieldU niqueness
(c) H ` Γ; L
(a) ∀o1 , o2 ∈ dom(H).
7. By 6.a) and T-Let
reach(H, o, o1 )∧H(o1 ) = hC1 , F M1 i∧f type(C1 , f1 ) =
(a) Γ ; b ` y.f = z : τ
Box[D1 ] ∧ reach(H, F M1 (f1 ), o2 ) =⇒
(b)
Γ, x : τ ; b ` t : σ
domedge(H, o1 , f1 , o, o2 )
8.
By
7.a) and T-Assign
(b) ∀o1 , o2 ∈ dom(H).
0
(a)
Γ
; b`y:D
reach(H, o , o1 )∧H(o1 ) = hC1 , F M1 i∧f type(C1 , f1 ) =
(b)
f
type(D,
f) = E
Box[D1 ] ∧ reach(H, F M1 (f1 ), o2 ) =⇒
0
(c) Γ ; b ` z : E 0
domedge(H, o1 , f1 , o , o2 )
(d) E 0 <: E
26. By 2.b-i), 24., 25.a-b), and def. f ieldU niqueness,
0
0
f ieldU niqueness(H , F )
(e) τ = E
27. By 2.b), 8.b), 18., 19., 22., 23., 26., and F-ok, H 0 ; a `
9. By 8.c) and T-Var, Γ(z) = E 0
F 0 ok
10. By 6.c), 9., and WF-Env, H ` Γ; L; z
28. By 2.a), 27., and SingFS-ok, H 0 ; a ` F S 0 ok
11. By 9., 10., and WF-Var, L(z) = null ∨ L(z) ∈
29. By 2.d), 4.c), 6.b), and WF-Env, H ` Γ; L; y
dom(H) ∧ typeof (H, L(z)) <: E 0
0
0
30. By 2.d), 6.b), 29., and WF-Var, typeof (H, o ) <: D
12. By 1.h), 5.b), 11., and def. 15
31. By 5.g), 30., and <:-Trans, typeof (H, o0 ) <: D
(a) ∀x̂ 7→ b(ô, p̂) ∈ L. sep(H, ô, o)
0 0
32. By 2.g) and 31., typeof (H , o ) <: D
(b) ∀x̂ 7→ b(ô, p̂) ∈ L. L(z) = null∨sep(H, ô, L(z))
33. By 1.a), 2.f-g), 32., and def. 11, ` H 0 : ?
13. Case: openbox(H, ô, F, F S) for some ô ∈ dom(H).
Then by Lemma 3, a = ocap.
34. 12., 28., and 33. conclude this case.
14. By 5.d) and 13., globalOcapSep(H, F )
- Case E-Frame. We only consider the case where H, F −→
H 0 , F 0 by E-Assign; the other cases follow analogously.
15. By 4.c), 13., and F-ok
1. By the assumptions
(a) boxSep(H 0 , F 0 )
(a) ` H : ?
(b) boxObjSep(H 0 , F 0 )
(b) H ` F ◦ F S
(c) boxOcap(H 0 , F 0 )
(c) H ; a ` F ◦ F S ok
(d) globalOcapSep(H 0 , F 0 )
(d) H, F ◦ F S  H 0 , F 0 ◦ F S
(e) f ieldU niqueness(H 0 , F 0 )
0
0
(e) H, F −→ H , F
16. By 1.c) and FS-ok
(f) F = hL, let x = y.f = z in t, P il
(a) H ; a ` F ok
(g) F 0 = hL, let x = z in t, P il
(b) H ; c(` F S ok
(h) L(y) = o
ocap if c = ocap ∨ l = 
(c) a =
(i) H(o) = hC, F M i

otherwise
(j) H 0 = H[o 7→ hC, F M [f 7→ L(z)]i]
(d) boxSep(H, F, F S)
2. By 1.b), T-FS-A, and T-FS-NA
(e) uniqueOpenBox(H, F, F S)
(a) H ` F : σ
(f) openBoxP ropagation(H, F, F S)
(b) l =  =⇒ H ` F S ∧ l = w =⇒ H `σw F S

17. We show H 0 ; c ` F S ok by induction on the size
of F S. Let F S = G ◦ . By 16.b) and SingFS-ok,
H ; c ` G ok
18. By 17. and F-ok
(a) boxSep(H, G)
(b) boxObjSep(H, G)
(c) boxOcap(H, G)
(d) c = ocap =⇒ globalOcapSep(H, G)
(e) f ieldU niqueness(H, G)
19. By 1.j), 13., and 16.e), boxSep(H 0 , G)
20. Assume l 6= . Then by 13., 16.f), and def. 10,
openbox(H, ô, G, ). Contradiction. Therefore, l = .
21. By 1.j), 20., , and E-Open, G = hLG , tG , PG im =⇒
∀x̂ 7→ ô ∈ LG . sep(H 0 , o, ô) ∧ (L(z) = null ∨
sep(H 0 , L(z), ô))
22. By 1.j), 18.b), and 21., boxObjSep(H 0 , G)
23. By 1.j), 13., 18.c), 20., , and E-Open, boxOcap(H 0 , G)
24. By 1.j), 13., 18.d), 20., , and E-Open, c = ocap =⇒
globalOcapSep(H 0 , G)
25. By 1.j), 15.e), 18.e), and def. 13,
f ieldU niqueness(H 0 , G)
26. By 19., 22., 23., 24., 25., and F-ok, H 0 ; c ` G ok
27. By 26. and SingFS-ok, H 0 ; c ` F S ok
28. Let F S = G ◦ GS
29. If l =  then H 0 ; c ` G ok as before.
30. Let l = v 6= 
31. By 13., 16.f), 30., and def. 10, openbox(H, ô, G, GS)
32. By 1.j), 13., and 16.e), boxSep(H 0 , G)
33. By 1.j), 5.b), 18.b), 31., and def. 15, boxObjSep(H 0 , G)
34. By 1.j), 5.b), 13., 18.c), and 31., boxOcap(H 0 , G)
35. By 1.j), 14., and 18.d),
c = ocap =⇒ globalOcapSep(H 0 , G)
36. By 1.j), 15.e), and 18.e), f ieldU niqueness(H 0 , G)
37. By 32., 33., 34., 35., 36., and F-ok, H 0 ; c ` G ok
38. By 29. and 37., H 0 ; c ` G ok
39. By 16.b) and FS-ok
(a) H ; c ` G ok
(b) H ; (
d ` GS ok
ocap if d = ocap ∨ label(G) = 
(c) c =

otherwise
(d) boxSep(H, G, GS)
(e) uniqueOpenBox(H, G, GS)
(f) openBoxP ropagation(H, G, GS)
40. By 1.h-g), 13., 16.e), 31., and 33., boxSep(H 0 , G, GS)
41. By 1.h-g), 13., 16.e), 31., and 39.e),
uniqueOpenBox(H 0 , G, GS)
42. By 1.h-g), 5.b), 13., 31., and 39.f),
openBoxP ropagation(H 0 , G, GS)
43. By 38., 39.c), 40., 41., 42., and the IH, H 0 ; c `
F S ok

44. The case ¬∃ô ∈ dom(H). openbox(H, ô, F, F S)
follows analogously to 13.-43.
45. By 1.f-j), 5.b), and 16.d), boxSep(H 0 , F 0 , F S)
46. By 1.f-j), 5.b), and 16.e), uniqueOpenBox(H 0 , F 0 , F S)
47. By 1.f-j), 5.b), and 16.e-f),
openBoxP ropagation(H 0 , F 0 , F S)
48. By 4.c), 16.c), 43., 44., 45., 46., 47., and FS-ok,
H 0 ; a ` F 0 ◦ F S ok
49. By 1.i-j), 2.b), WF-Env, and WF-Var, l =  =⇒
H 0 ` F S ∧ l = w =⇒ H 0 `σw F S
50. By 4.b), 49., T-FS-A, and T-FS-NA, H 0 ` F 0 ◦ F S
51. 4.a), 48., and 50. conclude this case.

Lemma 3. If ` H : ? then:
If (H ` F ◦ F S ∨ H `σx F ◦ F S) and H ; a ` F ◦ F S ok
then openbox(H, ô, F, F S) =⇒ a = ocap
Proof. By induction on the size of F S.
1. Let F S = G ◦ . By the assumptions
(a) ` H : ?
(b) H ` F ◦ F S
(c) H ; a ` F ◦ F S ok
(d) openbox(H, ô, F, F S)
2. By 1.c) and FS-ok
(a) H ; a ` F ok
(b) H ; b(` G ◦  ok
ocap if b = ocap ∨ label(F ) = 
(c) a =

otherwise
(d) uniqueOpenBox(H, F, F S)
(e) openBoxP ropagation(H, F, F S)
3. Assume label(F ) 6= . Then by 1.d) and 2.e),
openbox(H, ô, G, ). Contradiction. Therefore, label(F ) =
 and by 2.c), a = ocap.
4. Let F S = G ◦ GS. By the assumptions
(a) ` H : ?
(b) H ` F ◦ F S
(c) H ; a ` F ◦ F S ok
(d) openbox(H, ô, F, F S)
5. By 4.c) and FS-ok
(a) H ; a ` F ok
(b) H ; b(` G ◦ GS ok
ocap if b = ocap ∨ label(F ) = 
(c) a =

otherwise
(d) uniqueOpenBox(H, F, F S)
(e) openBoxP ropagation(H, F, F S)
6. Assume label(F ) = x 6= . Then by 4.d) and 5.e),
openbox(H, ô, G, GS).
7. By 4.b), 6., and T-FS-A
(a) H ` F x : σ

(b) H `σx G ◦ GS
8. By 4.a), 7.b), 5.b), 6., and the IH, b = ocap
9. By 5.c) and 8., a = ocap

A.3

Proof of Theorem 4

Lemma 4. If C 0 <: C and f ∈ f ields(C), then
1. f ∈ f ields(C 0 )
2. f type(C, f ) = f type(C 0 , f )
Proof. Directly by <:-Ext and WF-Class.
Theorem (Progress). If ` H : ? then:
If H ` F S and H ; a ` F S ok then either H, F S 
H 0 , F S 0 or F S = hL, x, P il ◦  or F S = F ◦ GS where
• F = hL, let x = t in t0 , P il , t ∈ {y.f, y.f =

z, y.m(z), y.open {z ⇒ t00 }}, and L(y) = null; or
• F = hL, capture(x.f, y) {z ⇒ t}, P il where L(x) =
null ∧ L(y) = null; or
• F = hL, swap(x.f, y) {z ⇒ t}, P il where L(x) =
null ∧ L(y) = null.
Proof. - By H; a ` F S ok, F S = F ◦ F S 0 .
- Define hL, t, P il := F .
- By induction on the structure of t,
- Case t = x
1. Assume F S 0 = F 0 ◦ F S 00 ; otherwise the theorem
conclusion applies.
2. By the assumptions, H ` F S.
3. By 2., T-FS-NA and T-FS-A,
(a) Γ ; a ` x : σ
(b) H ` Γ; L
4. By 3., WF-Env, dom(Γ) ⊆ dom(L).
5. By T-Var, Γ(x) = σ ∧ x ∈ dom(Γ).
6. By 4. and 5., x ∈ dom(L).
7. Define
0
(a) hL0 , t0 , P 0(
il := F 0
L0 [y 7→ L(x)] if l = y
(b) L00 :=
, which is
L0
otherwise
well-defined by 6.
0
(c) F 00 := hL00 , t0 , P 0 il
8. By E-Return1, E-Return2, H, F −→ H, F 0
9. By 8., H, F ◦ F 0 ◦ F S 00  H, F 00 ◦ F S 00
10. 9. concludes this case.
- Case t = let x = null in t0
1. By E-Null, H, F −→ H, hL[x 7→ null], t, P il
2. By 1., E-Frame H, F ◦F S 0  H, hL[x 7→ null], t, P il ◦
F S0
3. 2. concludes this case.
- Case t = let x = new C in t0
1. Define
(a) o fresh
(b) f := f ields(C)
(c) H 0 := H[o 7→ hC, f 7→ nulli]
(d) L0 := L[x 7→ o]
(e) F 0 := hL0 , t0 , P il

2. By E-New, H, F −→ H 0 , F 0
3. By 1., E-Frame H, F ◦ F S 0  H 0 , F 0 ◦ F S 0
4. 3. concludes this case.
- Case t = box[C]{x ⇒ t0 }
1. Define
(a) o fresh
(b) f := f ields(C)
(c) H 0 := H[o 7→ hC, f 7→ nulli]
(d) p fresh
(e) L0 := L[x 7→ b(o, p)]
(f) P 0 := P ∪ {p}
(g) F 0 := hL0 , t0 , P 0 i
2. By E-Box, H, F ◦ F S 0  H 0 , F 0 ◦ 
3. 2. concludes this case.
- Case t = let x = y in t0
1. By the assumption
(a) ` H : ?
(b) H ` F ◦ F S 0
2. By 1.b), T-FS-NA and T-FS-A, H ` F : σ
3. By 2., T-Frame1,
(a) Γ ; a ` let x = y in t0 : σ
(b) H ` Γ ; L
4. By 3.b), WF-Env, dom(Γ) ⊆ dom(L)
5. By 4.a), T-Var, T-Let, y ∈ dom(Γ)
6. By 4, 5, y ∈ dom(L), and L(y) is defined.
7. Define L0 := L[x 7→ L(y)]
8. By E-Var, 7., H, F −→ H, hL0 , t0 , P il
9. By 8., E-Frame, H, F ◦ F S 0  H, F 0 ◦ F S 0
10. 9. concludes this case.
- Case t = let x = y.f in t0
1. By the assumption
(a) ` H : ?
(b) H ` F ◦ F S 0
2. By 1.b), T-FS-NA and T-FS-A, H ` F : σ
3. By 2., T-Frame1,
(a) Γ ; a ` let x = y.f in t0 : σ
(b) H ` Γ; L
4. By 3.a), T-Let, T-Select, T-Var,
(a) Γ(y) = C
(b) f type(C, f ) = D
5. By 3.b), WF-Env,
(a) dom(Γ) ⊆ dom(L)
(b) ∀x ∈ dom(Γ), H ` Γ; L; x
6. By 4.a)., 5.a), y ∈ dom(L)
7. By 5.b), WF-Var, 4.a), and assuming L(y) = null
(otherwise the theorem conclusion holds),
(a) L(y) = o
(b) typeof (H, o) <: C
8. By 4.b), f ∈ f ields(C)
9. By 7.b), o ∈ dom(H).

Define hC 0 , F M i := H(o) (which is defined by 9.)
By 1.a), 10, and Definition 2, dom(F M ) = f ields(C 0 )
By 10, typeof (H, o) = C 0
By 7.b), 11., 8., and Lemma 4, f ∈ dom(F M ).
Define
(a) L0 := L[x 7→ F M (f )] (defined by 13.)
(b) F 0 := hL0 , t0 , P il
15. By 14.a-b), E-Select, H, F −→ H, F 0
16. By 15, E-Frame, H, F ◦ F S 0  H, F 0 ◦ F S
17. 16. concludes the proof.

10.
11.
12.
13.
14.

- Case t = capture(x.f, y){z ⇒ t0 }
1. By assumption
(a) ` H : ?
(b) H ` F ◦ F S 0
(c) H ; a ` F S ok
2. By 1.b), T-FS-NA, and T-FS-A,
(a) Γ ; a ` capture(x.f, y){z ⇒ t0 : σ
(b) H ` Γ; L
(c) H ` Γ; L; P
3. By 2.c), ∀x ∈ dom(Γ), L(x) = b(o, p) ∧ Perm[Q] ∈
Γ =⇒ p = γ(Q) ∈ P
4. By 2.a), T-capture,
(a) Γ ; a ` x : Q . Box[C]
(b) Γ ; a ` y : Q0 . Box[D]
(c) {Perm[Q], Perm[Q]0 } ⊆ Γ
(d) D <: f type(C, f )
5. By 2.b),
(a) dom(Γ) ⊆ dom(L)
(b) ∀x ∈ dom(Γ), H ` Γ; L; x
6. By 5.b), 4.a-b), assuming L(x) 6= null ∧ L(y) 6=
null (otherwise the theorem conclusion holds),
(a) L(x) = b(o, p)
(b) typeof (H, o) ≤ C
(c) L(y) = b(o0 , p0 )
(d) typeof (H, o0 ) ≤ D
7. By 4.a), 4.b), 4.c), 7.a), 7.c), 3,
(a) p ∈ P
(b) p0 ∈ P
8. Define hC 0 , F M i := H(o)
9. Define
(a) L0 := L[z 7→ L(x)]
(b) H 0 := H[o 7→ hC 0 , F M [f 7→ o0 ]i]
(c) P 0 := P \ {p0 }
(d) F 0 := hL0 , t0 , P 0 i
10. By E-Capture, H, F ◦ F S 0  H 0 , F 0 ◦ 
11. 10. concludes this case
- Cases t = swap(x.f, y){z ⇒ t0 },
let x = y.f = z in t0 ,
let x = y.m(z) in t0 are left out and are proven analogously to the capture and select cases.

B.

Formulation of key definitions and
theorems in Coq

Static and dynamic operational semantics of CLC1 were
mechanized in the Coq theorem proving system. The Coq
mechanization closely follows the definitions in this paper
and is inspired by [43].
Partial functions
An important difference is the use of explicit partial functions over finite domains defined as follows in Coq:
1
2
3
4
5
6
7
8
9
10
11
12
13
14

Module Partial (T: InfiniteTypeWithDecidableEquality)
(B: Typ).
Definition B := BT.t.
Notation A := T.t.
Record PartFunc : Type :=
mkPartFunc {
func: A -> option B;
domain: list A;
fDomainCompat :
forall valT: A,
~ In valT domain <-> func valT = None
}.
...

Partial functions are defined in a module, which is instanciated with different domain and range types for the heap,
environment, typing context and field map:
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36

Inductive FM_Range_type :=
| FM_null : FM_Range_type
| FM_ref : Ref_type -> FM_Range_type.
Module FM_typeM <: Typ .
Definition t := FM_Range_type.
End FM_typeM.
Module p_FM := Partial FieldNameM FM_typeM.
Definition FM_type := p_FM.PartFunc.
Inductive RTObject :=
| obj : ClassName_type -> FM_type -> RTObject.
Module RTObject_typeM <: Typ .
Definition t := RTObject.
End RTObject_typeM.
Module p_heap := Partial RefM RTObject_typeM.
Definition Heap_type := p_heap.PartFunc.
Inductive env_Range_type :=
| envNull : env_Range_type
| envRef : Ref_type -> env_Range_type
| envBox : Ref_type -> env_Range_type.
Module env_Range_typeM <: Typ.
Definition t := env_Range_type.
End env_Range_typeM.
Module p_env := Partial VarNameM env_Range_typeM.
Definition Env_type := p_env.PartFunc.

37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52

Inductive typecheck_type :=
| typt_class : ClassName_type -> typecheck_type
| typt_box : ClassName_type -> typecheck_type
| typt_all : typecheck_type.
Inductive effect :=
| eff_ocap : effect
| eff_epsilon : effect.
Module tyM <: Typ.
Definition t := typecheck_type.
End tyM.
Module p_gamma := Partial VarNameM tyM.
Notation Gamma_type := p_gamma.PartFunc.

Mutual recursion
Several definitions in this paper utilize mutual recursion,
which is not well supported in Coq.
Mutual recursion in syntax of CLC1
The syntax of CLC1 has mutual recursion between terms
t = let x = e in t and expressions e = x.open{ y => t }.
We solved this problem by defining a combined inductive
type ExprOrTerm and defining predicates isExpr, isTerm
for use when an expression or term is expected:
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35

Inductive ExprOrTerm :=
| Null : ExprOrTerm
| Var : VarName_type -> ExprOrTerm
| FieldSelection : VarName_type -> FieldName_type
-> ExprOrTerm
| FieldAssignment : VarName_type -> FieldName_type
-> VarName_type -> ExprOrTerm
| MethodInvocation : VarName_type -> MethodName_type
-> VarName_type -> ExprOrTerm
| New : ClassName_type -> ExprOrTerm
| Box : ClassName_type -> ExprOrTerm
| Open : VarName_type -> VarName_type -> ExprOrTerm
-> ExprOrTerm
| TLet : VarName_type -> ExprOrTerm -> ExprOrTerm
-> ExprOrTerm.
Fixpoint isTerm (e: ExprOrTerm) : Prop :=
match e with
| Var _ => True
| TLet _ e t => (fix isExpr (e: ExprOrTerm) : Prop :=
match e with
| TLet _ _ _ => False
| Open _ _ t’ => isTerm t’
| _ => True
end
) e /\ isTerm t
| _ => False
end.
Definition isExpr (e: ExprOrTerm) : Prop :=
match e with
| TLet _ _ _ => False
| Open _ _ t => isTerm t
| _ => True
end.

Mutual recursion in T-FS

p_gamma.emptyPartFunc
y (typt_class C)
) eff t sigma ->
TypeChecks gamma eff (Open x y t) (typt_box C)
| T_Let : forall gamma eff e sigma x tau t,
TypeChecks gamma eff e sigma ->
TypeChecks (p_gamma.updatePartFunc gamma x sigma) eff
t tau ->
TypeChecks gamma eff (TLet x e t) tau.

The definitions and rules T-FS-NA, T-FS-NA2, T-FS-A, TFS-A2 employ mutual recursion betwen H ` F S and H `τx
F S. We defined this rule in Coq by combining the two cases
into a single case H `a F S, where a :=  | (x, τ ):
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31

Inductive WF_FS : FS_ann_type -> Heap_type ->
list (ann_frame_type) -> Type :=

Inductive Reduction_FS : cfg_type -> cfg_type -> Type:=
| E_StackFrame : forall H H’ L L’ t t’ FS a,
Reduction_SF ( # H , L , t ! ) ( # H’ , L’ , t’ ! )
->
Reduction_FS (H, ( (ann_frame (sframe L t) a) :: FS) )
(H’, (ann_frame (sframe L’ t’) a) :: FS )
| E_Return1 : forall H L x y F FS envVal,
p_env.func L x = Some envVal ->
Reduction_FS (H,
(ann_frame (sframe L (Var x)) (ann_var y)) :: F :: FS)
(H, updFrame F y envVal :: FS)
| E_Return2 : forall H F FS,
Reduction_FS (H, (ann_frame F ann_epsilon) :: FS)
(H, FS)

| T_EmpFS : forall H, WF_FS None H nil
| T_FS_NA : forall H F FS sigma,
WF_Frame H (ann_frame F ann_epsilon)
sigma ->
WF_FS None H FS ->
WF_FS None H ((ann_frame F ann_epsilon)
:: FS)
| T_FS_NA2 : forall H F FS sigma x tau,
( H , x , tau ## (ann_frame F
ann_epsilon) @@ sigma ) ->
WF_FS None H FS ->
WF_FS (Some (x, tau)) H
((ann_frame F ann_epsilon) :: FS)

| E_Open : forall H L x1 x2 y t1 t2 ann FS o,
isTerm t1 ->
isTerm t2 ->
p_env.func L x2 = Some (envBox o) ->
In o (p_heap.domain H) ->
Reduction_FS (H, (ann_frame (sframe L
( t_let x1 <- (Open x2 y t1) t_in t2 ))
ann) :: FS)
(H, (ann_frame (sframe
(p_env.emptyPartFunc +++ y --> (envBox o) )
t1)
ann_epsilon)
:: (ann_frame (sframe ( L +++ x1 --> (envBox o) ) t2)
ann) :: FS).

| T_FS_A : forall H F FS x tau ,
WF_Frame H (ann_frame F (ann_var x))
tau ->
WF_FS (Some (x, tau)) H FS ->
WF_FS None H ((ann_frame F
(ann_var x)) :: FS)
| T_FS_A2 : forall H F FS y sigma x tau,
( H, y, sigma ## (ann_frame F
(ann_var x)) @@ tau) ->
WF_FS (Some (x, tau)) H FS ->
WF_FS (Some (y, sigma)) H
((ann_frame F (ann_var x)) :: FS).

Reduction and typing
Reductions and typing rules are defined as follows:
Inductive TypeChecks : Gamma_type -> effect ->
ExprOrTerm -> typecheck_type -> Type :=
| T_Null : forall gamma eff,
TypeChecks gamma eff Null typt_all
| T_Var : forall gamma eff x sigma,
p_gamma.func gamma x = Some sigma ->
TypeChecks gamma eff (Var x) sigma
| T_Field : forall gamma eff x f C,
forall witn: fldP C f,
p_gamma.func gamma x = Some (typt_class C) ->
TypeChecks gamma eff (FieldSelection x f)
(typt_class (ftypeP C f witn))
| T_Assign : forall gamma eff x f y C D,
forall witn: fldP C f,
p_gamma.func gamma y = Some (typt_class C) ->
TypeChecks gamma eff (FieldSelection x f)
(typt_class D) ->
subtypeP (typt_class C) (typt_class D) ->
TypeChecks gamma eff (FieldAssignment x f y)
(typt_class C)
| T_New : forall gamma C eff,
TypeChecks gamma eff (New C) (typt_class C)
| T_Open : forall gamma eff x C y t sigma,
TypeChecks gamma eff (Var x) (typt_box C) ->
TypeChecks (p_gamma.updatePartFunc

Heap properites and invariants
` H : ? and H ` Γ, L were defined as follows:
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25

Definition Heap_obj_ok H C FM :=
forall f o,
forall f_witn : fldP C f,
p_FM.func FM f = Some (FM_ref o) ->
{ o_witn: In o (p_heap.domain H) &
subclassP (heap_typeof H o o_witn)
(ftypeP C f f_witn)
}.
Definition Heap_dom_ok H : Prop :=
forall o C FM,
p_heap.func H o = Some (obj C FM) ->
fieldsP C (p_FM.domain FM).
Definition Heap_ok H : Prop :=
forall o C FM,
p_heap.func H o = Some (obj C FM) ->
Heap_obj_ok H C FM.
Definition WF_Var (H: Heap_type) (Gamma: Gamma_type)
(L: Env_type) (x: VarName_type):=
(p_env.func L x = Some envNull) +
{C_o |
match C_o with
| (C, o) => {witn |
p_env.func L x = Some (envRef o) /\
p_gamma.func Gamma x = Some (typt_class C) /\
subtypeP (typt_class (heap_typeof H o witn))

26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42

(typt_class C)
}
end} +
{C_o |
match C_o with
| (C, o) => {witn |
p_env.func L x = Some (envBox o) /\
p_gamma.func Gamma x = Some (typt_box C) /\
subtypeP (typt_class (heap_typeof H o witn))
(typt_class C)
}
end}.
Definition WF_Env H Gamma L :=
gamma_env_subset Gamma L *
forall x sigma,
p_gamma.func Gamma x = Some sigma ->
WF_Var H Gamma L x.

Preservation theorems for CLC1
We defined and proved simplified versions of Theorem 1:
1
2
3
4
5
6
7
8
9
10

Theorem single_frame_WF_ENV_preservation :
forall H H’ L L’ t t’ sigma ann,
forall (heap_dom_ok: Heap_dom_okP H),
WF_Frame’ H (ann_frame (sframe L t) ann) sigma ->
Heap_okP H ->
Reduction_SF’ ( # H, L, t !) ( # H’, L’, t’ !) ->
((WF_Frame’ H’ (ann_frame (sframe L’ t’) ann) sigma) *
(Heap_okP H’) *
(Heap_dom_okP H’)
).

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20

Theorem single_frame_WF_ENV_preservation :
forall H H’ L L’ t t’ sigma ann,
forall (heap_dom_ok: Heap_dom_okP H),
WF_Frame’ H (ann_frame (sframe L t) ann) sigma ->
Heap_okP H ->
Reduction_SF’ ( # H, L, t !) ( # H’, L’, t’ !) ->
((WF_Frame’ H’ (ann_frame (sframe L’ t’) ann) sigma) *
(Heap_okP H’) *
(Heap_dom_okP H’)
).
Notation "[ H ## FS ]" := (WF_FS P None H FS) (at level 0).
Theorem multiple_frame_WF_ENV_preservation :
forall H H’ FS FS’,
Reduction_FS’ (H, FS)
(H’, FS’) ->
Heap_okP H ->
[ H ## FS ] ->
[ H’ ## FS’ ] * (Heap_okP H’).

