Tracing sharing in an imperative pure calculus
Paola Gianninia , Tim Richterb , Marco Servettoc , Elena Zuccad

arXiv:1803.05838v1 [] 15 Mar 2018

a Università

del Piemonte Orientale, Italy
Potsdam, Germany
c Victoria University of Wellington, New Zealand
d Università di Genova, Italy
b Universität

Abstract
We introduce a type and effect system, for an imperative object calculus, which
infers sharing possibly introduced by the evaluation of an expression, represented as an equivalence relation among its free variables. This direct representation of sharing effects at the syntactic level allows us to express in a natural
way, and to generalize, widely-used notions in literature, notably uniqueness
and borrowing. Moreover, the calculus is pure in the sense that reduction is defined on language terms only, since they directly encode store. The advantage
of this non-standard execution model with respect to a behaviourally equivalent
standard model using a global auxiliary structure is that reachability relations
among references are partly encoded by scoping.
Keywords: imperative calculi, sharing, type and effect systems
2010 MSC: 68N15, 68Q55

1. Introduction
In the imperative programming paradigm, sharing is the situation when a
portion of the store can be accessed through more than one reference, say x and
y, so that a change to x affects y as well. Unwanted sharing relations are common bugs: unless sharing is carefully maintained, changes through a reference
might propagate unexpectedly, objects may be observed in an inconsistent state,
and conflicting constraints on shared data may inadvertently invalidate invariants. Preventing such errors is even more important in increasingly ubiquitous
multi-core and many-core architectures.
For this reason, there is a huge amount of literature on type systems for
controlling sharing and interference, notably using type annotations to restrict
the usage of references, see Sect.7 for a survey. In particular, it is very useful
for a programmer to be able to rely on the following properties of a reference x .
Email addresses: giannini@di.unipmn.it (Paola Giannini), tim@cs.uni-potsdam.de
(Tim Richter), marco.servetto@ecs.vuw.ac.nz (Marco Servetto), elena.zucca@unige.it
(Elena Zucca)

Preprint submitted to Journal of LATEX Templates

March 16, 2018

• Capsule reference: x denotes an isolated portion of store, that is, the
subgraph reachable from x cannot be reached through other references.
This allows programmers (and static analysis) to identify state that can
be safely handled by a thread. In this paper we will use the name capsule
for this property, to avoid confusion with many variants in the literature
[1, 2, 3, 4, 5, 6].
• Lent reference [7, 8], also called borrowed [9, 10]: the subgraph reachable from x can be manipulated, but not shared, by a client. Typically,
borrowing can be employed to ensure that the capsule guarantee is not
broken.
In this paper, we propose a type and effect system which provides, in our
opinion, a very powerful, yet natural, way to express sharing. Notably, the two
above mentioned notions are smoothly included and generalized.
The distinguishing features are the following:
1. Rather than declaring type annotations, the type system infers sharing
possibly introduced by the evaluation of an expression.
2. Sharing is directly represented at the syntactic level, as an equivalence
relation among the free variables of the expression.
3. The calculus is pure in the sense that reduction is defined on language
terms only, rather than requiring an auxiliary structure.
We now describe these three features in more detail.
Given an expression e, the type system computes a sharing relation S which
is an equivalence relation on the set containing the free variables of e and an
additional, distinguished variable res denoting the result of e. That two variables, say x and y, are in the same equivalence class in S, means the evaluation
of e can possibly introduce sharing between x and y, that is, connect their
reachable object graphs, so that a modification of (a subobject of) x could affect y as well, or conversely. For instance, evaluating the expression x .f =y;z .f
introduces connections
• between x and y,
• between res (the result) and z .
The capsule notion becomes just a special case: an expression is a capsule iff its
result will be disjoint from any free variable (formally, res is a singleton in S).
For instance, the expression x .f =y;new C (new D ()).f is a capsule, whereas
the previous expression is not.1
The lent notion also becomes a special case: a variable x is used as lent
in an expression if the evaluation of the expression will neither connect x to
any other variable, nor to the result (formally, x is a singleton in S). In other
words, the evaluation of the expression does not introduce sharing between x
1 Note that our notion is related to the whole reachable object graph. For instance, a
doubly-linked list whose elements can be arbitrarily aliased can be externally unique [1] and
properly follow an owners as dominator strategy [11], but is not a capsule.

2

e
d
T
µ

::=
::=
::=
::=

x | e.f | e.f =e ′ | new C (es) | {ds e}| e.m(es)
T x =e;
C µ | int
ǫ|a

expression
declaration
declaration type
optional modifier

Figure 1: Syntax
and other variables (including res). For instance x is lent in x .f1 =x .f2 ;z .f . In
our type system, this notion is generalized from singletons to arbitrary sets of
variables: for instance, in the previous example x .f =y;z .f , the set {x , y} is an
equivalence class in S since the evaluation of the expression does not introduce
sharing between this set and other variables (including res).
Altogether, this direct representation at the syntactic level allows us to express sharing in a natural way. Moreover, execution is modeled by a pure calculus, where store is encoded directly in language terms, rather than by an
auxiliary structure. Formally, this is achieved by the block construct, introducing local variable declarations, which play the role of store when evaluated. This
operational semantics2 will be informally introduced in Sect.2, and formalized
in Sect.5.
A preliminary presentation of the approach presented in this paper has been
given in [12, 13].
The rest of the paper is organized as follows: in Sect.2 we provide syntax
and an informal execution model, in Sect.3 the type system, and in Sect.4 some
examples. The operational semantics of the calculus is presented in Sect.5, and
the main results and proofs in Sect.6. In Sect.7 we discuss related work, and
in Sect.8 we draw some conclusion and highlight future work. Appendix A
contains a (rather complex) type derivation. The proofs omitted from the main
paper are in Appendix B.
2. Language
The syntax of the language is given in Fig.1. We assume sets of variables
x , y, z , class names C , D , field names f , and method names m. We adopt
the convention that a metavariable which ends in s is implicitly defined as a
(possibly empty) sequence, for example, ds is defined by ds ::= ǫ | d ds, where
ǫ denotes the empty sequence.
The calculus is designed with an object-oriented flavour, inspired by Featherweight Java [14]. This is only a presentation choice: all the ideas and results
of the paper could be easily rephrased in a different imperative calculus, e.g.,
supporting data type constructors and reference types. For the same reason, we
2 Which is, of course, expected to be behaviorally equivalent to the conventional semantics
where store is a global flat auxiliary structure, as we plan to formally state and prove in
further work.

3

D z=new D(0); C x=new C(z,z);

C y=x;

D w = new D ( y . f1 . f +1); x . f2 = w ; x −→

D z=new D(0); C x=new C(z,z);

D w = new D ( x.f1 . f +1); x . f2 = w ; x −→

D z=new D(0); C x=new C(z,z);

D w = new D ( z.f +1); x . f2 = w ; x −→

D z=new D(0); C x=new C(z,z);

D w = new D ( 0+1 ); x . f2 = w ; x −→

D z=new D(0); C x=new C(z,z); D w=new D(1);
D z=new D(0); C x=new C(z,w); D w=new D(1);

x.f2=w ; x −→
x

Figure 2: Example of reduction
omit features such as inheritance and late binding, which are orthogonal to our
focus.
An expression can be a variable (including the special variable this denoting
the receiver in a method body), a field access, a field assignment, a constructor
invocation, a block consisting of a sequence of declarations and a body, or a
method invocation. In a block, a declaration specifies a type, a variable and
an initialization expression. We assume that in well-formed blocks there are no
multiple declarations for the same variable, that is, ds can be seen as a map
from variables to expressions.
A declaration type is a class name with an optional modifier a, which, if
present, indicates that the variable is affine. We also include int as an example
of primitive type, but we do not formally model related operators used in the
examples, such as integer constants and sum. An affine variable can occur
at most once in its scope, and should be initialized with a capsule, that is, an
isolated portion of store. In this way, it can be used as a temporary reference, to
“move” a capsule to another location in the store, without introducing sharing.
In the examples, we generally omit the brackets of the outermost block, and
abbreviate {T x =e; e ′ } by e;e ′ when x does not occur free in e ′ .
We turn our attention to the operational semantics now. Fig.2 shows an
example of a reduction sequence in the calculus.
The main idea is to use variable declarations to directly represent the store.
That is, a declared (non affine) variable is not replaced by its value, as in
standard let, but the association is kept and used when necessary, as it happens,
with different aims and technical problems, in cyclic lambda calculi [15, 16].
In the figure, we emphasize at each step the declarations which can be seen
as the store (in grey) and the redex which is reduced (in a box).
Assuming a program (class table) where class C has two fields f1 and f2 of
type D, and class D has an integer field f, in the initial term in Fig.2 the first
two declarations can be seen as a store which associates to z an object of class D
whose field contains 0, and to x an object of class C whose two fields contains (a
reference to) the previous object. The first reduction step eliminates an alias,
by replacing occurrences of y by x. The next three reduction steps compute
x.f1.f+1, by performing two field accesses and one sum. The last step performs
a field assignment, modifying the current store. Finally, in the last line we have
a term which can no longer be reduced, consisting of a store and the expression

4

x which denotes a reference in the store, taken as entry point. In other words,
the final result of the evaluation is an object of class C whose fields contain
(references to) two objects of class D, whose fields contain 0 and 1, respectively.
As usual, references in the store can be mutually recursive3, as in the following example, where we assume a class B with a field of type B.
B x = new B ( y ); B y = new B ( x ); y

Again, this is a term which can no longer be reduced, consisting of a store and
the reference y as entry point. In other words, this term can be seen as an
object of class B whose field contains (a reference to) another object of class B,
whose field contains (a reference to) the original object.
In the examples until now, store is flat, as it usually happens in models of
imperative languages. However, in our calculus, we are also able to represent a
hierarchical store, as shown in the example below, where we assume a class A
with two fields of type B and D, respectively.
D z = new D (0);
A w= {
B x = new B ( y );
B y = new B ( x );
A u = new A (x , z );
u };
w

Here, the store associates to w a block introducing local declarations, that
is, in turn a store. The advantage of this representation is that it models in a
simple and natural way constraints about sharing among objects, notably:
• the fact that an object is not referenced from outside some enclosing object
is directly modeled by the block construct: for instance, the object denoted
by y can only be reached through w
• conversely, the fact that an object does not refer to the outside is modeled
by the fact that the corresponding block is closed (that is, has no free
variables): for instance, the object denoted by w is not closed, since it
refers to the external object z.
In other words, our calculus smoothly integrates memory representation with
shadowing and α-conversion. However, there is a problem which needs to be
handled to keep this representation correct: reading (or, symmetrically, updating) a field could cause scope extrusion. For instance, the term
C y = { D z = new D (0); C x = new C (z , z ); x };

y . f1

under a naive reduction strategy would reduce to the ill-formed term
C y = { D z = new D (0); C x = new C (z , z ); x };

z

3 However, mutual recursion is not allowed between declarations which are not evaluated,
e.g., B x= new B(y.f); B y= new B(x.f); y is ill-formed.

5

To avoid this problem, the above reduction step is forbidden. However, reduction is not stuck, since we can transform the above term into an equivalent term
where the inner block has been flattened, and get the following correct reduction
sequence:
C
D
D
D
D

y=
z=
z=
z=
z=

{ D z = new
new D (0);
new D (0);
new D (0);
new D (0);

D (0); C x = new C (z , z ); x } y . f1 ∼
=
C x = new C (z , z ); C y = x ; y . f1 −→
C x = new C (z , z ); x . f1 −→
C x = new C (z , z ); z ∼
=
z

Formally, in addition to the reduction relation which models actual computation,
our operational semantics is defined by a congruence relation ∼
= , which captures
structural equivalence, as in π-calculus [17]. Note also that in the final term the
declaration of x can be removed (again by congruence), since it is useless.
Moving declarations from a block to the directly enclosing block is not always
safe. For instance, in the following variant of the previous example
C a y = { D z = new D (0); C x = new C (z , z ); x }; y . f1

the affine variable is required to be initialized with a capsule, and this is the case
indeed, since the right-hand side of the declaration is a closed block. However,
by flattening the term:
D z = new D (0); C x = new C (z , z ); C a y = x ; y . f1

this property would be lost, and we would get an ill-typed term. Indeed, these
two terms are not considered equivalent in our operational model. Technically,
this is obtained by detecting, during typechecking, which local variables will be
connected to the result of the block, as z in the example, and preventing to
move such declarations from a block which is the initialization expression of an
affine variable.
In this case, reduction proceeds by replacing the (unique) occurrence of the
affine variable by its initialization expression, as shown below.
C a y = { D z = new D (0); C x = new C (z , z ); x } y . f1 −→
{ D z = new D (0); C x = new C (z , z ); x }. f1 ∼
=
D z = new D (0); C x = new C (z , z ); x . f1 −→
D z = new D (0); C x = new C (z , z ); z ∼
=
D z = new D (0); z

3. Type system
In this section we introduce the type and effect system for the language. We
use X , Y to range over sets of variables.
A sharing relation S on a set of variables X is an equivalence relation on
X, called the domain of S and dubbed dom(S). As usual [x]S denotes the
equivalence class of x in S. We will call the elements hx , yi of a sharing relation
connections, and say that x and y are connected. The intuitive meaning is that,
if x and y are connected, then their reachable graphs in the store are possibly
6

shared (that is, not disjoint), hence a modification of the reachable graph of x
could affect y as well, or conversely.
The typing judgment has shape
Γ ⊢ e : T |S

e′

where Γ is a type environment, that is, an assignment of types to variables,
written x1 :T1 , . . . , x1 :Tn , S is a sharing relation, and e ′ is an annotated expression. The domain of S consists of the variables in Γ, except those affine or
of primitive type, plus a distinguished variable res for “result”. The intuitive
meaning is that S represents the connections among the free variables of e possibly introduced by the evaluation of the expression, and the variables in [res]S
are the ones that will be possibly connected to the result of the expression.
We write capsule(S) if [res]S = {res}. If Γ ⊢ e : T | S
e ′ with capsule(S),
then the expression e denotes a capsule, that is, reduces to an isolated portion
of store. An affine variable will never be connected to another, nor to res, since
it is initialized with a capsule and used only once. Analogously, a variable of a
primitive type will never be connected to another.
Moreover, during typechecking expressions are annotated. The syntax of
annotated expressions is given by:
e

X

::= x | e.f | e.m(e1 , . . . , en ) | e.f =e ′ | new C (es) | { ds e}

where we use the same metavariable of source expressions for simplicity. As we
can see, the only difference is that blocks are annotated by a set X of variables.
In an annotated block obtained as output of typechecking, X will be the local
variables declared in the block (possibly) connected with the result of the body,
see rule (t-block). Such annotations, as we will see in the next section, are used
to define the congruence relation among terms. In particular, they prevent
from moving outside of a block which initializes an affine variable declarations
of variables which will be possibly connected to the result of the block. Indeed,
moving such declarations would make the term ill-typed, as shown in the last
example of Sect.2.
The class table is abstractly modeled by the following functions:
• fields(C ) gives, for each declared class C , the sequence T1 f1 . . . Tn fn of
its fields declarations, with Ti either class name or primitive type.4
• meth(C , m) gives, for each method m declared in class C , the tuple
hT | S, µ, T1 x1 . . . Tn xn , ei consisting of its return type paired with the
resulting sharing relation, optional a modifier for this, parameters, and
body.
We assume a well-typed class table, that is, method bodies are expected to be
well-typed with respect to method types. Formally, if
meth(C , m) = hT | S, µ, T1 x1 . . . Tn xn , ei, then it should be
4 That

is, the a modifier, denoting a temporary reference, makes no sense for fields.

7

• Γ ⊢ e : T |S

e ′ , with

• Γ = this:C µ , x1 :T1 , . . . , xn :Tn .
Note that the S effects in the return type of a method can be inferred by
typechecking the body for a non-recursive method. Recursion could be handled
by a global fixed-point inference to find effects across methods. Alternatively,
and also to support interfaces, (some) effect annotations in method return types
could be supplied by the programmer, likely in a simpler form, e.g., using the
capsule modifier. In this case, typechecking the body should check conformance
to its declared interface. Still, the fixed-point inference scheme would be useful
in porting over code-bases, and might help to identify how effective the type
system is in practice. We leave this matter to further work.
The typing rules are given in Fig.3. We use the following notations:
• A sequence of subsets of X, say, X1 . . . Xn represents the smallest equivalence relation on X which contains all pairs hx , yi where both x and y
belong to one and the same Xi . So, ǫ represents the identity relation on
any set of variables.
• S1 + S2 is the smallest equivalence relation containing S1 and S2 . It is
easy to show that sum is commutative and associative.
• S\X is the sharing relation on dom(S)\X obtained by “removing” X from
S, that is, the smallest equivalence relation containing the connections
hx , yi, for all hx , yi ∈ S, such that x , y 6∈ X . S\y stands for S\{y}.
The sharing relation S has less (or equal) sharing effects than S ′ , dubbed
S ⊑ S ′ , if, for all x we have that [x ]S ⊆ [x ]S ′ .
The following proposition asserts some properties of sharing relations.
Proposition 1.
1. S1 ⊑ S2 implies that for all S we have that S + S1 ⊑
S + S2 ,
2. S1 ⊑ S2 implies that for all X we have that S1 \X ⊑ S2 \X .
3. if S\X = S, then (S + S ′ )\X = S\X + S ′ \X .
Since S + ǫ = S and ǫ ⊑ S for all S, from 1. we have that S ⊑ S + S ′ for
all S and S ′ .
In rule (t-var), the evaluation of a variable (if neither affine nor of a primitive type) connects the result of the expression with the variable itself. In rule
(t-affine-var), the evaluation of an affine variable does not introduce any connection, so the resulting sharing relation is the identity relation. Indeed, affine
variables are temporary references and will be substituted with capsules. The
same happens for variables of primitive types.
In rule (t-field-access), the connections introduced by a field access are those introduced by the evaluation of the receiver.
In rule (t-field-assign), the connections among variables introduced by a field assignment are those introduced by the evaluation of the two expressions (S1 and
S2 ). Since both S1 and S2 contain the variable res, the equivalence class of this
variable in the resulting sharing relation is, as expected, the (transitive closure)
8

(t-var)

Γ ⊢ x : C | {x , res}

(t-field-access)

(t-field-assign)

(t-new)

x

Γ ⊢ e : C |S
Γ ⊢ e.fi : Ti | S
Γ ⊢ e1 : C | S1

Γ(x ) = C

(t-affine-var)

Γ ⊢ x : C |ǫ

Γ(x ) = T
a
x T = C | int

e′

fields(C ) = T1 f1 . . . Tn fn
e ′ .fi i ∈ 1..n

e1′

Γ ⊢ e2 : Ti | S2

e2′

e1′ .fi =e2′

Γ ⊢ e1 .fi =e2 : Ci | S1 + S2

fields(C ) = T1 f1 . . . Tn fn
i ∈ 1..n

ei′
1≤i≤n
fields(C )=T1 f1 . . . Tn fn
n
P
′)
Si
new C (e1′ , . . . , en
Γ ⊢ new C (e1 , . . . , en ) : C |
Γ ⊢ ei : Ti | Si

i=1

Γ[Γ′ ]
(t-block)

⊢ ei : Ti | Si
Γ[Γ′ ] ⊢ e : T | S ′

ei′ 1≤i≤n

e′

Γ ⊢ {T1 x1 =e1 ; . . . Tn xn =en ; e} : T | S\dom(Γ′ )
′
′ ; e ′}
{[res]S ∩dom(Γ ) T1 x1 =e1′ ; . . . Tn xn =en

Γ′ = x1 :T1 , . . . , xn :Tn
∀ 1≤i≤n Ti =Cia =⇒
capsule(Si ) ∧ xi affine
Si′ = (Si + {xi , res})\res
n
P
Si′ + S ′
S=
i=1

| S ′ , µ, T1

(t-invk)

Γ ⊢ e0 : C | S0
Γ ⊢ ei : Ti | Si

e0′
ei′

0≤i≤n

Γ ⊢ e0 .m(e1 , . . . , en ) : T | S
′)
e0′ .m(e1′ , . . . , en

meth(C , m)=hT
x1 . . . Tn xn , ei
µ = a =⇒ capsule(S0 )
∀ 1≤i≤n Ti =Cia =⇒ capsule(Si ) ∧ xi affine
S0′ = (S0 + {this, res})\res
Si′ = (Si + {xi , res})\res 1 ≤ i ≤ n
n
P
S=(
Si′ + S ′ )\{this, x1 , . . . , xn }
i=0

Figure 3: Typing rules
of the union of the two equivalence classes. For instance, given the assignment
e.f =e ′ , if the evaluation of e connects y with z and x with its result, and the
evaluation of e ′ connects y ′ with z ′ and x ′ with its result, then the evaluation
of the field assignment connects y with z , y ′ with z ′ , and both x and x ′ with
the result.
In rule (t-new), the connections among variables introduced by a constructor
invocation are those introduced by the evaluation of the arguments. As for field
assignment, the equivalence class of res in the resulting sharing relation is, as
expected, the (transitive closure) of the union of the equivalence classes of the
res in the sharing relations of the arguments of the constructor.
In rule (t-block), the initialization expressions and the body of the block are typechecked in the current type environment, enriched by the association to local
variables of their declaration types. We denote by Γ[Γ′ ] the type environment
which to a variable x assigns Γ′ (x ) if this is defined, and Γ(x ) otherwise. If a
local variable is affine, then its initialization expression is required to denote
a capsule, i.e., its result must not be connected with any variable. Moreover,
the variable can occur at most once in its scope, as abbreviated by the side
condition “xi affine”.5 The connections among variables introduced by a block
5 In

our case the affinity requirement can be simply expressed as syntactic well-formedness

9

are obtained modifying those introduced by the evaluation of the initialization
expressions (Si , 1≤i≤n) plus those introduced by the evaluation of the body S ′ .
More precisely:
• For each declared variable, the result of its initialization expression is
connected the variable itself ({xi , res}).
• No sharing should be introduced among the results of the evaluation of the
initialization expressions, and the result of the block. Formally, we remove
from the corresponding sharing relations the variable res (Si \res).
• Finally, we remove from the resulting sharing relation the local variables.
The block is annotated with the subset of local variables which are in the sharing
relation S with the result of the block.
In rule (t-invk), the typing of e0 .m(e1 , . . . , en ) is similar to the typing of the
block {T0 this=e0 ; T1 x1 =e1 ; . . . Tn xn =en ; e}. However, while in a block local
variable declarations can refer to each other, the receiver e0 and the arguments
ei (1≤i≤n) do not refer to this and the formal parameters, hence the sharing
effects among them are only those caused by the method body e. (We assume
that local variables xi (1≤i≤n) and this are not in the domain of Γ.) For
instance, assume that method m has parameters x and y, and the evaluation
of its body possibly connects x with this, and y with the result, i.e., the
sharing relation associated to the method is S ′ = {x , this}{y, res}. Then, the
evaluation of the method call z .m(x ′ , y ′ ), possibly connects x ′ with z , and y ′
with the result of the expression, i.e., has sharing effects {x ′ , z }{y ′ , res}.
Finally, note that primitive types are used in the standard way. For instance, in the premise of rule (t-new) the types of constructor arguments could
be primitive types, whereas in rule (t-meth-call) the type of receiver could not.
For a sequence of declarations ds = T1 x1 =e1 ; . . . Tn xn =en ;, and a set of
ds
variables X , we write X −→ x if x is (transitively) used by X through ds. This
relation is inductively defined as follows:
ds

X −→ x if x ∈ X
ds
ds
X −→ x if x ∈ FV(ei ), for some i ∈ 1..n, and X −→ xi .
The subsequence ds |X of the declarations that are (transitively) used by X is
ds

defined by: for all i ∈ 1..n, Ti xi =ei ; ∈ ds |X if X −→ xi .
The following proposition formalizes some simple properties of the type
judgement. Notably, free variables are mentioned in sharing effects, variables
mentioned in sharing effects are in the current type environment, affine variables are always singletons in the sharing relation, and blocks are annotated
with local variables.
Proposition 2. Let Γ ⊢ e : C | S

e ′ . Then

1. if x ∈ FV(e), then hx , x i ∈ S
2. if hx , yi ∈ S, then Γ(x ) = Γ(y) = C µ , with µ = ǫ if x 6= y
condition, rather than by context rules, as in linear logic-style type systems.

10

X

3. if e = {ds eb }, then e ′ = { ds ′ eb′ } with X ⊆ dom(ds |FV(eb ) )
Proof. By induction on type derivations.
4. Examples
In this section we illustrate the expressiveness of the type system by programming examples, and we show a type derivation.
Example 3. Assume we have a class D with a field f of type D, and a class C
with two fields of type D. Consider the following closed expression e:
D y = new D ( y );
D x = new D ( x );
C a z = { D z2 = new D ( z2 ); D z1 = ( y . f = x ); new C ( z2 , z2 )};
z

The inner block (right-hand side of the declaration of z) refers to the external
variables x and y, that is, they occur free in the block. In particular, the execution of the block has the sharing effect of connecting x and y. However, these
variables will not be connected to the final result of the block, since the result
of the assignment will be only connected to a local variable which is not used
to build the final result, as more clearly shown by using the sequence abbreviation: {D z2= new D(z2); y.f= x; new C(z2,z2)}. Indeed, as will be shown in
the next section, the block reduces to {D z2= new D(z2); new C(z2,z2)} which
is a closed block. In existing type systems supporting the capsule notion this
example is either ill-typed [6], or can be typed by means of a rather tricky swap
typing rule [7, 8] which, roughly speaking, temporarily changes, in a subterm,
the set of variables which can be freely used.
Example 4. As a counterexample, consider the following ill-typed term
D y = new D ( y );
D x = new D ( x );
C a z = { D z1 = ( y . f = x ); new C ( z1 , z1 )};
z

Here the inner block is not a capsule, since the local variable z1 is initialized as
an alias of x, hence connected to both x and y. Indeed, the block reduces to
new C(x,x) which is not closed.
Type derivation for Example 3. Let Γ1 = y:D, x:D, z:Ca , and Γ2 = z2:D, z1:D. In
Fig.4 we give the type derivation that shows that expression e of Example 3 is
well-typed. To save space we omit the annotated expression produced by the
derivation, and show the annotations for the blocks at the bottom of the figure.
Consider the type derivation D2 for the expression ei which initializes z (inner block). The effect of the declaration of z2 is the sharing relation {z2, res}
and the effect of the declaration of z1 is the sharing relation {z1, x, y, res}.
Before joining these sharing relations, we remove res from their domains, since
the results of the two expressions are not connected with each other. So the
11

Γ1 [Γ2 ] ⊢ x : D | {x, res}
Γ1 [Γ2 ] ⊢ y : D | {y, res}
D1 :

Γ1 [Γ2 ] ⊢ y.f=x : D | {x, y, res}
Γ1 [Γ2 ] ⊢ new D(y.f=x) : D | {x, y, res}
Γ1 [Γ2 ] ⊢ z2 : D | {z2, res}

Γ1 [Γ2 ] ⊢ z2 : D | {z2, res}

D2 : Γ1 [Γ2 ] ⊢ new D(z2) : D | {z2, res} D1 Γ1 [Γ2 ] ⊢ new C(z2, z2) : C | {z2, res}
Γ1 ⊢ {D z2=new D(z2); D z1=new D(y.f=x); new C(z2, z2)} : C | {x, y}
Γ1 ⊢ y : D | {y, res}
D : Γ1 ⊢ new D(y) : D | {y, res}

Γ1 ⊢ x : D | {x, res}
Γ1 ⊢ new D(x) : D | {x, res}
a

D2

Γ1 ⊢ z : C | ǫ

i

⊢ {D y=new D(y); D x=new D(x); C z=e ; z} : C | ǫ

• D2 yields eia = {{z2} D z2=new D(z2); D z1=new D(y.f=x); new C(z2, z2)}
• D yields e′ ={∅ D y=new D(y); D x=new D(x); Ca z=eia ; z}

Figure 4: Type derivation for Example 3
resulting sharing relation is represented by {z1, x, y} (z2 is only connected with
itself). The effect of the evaluation of the body is the sharing relation represented by {z2, res}. Therefore, before removing the local variables z1 and z2
from the sharing relations we have the sharing relation {z1, x, y} {z2, res}. The
block is annotated with {z2} (the local variable in the equivalence class of res).
Since, after removing the local variables, [res] = {res}, ei denotes a capsule,
and may be used to initialize an affine variable.
D is the type derivation for the whole expression e. Note that, since z is an
affine variable, the sharing relation of z, which is the body of the block, is the
identity. In particular, [res] = {res}, so the annotation of the block e is ∅.
Example 5. We provide now a more realistic programming example, assuming
a syntax enriched by usual programming constructs. See the Conclusion for a
discussion on how to extend the type system to such constructs.
The class CustomerReader below models reading information about customers
out of a text file formatted as shown in the example:
Bob
1 500 2 1300
Mark
42 8 99 100

In odd lines we have customer names, in even lines we have a shop history: a
sequence of product codes. The method CustomerReader.read takes a Scanner,

12

assumed to be a class similar to the one in Java, for reading a file and extracting
different kinds of data.
class CustomerRea de r {
static Customer read ( Scanner s )/*S = ǫ*/{
Customer c = new Customer ( s . nextLine ())
while ( s . hasNextNum ()){
c . addShopHistor y ( s . nextNum ())
}
return c
}
}
class Scanner {
String nextLine ()/* S = ǫ*/{...}
boolean hasNextNum ()/* S = ǫ*/{...}
int nextNum ()/* S = ǫ*/{...}
}

Here and in the following, we insert after method headers, as comments, their
sharing effects. In a real language, a library should declare sharing effects of
methods by some concrete syntax, as part of the type information available
to clients. In this example, CustomerReader.read uses some methods of class
Scanner. Such methods have no sharing effects, as represented by the annotation
S = ǫ. Note that for the last two methods this is necessarily the case since they
have no explicit parameters and a primitive return type. For the first method,
the only possible effect could have been to mix this with the result.
A Customer object is read from the file, and then its shop history is added.
Since methods invoked on the scanner introduce no sharing, we can infer that the
same holds for method CustomerReader.read. In other words, we can statically
ensure that the data of the scanner are not mixed with the result.
The following method update illustrates how we can “open” capsules, modify
their values and then recover the original capsule guarantee. The method takes
a customer, which is required to be a capsule by the fact that the corresponding
parameter is affine, and a scanner as before.
class CustomerRea de r {...// as before
static Customer update ( Customer a old , Scanner s )/*S = ǫ*/{
Customer c = old // we open the capsule ‘old ’
while ( s . hasNextNum ()){
c . addShopHistor y ( s . nextNum ())
}
return c
}
}

A method which has no sharing effects can use the pattern illustrated above:
one (or many) affine parameters are opened (that is, assigned to local variables)
and, in the end, the result is guaranteed to be a capsule again. This mechanism
is not possible in [2, 1, 5] and relies on destructive reads in [6].
A less restrictive version of method update could take a non affine Customer old
parameter, that is, not require that the old customer is a capsule. In this case,
13

the sharing effects would be S = {res, old}. Hence, in a call Customer.update(c1,s),
the connections of c1 would be propagated to the result of the call. In other
words, the method type is “polymorphic” with respect to sharing effects. Notably, the method will return a capsule if invoked on a parameter which is a
capsule.
Example 6. The following method takes two teams t1, t2. Both teams want to
add a reserve player from their respective lists p1 and p2, assumed to be sorted
with best players first. However, to keep the game fair, the two reserve players
can only be added if they have the same skill level.
static void addPlayer ( Team t1 , Team t2 , Players p1 , Players p2 )
/*S = {t1, p1}, {t2, p2}*/{
while ( true ){// could use recursion instead
if ( p1 . isEmpty ()|| p2 . isEmpty ()) {/* error */}
if ( p1 . top (). skill == p2 . top (). skill ){
t1 . add ( p1 . top ());
t2 . add ( p2 . top ());
return ;
}
else {
removeMoreS ki l le d ( p1 , p2 );
}
}

The sharing effects express the fact that each team is only mixed with its list
of reserve players.
Example 7. Finally, we provide a more involved example which illustrates the
expressive power of our approach. Assume we have a class C as follows:
class C {
C f;
C clone ()/* S = ǫ*/{...}
C mix ( C x )/*S = {x, this, res}*/{...}
}

The method clone is expected to return a deep copy of the receiver. Indeed,
this method has no parameters, apart from the implicit non-affine6 parameter
this, and returns an object of class C which is not connected to the receiver, as
specified by the fact that the sharing relation is the identity, represented by ǫ,
where res is not connected to this. Note that a shallow clone method would
be typed C clone()/*S = {this, res}*/.
The method mix is expected to return a “mix” of the receiver with the
argument. Indeed, this method has, besides this, a parameter x of class C,
both non affine, returns an object of class C and its effects are connecting x with
this, and both with the result.
Consider now the following closed expression e:
6 We assume this to be non-affine unless explicitly indicated, e.g., by inserting a as first
element of the list of parameters.

14

e
d

::=
::=

x | v .f | v .m(vs) | v .f =v | new C (vs) | {ds e}
T x =e;

expression
declaration

T
v
dv

::=
::=
::=

Cµ
X
x | { dvs v } | new C (vs)
C x =new C (vs);

declaration type
value
evaluated declaration

Figure 5: Syntax of calculus, values, and evaluated declarations
C c1 = new C ( c1 );
C outer = {
C c2 = new C ( c2 );
C a inner = {
C c3 = new C ( c3 );
C r = c2 . mix ( c1 ). clone ()
r . mix ( c3 )};
inner . mix ( c2 )};
outer
The key line in this example is C r=c2.mix(c1).clone().
Thanks to the fact that clone returns a capsule, we know that r will not be
connected to the external variables c1 and c2, hence also the result of the block
will not be connected to c1 or c2. However, the sharing between c2 and c1
introduced by the mix call is traced, and prevents the outer block from being
a capsule. The reader can check that, by replacing the declaration of r with
C r=c2.mix(c2).clone(), also the outer block is a capsule, hence variable outer

could be declared affine. This example is particularly challenging to test the
capability of a type system to detect the capsule property. For instance, the
type system in [6] does not discriminate these two cases, those in [7, 8] require
rather tricky and non syntax-directed rules. The type derivation for Example 7
can be found in the Appendix.
5. The calculus
The calculus has a simplified syntax, defined in Fig.5, where we assume that,
except from right-hand sides of declarations and bodies of blocks, subterms of a
compound expression are only values. This simplification can be easily obtained
by a (type-driven) translation of the syntax of Fig.1 generating for each subterm
which is not a value a local declaration of the appropriate type. Moreover we
omit primitive types.
A value is the result of the reduction of an expression, and is either a variable
(a reference to an object), or a block where the declarations are evaluated (hence,
correspond to a local store) and the body is in turn a value.
A sequence dvs of evaluated declarations plays the role of the store in conventional models of imperative languages, that is, each dv can be seen as an
association of an object state new C (vs) or an evaluated block to a reference.
As anticipated in Sect.2, mutual recursion among evaluated declarations is
allowed, whereas we do not allow references to variables on the left-hand-side
15

of forward unevaluated declarations. E.g, C x= new C(y); C y= new C(x); x is
allowed, whereas C x= new C(y); C y= x.f; x is not.
That is, our calculus supports recursive object initialization, whereas, e.g., in
Java, we cannot directly create two mutually referring objects as in the allowed
example above, but we need to first initialize their fields to null. However, to
make recursive object initialization safe, we should prevent access to an object
which is not fully initialized yet, as in the non-allowed example. Here we take
a simplifying assumption, just requiring initialization expressions to be values.
More permissive assumptions can be expressed by a sophisticated type system
as in [18].
Semantics is defined by a congruence relation, which captures structural
equivalence, and a reduction relation, which models actual computation, similarly to what happens, e.g., in π-calculus [17].
Both relations are defined on terms obtained through the typechecking phase,
hence where blocks have been annotated as described in the previous section.
Formally, given an annotated term e, and denoting by e − the term obtained by
erasing annotations from e, we assume that Γ ⊢ e − : C | S
e, for some Γ, C ,
X , and S.
The congruence relation, denoted by ∼
= , is defined as the smallest congruence satisfying the axioms in Fig.6. We write FV(ds) and FV(e) for the free
variables of a sequence of declarations and of an expression, respectively, and
X [y/x ], ds[y/x ], and e[y/x ] for the capture-avoiding variable substitution on a
set of variables, a sequence of declarations, and an expression, respectively, all
defined in the standard way.
(alpha)

X [y/x ]
{X ds T x =e; ds ′ e ′ } ∼
ds[y/x ] T y=e[y/x ]; ds ′ [y/x ] e ′ [y/x ]}
={

(reorder)

(new)

X
{X ds C x =new C (xs); ds ′ e} ∼
= { C x =new C (xs); ds ds ′ e}

{x }
new C (xs) ∼
= { C x =new C (xs); x }

(garbage)

X \dom(dvs)
ds e}
{X dvs ds e} ∼
={

(block-elim)

(dec)

(FV(ds) ∪ FV(e)) ∩ dom(dvs) = ∅

{∅ e} ∼
=e

{Y ds C µ x ={X ds 1 ds 2 e}; ds ′ e ′ } ∼
=
{Y ds ds 1 C µ x ={X \dom(ds 1 ) ds 2 e}; ds ′ e ′ }

(body)

{Y ds {X ds 1 ds 2 e}} ∼
=
{Y ∪(X ∩dom(ds 1 )) ds ds 1 {X \dom(ds 1 ) ds 2 e}}

(val-ctx)

V[{X dvs 1 dvs 2 v }] ∼
=
{X ∩dom(dvs 1 ) dvs 1 V[{X \dom(dvs 1 ) dvs 2 v }]}

FV(ds 1 ) ∩ dom(ds 2 ) = ∅
FV(ds ds ′ e ′ )∩dom(ds 1 )=∅
µ = a =⇒ dom(ds 1 )∩X =∅
FV(ds 1 ) ∩ dom(ds 2 ) = ∅
FV(ds) ∩ dom(ds 1 ) = ∅
FV(dvs 1 ) ∩ dom(dvs 2 ) = ∅
FV(V) ∩ dom(dvs 1 ) = ∅

Figure 6: Congruence rules
Rule

(alpha)

is the usual α-conversion. The condition x , y 6∈ dom(ds ds ′ ) is
16

implicit by well-formedness of blocks.
Rule (reorder) states that we can move evaluated declarations in an arbitrary
order. Note that, instead, ds and ds ′ cannot be swapped, because this could
change the order of side effects.
In rule (new), a constructor invocation can be seen as an elementary block where
a new object is allocated.
Rule (garbage) states that we can remove (or, conversely, add) a useless sequence
of evaluated declarations from a block. Note that it is only possible to safely
remove/add declarations which are evaluated, since they do not have side effects.
Rule (block-elim) states that a block with no declarations is equivalent to its body.
With the remaining rules we can move a sequence of declarations from a block
to the directly enclosing block, or conversely, as it happens with rules for scope
extension in the π-calculus [17].
In rules (body) and (dec), the inner block is the body, or the right-hand side of
a declaration, respectively, of the enclosing block. The first two side conditions
ensure that moving the declarations ds 1 does cause neither scope extrusion nor
capture of free variables. More precisely: the first prevents moving outside a
declaration in ds 1 which depends on local variables of the inner block. The
second prevents capturing with ds 1 free variables of the enclosing block. Note
that the second condition can be obtained by α-conversion of the inner block,
but the first cannot. Finally, the third side condition of rule (dec) prevents,
in case the block initializes an affine variable, to move outside declarations of
variables that will be possibly connected to the result of the block. Indeed, in
this case we would get an ill-typed term. In case of a non affine declaration,
instead, this is not a problem.
Rule (val-ctx) handles the cases when the inner block is a subterm of a field
access, method invocation, field assignment or constructor invocation. Note
that in this case the inner block is necessarily a (block) value. To express all
such cases in a compact way, we define value contexts V in the following way:
V ::= [ ] | V.f | V.f =v | v .f =V | new C (vs, V, vs ′ )
For instance, if V = new C (vs, [ ], vs ′ ), we get
X ∩dom(dvs 1 )
new C (vs, {X dvs 1 dvs 2 v }, vs ′ ) ∼
dvs 1 new C (vs, {X \dom(dvs 1 ) dvs 2 v }, vs ′ )}
={

As for rules (dec) and (body), the first side condition prevents moving outside
a declaration in dvs 1 which depends on local variables of the inner block, and
the second side condition prevents capturing free variables of V.
The following definition introduces a simplified syntactical form for values
and evaluated declarations. In particular evaluated declarations correspond to
objects and values are references to objects.
Definition 8.
1. A sequence of evaluated declarations dvs is in canonical
form if, for all dv in dvs, dv = C x =new C (xs); for some C , x and xs.
X
2. A value v is in canonical form if either v = x for some x , or v = { dvs x }
for some X , dvs, and x , with dvs 6= ǫ in canonical form and dvs |x = dvs.
The following proposition shows that congruence allows us to assume that
values are in canonical form.
17

Proposition 9. If v is a value, then there exists v ′ such that v ∼
= v ′ and v ′ is
in canonical form.
Proof. By structural induction on values, and for blocks by induction on the
number of declarations that are not in canonical form. The full proof is in
Appendix B.
X

X

Values of shape { dvs x } such that FV({ dvs |x x }) = ∅ are capsules. Their
inner objects can be reached only through a reference to the block.
In the following, unless otherwise stated, we assume that values and evaluated declarations are in canonical form.
Evaluation contexts, defined as follows, express standard left-to-right evaluation.
X

X

E ::= [ ] | { dvs T x =E; ds e} | { dvs E}
X

In the evaluation context { dvs T x =E; ds e} we assume that no declaration
in ds is evaluated.
We introduce now some notations which will be used in reduction rules. We
write dvs(x ) for the declaration of x in dvs, if any (recall that in well-formed
blocks there are no multiple declarations for the same variable). We write HB(E)
for the hole binders of E, that is, the variables declared in blocks enclosing the
context hole, defined by:
• if E = {dvs T x =E ′ ; ds e}, then HB(E) = dom(dvs) ∪ {x } ∪ HB(E ′ )
• if E = {dvs E ′ }, then HB(E) = dom(dvs) ∪ HB(E ′ )
We write Ex and dec(E, x ) for the sub-context declaring x and the declaration of
x extracted from E, defined as follows:
• let E = {dvs T y=E ′ ; ds e}
- if dvs(x ) = dv and x 6∈ HB(E ′ ), then Ex = {dvs T y=[ ]; ds e} and
dec(E, x ) = dv
- else Ex = {dvs T y=Ex′ ; ds e} and dec(E, x ) = dec(E ′ , x )
• let E = {dvs E ′ }
- if dvs(x ) = dv and x 6∈ HB(E ′ ), then Ex = {dvs [ ]} and dec(E, x ) = dv
- else Ex = {dvs Ex′ }, and dec(E, x ) = dec(E ′ , x )
Note that Ex and dec(E, x ) are not defined if x is not declared in any block
enclosing the context hole, that is, if x 6∈ HB(E).
Reduction rules are given in Fig.7.
Rule (congr) states that congruence can be used to reduce a term which otherwise would be stuck, as it happens for the α-rule in lambda calculus.
In rule (field-access), given a field access of shape x .f , the first enclosing
declaration for x is found (through the auxiliary function dec). The fields of the
class C of x are retrieved from the class table. If f is actually the name of a field
of C , say, the i-th, then the field access is reduced to the reference xi stored in
this field. In the last side condition, Ex is the (necessarily defined) sub-context
containing the first enclosing declaration for x , and the condition xi 6∈ HB(E ′ )

18

(congr)

e1 −→ e2
e1′ −→ e2′

(field-access)

(invk)

e1
e2

∼
= e1′
∼
= e2′

E [x .fi ] −→ E [xi ]

dec(E , x ) = C x =new C (x1 , . . . , xn );
fields(C ) = C1 f1 . . . Cn fn ∧ 1 ≤ i ≤ n
E = Ex [E ′ ] ∧ xi 6∈ HB(E ′ )

E [v .m(v1 , .., vn )] −→
E [{C µ this=v ; T1 x1 =v1 ; ..Tn xn =vn ; e}]

(field-assign)

(alias-elim)

(affine-elim)

E [x .fi =y] −→ E x .i=y [y]

class(E, v ) = C
meth(C , m)=hD, µ, T1 x1 ..Tn xn , ei

dec(E , x ) = C x =new C (x1 , . . . , xn );
fields(C ) = C1 f1 . . . Cn fn ∧ 1 ≤ i ≤ n
E = Ex [E ′ ] ∧ y 6∈ HB(E ′ )

E [{X dvs C x =y; ds e}] −→ E [{X \{x } dvs ds[y/x ] e[y/x ]}]
E [{X dvs C a x =v ; ds e}] −→ E [{X \{x } dvs ds[v /x ] e[v /x ]}]

Figure 7: Reduction rules
ensures that there are no declarations for xi in inner blocks (otherwise xi would
be erroneously bound). This can always be obtained by rule (alpha) of Fig.6.
For instance, assuming a class table where class A has an int field, and class
B has an A field f, without this side condition, the term (without annotations):
A a = new A (0); B b = new B ( a ); { A a = new A (1); b . f }

would reduce to
A a = new A (0); B b = new B ( a ); { A a = new A (1); a }

whereas this reduction is forbidden, and by rule
reduced to

(alpha)

the term is instead

A a = new A (0); B b = new B ( a ); { A a1 = new A (1); a }

For this example: Eb = {A a = new A(0); B b = new B(a) E ′ } and E ′ =
{A a = new A(1) [ ]}.
In rule (invk), the class C of the receiver v is found through the auxiliary function
class defined by
class(E, x ) = C if dec(E, x ) = C x = ;
X
class(E, { dvs x }) = C if dvs(x ) = C x = ;
and method m of C , if any, is retrieved from the class table. The call is reduced
to a block where declarations of the appropriate type for this and the parameters are initialized with the receiver and the arguments, respectively, and the
body is the method body.
In rule (field-assign), given a field assignment of shape x .f =y, the first enclosing declaration for x is found (through the auxiliary function dec). If f is

19

actually the name of a field of C , say, the i-th, then this first enclosing declaration is updated, by replacing the i-th constructor argument by y, obtaining
C x =new C (x1 , xi−1 , y, xi+1 , . . . , xn );, as expressed by the notation E x .i=y (the
obvious formal definition of which is omitted). As for rule (field-access) we have
the side condition that y 6∈ HB(E ′ ) This side condition, requiring that there
are no inner declarations for the reference y, prevents scope extrusion, since if
y ∈ HB(E ′ ), E x .i=u would take y outside the scope of its definition. The congruence rules (dec) and (body) of Fig.6 can be used to correctly move the declaration
of y outside its declaration block, as previously described. For example, without
the side condition, the term (without annotations)
A a = new A (0); B b = new B ( a ); { A a1 = new A (1); b . f = a1 }

would reduce to
A a = new A (0); B b = new B ( a1 ); { A a1 = new A (1); a1 }

The previous term is congruent to
A a = new A (0); B b = new B ( a ); A a1 = new A (1); b . f = a1

by applying rule

(body),

and then

(block-elim).

This term reduces correctly to

A a = new A (0); B b = new B ( a1 ); A a1 = new A (1); a1

The last two rules eliminate evaluated declarations from a block.
In rule (alias-elim), a reference (non affine variable) x which is initialized as an
alias of another reference y is eliminated by replacing all its occurrences. In rule
(affine-elim), an affine variable is eliminated by replacing its unique occurrence
with the value associated to its declaration.
We conclude this section by briefly discussing how the reduction relation
should actually be computed. Indeed, the definition in Fig.7 is not fully algorithmic, since rule (congr) can always be applied in a nondeterministic way,
analogously to what happens, e.g., with α-conversion in lambda calculus or
structural rules in π-calculus. Whereas this is cleaner and simpler at the theoretical level, of course an implementation should follow a strategy. Again as
is usually done for analogous cases, congruence is expected to be applied only
when needed (since otherwise reduction would be stuck). All our congruence
rules except for (alpha) and (reorder) are meant to be applied from left to right
(as a reduction). This is witnessed by the fact that values in canonical form
do not match the left-hand side of any of the previously mentioned congruence
rules and Proposition 9 ensures that any value may be reduced in this form.
6. Results
In this section we present the main formal results on our calculus. First, we
show a canonical form theorem describing constraints on free variables of welltyped values. Then we prove subject reduction, stating that reduction preserves
the type, and may reduce the sharing effects. In addition, reduction preserves
an invariant on the store that allows us to prove that lent and capsule references
have the expected behaviour informally described in the Introduction.
20

Finally, we prove progress, i.e., that well-typed expressions do not get “stuck”.
Note that, since our operational model is a pure calculus, in the statements and
proofs we do not need invariants on auxiliary structures such as memory.
First of all we extend the typing judgment to annotated expressions, and to
(annotated) sequences of declarations, as follows:
• Given an annotated expression e, we write Γ ⊢ e : C | S if Γ ⊢ e − :
C |S
e where e − is obtained by erasing the annotations from e.
• Given ds = C1µ1 x1 =e1 ; . . . Cnµn xn =en ;, an (annotated) sequence of declarations, Γ ⊢ ds : S if
1. Γ ⊢ ei : Ci | Si , for some Si (1 ≤ i ≤ n),
n
P
(Si + {xi , res})\res, and
2. S =
i=1

3. if µi =a then capsule(Si ) (1 ≤ i ≤ n), and xi used at most once in ds.
Note that S is a sharing relation only on dom(Γ), that is, not including res,
according to the fact that a sequence of declarations has no “result”.
Canonical form theorem. In this subsection we state a theorem describing constraints on free variables of well-typed values. Notably, the free variables of a
value (in canonical form) are either affine or are connected to its result. Therefore, a capsule value can contain only affine free variables.
In the following we use the underscore for a type, when the specific type is
irrelevant. Moreover, we we will say that x is affine/non-affine in Γ if Γ(y) = C a
or Γ(y) = C , respectively.
Theorem 10. If Γ ⊢ v : | S, and y ∈ FV(v ), then:
1. if y is non-affine in Γ, then hy, resi ∈ S
2. if capsule(S), then y is affine in Γ.
Proof. 1. By cases on the shape of values. Thanks to Proposition 9 we can
assume values in canonical form.
• If v is a variable x , then the only free variable in v is x itself. The judgment
Γ ⊢ x : C | S has been necessarily derived by rule (t-var), hence the thesis
holds.
X
• If v is of shape { dvs x }, since dvs is in canonical form we have dvs =
C1 x1 =new C1 (xs 1 ); . . . Cn xn =new Cn (xs n );, hence y ∈ FV(v ) implies y ∈
xs i for some i ∈ 1..n.
dvs
Moreover, again since dvs is in canonical form, x −→ y for each y occurring
in the block. The judgment Γ ⊢ v : | S has been necessarily derived by
rule (t-block) with premises derived by (t-new) for each declaration and
(t-var) for the body (indeed x = xi for some 1≤i≤n) hence we have
Γ[Γ′ ] ⊢ new Ci (xs i ) : Ci | Si (1 ≤ i ≤ n)
Γ[Γ′ ] ⊢ x : C | {x , res}
Γ′ = x1 :C1 , . . . , xn :Cn
Si′ = (Si + {xi , res})\res
n
P
Si′ + {x , res}
S = S ′ \dom(Γ′ ), with S ′ =
i=1

21

dvs

We show that, if x −→ y, and y is not affine in Γ[Γ′ ], then hy, resi ∈ S ′ ,
dvs

by induction on the definition of x −→ y.
dvs

– x −→ x , and in this case the thesis trivially holds.
dvs
dvs
– x −→ y if y ∈ FV(new Ci (xs i )), for some i ∈ 1..n, and x −→ xi .
The judgment Γ[Γ′ ] ⊢ new Ci (xs i ) : Ci | Si has been derived by
′
(t-new) with Γ[Γ ] ⊢ y : | {y, res}, derived by rule (t-var), among
the premises, hence hy, resi ∈ Si . By transitivity we get hy, xi i ∈
(Si + {xi , res}), hence hy, xi i ∈ Si′ , and as a consequence hy, xi i ∈ S ′ .
Since by the inductive hypothesis we have hxi , resi ∈ S ′ , again by
transitivity we get hy, resi ∈ S ′ .
Now, if y is free in the block, y 6∈ dom(Γ′ ), hence we get hy, resi ∈ S as
needed.
2. If y is free in v then Γ(y) is defined, by Proposition 2.1-2. However, if we had
Γ(y) = C , then by the previous point we would have hy, resi ∈ S, contradicting
capsule(S). Hence, Γ(y) = C a .
Subject reduction. To show subject reduction, we need some preliminary lemmas.
The following lemma states that typing essentially depends only on the free
variables of the expression. We denote by Γ\x the type environment obtained
by removing the type association for x from Γ, if any.
Lemma 11. (Weakening) Let Γ ⊢ e : C | S. If x 6∈ FV(e), then
1. Γ[x :T ] ⊢ e : C | S + {x } for all T , and
2. Γ\x ⊢ e : C | S\x .
Proof. By induction on derivations.
Even though the sharing relation S does not change, its domain is extended
when adding a variable x to the context (the equivalence class of x contains
only x ), and restricted when removing a variable.
The following lemma asserts that congruent expressions have the same type
and sharing effects that coincide on the free variables of both expressions.
Lemma 12. (Congruence preserves types) Let e1 and e2 be annotated expressions such that Γ ⊢ e1 : C1 | S1 and Γ ⊢ e2 : C2 | S2 . If e1 ∼
= e2 , then C1 = C2 ,
and, for all x ∈ (FV(e1 ) ∩ FV(e2 )) ∪ {res}, [x ]S1 = [x ]S2 .
Proof. The proof is in Appendix B.
To prove subject reduction and progress we introduce the set of redexes, and
we show that expressions can be decomposed in an evaluation context filled with
a redex. Therefore an expression either is a value or it matches the left-hand
side of exactly one reduction rule.
Definition 13. Redexes, ρ, are defined by:
ρ ::= x .fi | v .m(vs) | x .f =y | {X dvs C x =y; ds e} | {X dvs C a x =v ; ds e}

22

Lemma 14. (Decomposition) If e is not a value, then there are E and ρ such
that e ∼
= E[ρ].
Proof. The proof is in Appendix B.
The type environment extracted from ds, denoted Γds , is defined by:
Γds = T1 :x1 , . . . , Tn :xn if ds = T1 x1 =e1 ; . . . Tn xn =en ;.
Given an evaluation context E, let ΓE be the type environment extracted from
E, defined by:
Γ[ ] is the empty type environment,
• Γ{dvs T x =E; ds e} = Γdvs ds [x :T ][ΓE ], and
• Γ{dvs E} = Γdvs [ΓE ].
The following lemma asserts that subexpressions of typable expressions are
themselves typable, and may be replaced with expressions that have the same
type and the same or possibly less sharing effects.
Lemma 15. (Context) Let Γ ⊢ E[e] : C | S, then
1. Γ[ΓE ] ⊢ e : D | S1 for some D and S1 ,
2. if Γ[ΓE ] ⊢ e ′ : D | S2 where S2 ⊑ S1 (S2 = S1 ), then Γ ⊢ E[e ′ ] : C | S ′ with
S ′ ⊑ S (S ′ = S).
Proof. The proof is in Appendix B.
The following lemma is used to prove that the elimination rules, namely
and (capsule-elim), do not introduce sharing. In particular, for (aliaselim) a non-affine variable x is substituted with a non-affine variable y which is
in the equivalence class of x in the sharing relation S, so that there is no newly
produced connection. For (capsule-elim), an affine variable is substituted with a
capsule value, so also in this case there is no newly produced connection.
(alias-elim)

Lemma 16. (Substitution)
1. Let Γ, x :D ⊢ e : C | S (Γ, x :D ⊢ ds : S). If Γ ⊢ y : D | {y, res} and
y ∈ [x ]S , then Γ\x ⊢ e[y/x ] : C | S\x (Γ\x ⊢ ds[y/x ] : S\x ).
2. Let Γ, x :D a ⊢ e : C | S (Γ, x :D a ⊢ ds : S). If Γ ⊢ v : D | ǫ, then Γ\x ⊢
e[v /x ] : C | S (Γ\x ⊢ ds[v /x ] : S\x ).
Proof. By induction on e.
Lemma 17. Let Γ ⊢ v : C | S where v is a canonical value. If capsule(S), then
S = ǫ.
Proof. The proof is in Appendix B.
The following lemma asserts that the sharing relation of a subexpression is
finer than the sharing relation of the expression that contains it.
Lemma 18. If Γ ⊢ E[e] : C | S and Γ ⊢ e : D | S ′ , then S ′ \X ⊑ S where
X = {res} ∪ HB(E).
23

Proof. The proof is in Appendix B.
The following lemma states a technical property needed to prove that sharing
relations are preserved when we reduce a field access redex x .f .
Lemma 19. If Γ ⊢ E[e1 ] : C | S1 , Γ ⊢ E[e2 ] : C | S2 , Γ ⊢ e1 : D | X1 and
Γ ⊢ e2 : D | X2 with
• res ∈ X1 iff res ∈ X2 , and
• (X1 ∪ X2 ) ∩ HB(E) = ∅
then S1 + Y = S2 + Y where Y = (X1 ∪ X2 ) \ {res}.
Proof. The proof is in Appendix B.
As already mentioned, in the subject reduction theorem we show that, in
addition to preserving the type of expressions, reduction also preserves the capsule and lent properties of subexpressions. To trace the expression associated to
a variable x in a store we assume that there is no shadowing and define contexts
that have a hole on the right-hand-side of the (unique) declaration of x . Given
x define Cx by:
Cx

::=

Cx .f | Cx .m(vs) | v .m(vs Cx vs ′ ) | Cx .f =v | v .f =Cx
| new C (vs Cx vs ′ ) | {dvs T x =[ ]; ds ′ v } | {dvs T y=Cx ; ds ′ v }
| {dvs Cx }

Therefore, in Cx [e] the expression e occurs as the right-hand side of the (unique)
declaration for reference x . To lighten the notation we write simply C and C[e]
when the variable is not relevant.
The type assignment extracted from a context C, denoted ΓC , is defined
as for evaluation contexts by adding the clause for all non-block expressions:
ΓC.f = . . . = Γnew C (vs C vs ′ ) = ΓC . The declaration for a variable y in a
context C, denoted dec(C, y), can be defined as for evaluation contexts.
The following lemma states that a subexpression which occurs as the righthand side of a declaration in a well-typed expression is well-typed as well, under
the type assignment extracted from the surrounding context, and its free variables are associated to evaluated declarations in the context.
Lemma 20. If ⊢ C[e], then
1. ΓC ⊢ e : C | S for some C and S, and
2. if y ∈ FV(e), then ΓC ⊢ y : D | Sy and dec(C, y) = D y=new D (y1 , . . . , yn );.
Proof. By induction on C, observing that we do not allow forward references to
unevaluated declarations, and by definition of C the declarations before a hole
are all evaluated.
With dec(C, {y1 , . . . , yn }) we denote the declarations dec(C, y1 ) · · · dec(C, yn ).
The following defines the sharing relation induced by a sequence of evaluated
declarations.
24

Definition 21. Given a sequence of variables declarations dvs
C1 x1 =new C1 (xs 1 ); · · · Cm xm =new Cm (xs m );
define Sdvs = X1 + · · · + Xm where Xi = {xi , xs i } (1 ≤ i ≤ m).
The subject reduction theorem asserts that reduction preserves the type of
the expression, and may reduce its sharing effects. Reduction preserves also
the type of any expression which occurs as the right-hand side of a declaration.
Moreover, reduction reduces sharing effects, where, however, we must take into
account that free variables, having an associated right value in the store, are
connected to the corresponding fields. (Indeed, there is no guarantee that the
sole sharing effects of the expression are reduced, since a new free variable could
be introduced in the expression as an effect of field access.) This is the invariant
on the store that allows us to prove that lent and capsule references have the
expected behaviour informally described in the Introduction.
Theorem 22. (Subject reduction) If Γ ⊢ e1 : C | S and e1 −→ e2 , then
1. Γ ⊢ e2 : C | S ′ where S ′ ⊑ S, and
2. for all x such that e1 = Cx [e], e2 = Cx′ [e ′ ], and ΓCx ⊢ e : D | Sx we
have that: ΓCx′ ⊢ e ′ : D | Sx′ and (Sx′ + Sdvs ′ ) ⊑ (Sx + Sdvs ) where dvs =
dec(C, FV(e)) and dvs ′ = dec(C ′ , FV(e ′ )).
Proof. By Lemma 14, e1 ∼
= E[ρ], and, since we may have applied rule (congr) of
Fig.7, we have that e2 ∼
= E ′ [e ′ ] where E[ρ] −→ E ′ [e ′ ] has been derived by one of
the other rules. Let Γ ⊢ E[ρ] : C | S. By case analysis on the rule of Fig.7 used
for E[ρ] −→ E ′ [e ′ ]. We show the two most interesting cases, which are (fieldaccess) and (field-assign), and just hint the one for (alias-elim) and (capsule-elim). The
proof of the remaining cases is in Appendix B.
Rule (field-access).
1. In this case
• E ′ = E = Ex [E1 ] for some E1
• dec(E, x ) = dv x = D x =new D (x1 , . . . , xn );
• ρ = x .fi and e ′ = xi with xi 6∈ HB(E1 ).
By definition of Ex , for some E2
(1) either Ex = E2 [{ds ′ eb }] with ds ′ = dvs dv x T z =E1 [x .fi ]; ds
(2) or Ex = E2 [{dvs dv x E1 }].
and x 6∈ HB(E1 ).
We consider only case (1) since the proof for the other case is similar and
simpler.
From Lemma 15.1 we have that Γ[ΓE2 ] ⊢ {ds ′ eb } : C ′ | S1 for some C ′ and
S1 . From typing rule (T-block), Γ[ΓE2 ][Γds ′ ] ⊢ E1 [x .fi ] : D ′ | S2 for some
D ′ and S2 . From Lemma 15.1 and typing rules (field-access) and (var) we
have that Γ[ΓE2 ][Γds ′ ][ΓE1 ] ⊢ x .fi : Di | {x , res} and Γ[ΓE2 ][Γds ′ ][ΓE1 ] ⊢
xi : Di | {xi , res}. (Note that neither x nor xi can be forward references
to non evaluated declarations and therefore they must be defined without the a modifier.) From Lemma 19 we have that: if Γ[ΓE2 ][Γds ′ ] ⊢
25

E1 [xi ] : D ′ | S2′ , then S2 + {x , xi } = S2′ + {x , xi }. Since Γ[ΓE2 ][Γds ′ ] ⊢ dv x :
{x , x1 , . . . , xn , res}, we have that:
Γ[ΓE2 ][Γds ′ ] ⊢ T z =E1 [x .fi ]; dv x : S3 implies Γ[ΓE2 ][Γds ′′ ] ⊢ T z =E1 [xi ]; dv x :
S3 where ds ′′ = dvs dv x T z =E1 [xi ]; ds. Therefore
Γ[ΓE2 ] ⊢ {dvs dv x T z =E1 [xi ]; ds eb } : C ′ | S1
and from Lemma 15.2 we derive Γ ⊢ E[e ′ ] : C | S.
2. Let e1 = Cy [e], e2 = Cy′ [e ′ ], and e1 = E[x .fi ] −→ e2 = E ′ [xi ]. If the redex
x .fi is not a subexpression of e then e = e ′ , and since ΓCy = ΓCy′ , the
result is obvious. If x .fi is a subexpression of e, then from Lemma 14
for some E ′′ we have that e = E ′′ [x .fi ] and e ′ = E ′′ [xi ]. From ΓCx ⊢
E ′′ [x .fi ] : D | Sx and ΓCx ⊢ E ′′ [xi ] : D | Sx′ , and Lemma 15.1 we have that
Γ[ΓCx ][ΓE ′′ ] ⊢ x .fi : Di | {x , res} and Γ[ΓCx ][ΓE ′′ ] ⊢ xi : Di | {xi , res}.
From Lemma 19 we derive that Sx + {x , xi } = Sx′ + {x , xi }. Therefore,
also Sx + {x , x1 , . . . , xn } = Sx′ + {x , x1 , . . . , xn }.
Rule

(field-assign).

1. In this case
• E = Ex [E1 ] for some E1 ,
• E ′ = Exx .i=y [E1 ] since x 6∈ HB(E1 )
• dec(E, x ) = dv x = D x =new D (x1 , . . . , xn );
• ρ = x .fi =y and e ′ = y with y 6∈ HB(E1 ).
As for the case of field update Ex has either shape (1) or (2) with y 6∈
HB(E1 ). We consider only case (1).
From Lemma 15.1 we have that Γ[ΓE2 ] ⊢ {ds ′ eb } : C ′ | S1 for some C ′
and S1 . From typing rule (T-block) we have that Γ[ΓE2 ][Γds ′ ] ⊢ E1 [x .fi =y] :
D ′ | S2 for some D ′ and S2 . From Lemma 15.1, typing rule (T-Field-assign)
and (T-var) we have that Γ[ΓE2 ][Γds ′ ][ΓE1 ] ⊢ x : D | {x , res}, Γ[ΓE2 ][Γds ′ ][ΓE1 ] ⊢
y : Di | {y, res}, and Γ[ΓE2 ][Γds ′ ][ΓE1 ] ⊢ x .fi =y : Di | {x , y, res} where
fields(D )=D1 f1 . . . Dn fn and {y, res} ⊑ {x , y, res}.
From Γ[ΓE2 ] ⊢ {ds ′ eb } : C ′ | S1 and typing rule (T-block), we have that
(a) Γ[ΓE2 ][Γds ′ ] ⊢ T z =E1 [x .fi =y]; : S3 ,
(b) Γ[ΓE2 ][Γds ′ ] ⊢ dv x : Sx where Sx = {x , x1 , . . . , xn },
(c) Γ[ΓE2 ][Γds ′ ] ⊢ dvs ds : S4 , and
(d) Γ[ΓE2 ][Γds ′ ] ⊢ eb : C ′ | S5 .
Let dv ′x = D x =new D (x1 , . . . , xi−1 , y, xi+1 , . . . , xn ); and ds ′′ = dvs dv ′x T z =E1 [y]; ds.
We have that Γds ′ = Γds ′′ . Therefore
(a1) Γ[ΓE2 ][Γds ′′ ] ⊢ T z =E1 [y]; : S3′ ,
(b1) Γ[ΓE2 ][Γds ′′ ] ⊢ dv ′x : Sx′ where Sx′ = {x , x1, . . . , xi−1 , y, xi+1 , . . . , xn },
(c1) Γ[ΓE2 ][Γds ′′ ] ⊢ dvs ds : S4 , and
(d1) Γ[ΓE2 ][Γds ′′ ] ⊢ eb : | S5 .
From typing rules (T-field-assign) and (T-var), and Lemma 19 we get S3 +
{x , y} = S3′ + {x , y}. Moreover, from (a), typing rule (T-field-assign), and
Lemma 18 we have that x and y are in the same equivalence class in S3 ,
26

i.e., [x ]S3 = [y]S3 . Therefore, S3′ + Sx′ ⊑ S3 + Sx . From (a1)-(d1), typing
rule (T-block) and Lemma 15.2 we get
Γ[ΓE2 ] ⊢ {dvs dv ′x T z =E1 [y]; ds eb } : C ′ | S1′
′
where S1 ⊑ S1 . From Lemma 15.2 we derive that Γ ⊢ E2 [{dvs dv ′x T z =E1 [y]; ds eb }] :
C | S ′ where S ′ ⊑ S. Consider Exx .i=y [E1 ] = E2 [{dvs dv ′ T z =E1 ; ds eb }],
we have that Γ ⊢ Exx .i=y [E1 [y]] : C | S ′ , which proves the result.
2. Let e1 = Cy [e], e2 = Cy′ [e ′ ], and e1 = E[x .fi =y] −→ e2 = E ′ [y]. If the
redex is not a subexpression of e then e = e ′ , and since ΓCy = ΓCy′ , the
result is obvious. If x .fi =y is a subexpression of e, then from Lemma 14
for some E ′′ we have that e = E ′′ [x .fi =y] and e ′ = E ′′ [y]. From ΓCx ⊢
E ′′ [x .fi =y] : D | Sx , ΓCx ⊢ E ′′ [y] : D | Sx′ , and Lemma 15.1 we have that
Γ[ΓCx ][ΓE ′′ ] ⊢ x .fi =y : Di | {x , y, res} and Γ[ΓCx ][ΓE ′′ ] ⊢ y : Di | {y, res}.
From {y, res} ⊑ {x , y, res}, and Lemma 15.2 we derive that Sx′ ⊑ Sx .
Moreover, since FV(e ′ ) ⊆ FV(e), we derive the result.
Rule (alias-elim). Clause 1. is proved using Lemma 16.1. Clause 2. is proved
as in the case of (field-assign).
Rule (affine-elim). Clause 1. is proved using Lemma 16.2 and 17. Clause 2.
is proved as in the case of (field-assign).
Lent and capsule properties. We can now formally express and prove that our
type and effect system ensures that lent and capsule references have the expected
behaviour, informally described in the Introduction.
Informally, a reference is lent if its reachable object graph, which is made of
the reference itself and the reachable object graphs of its fields, can be manipulated, but non shared, by a client.
Theorem 23. (Lent) If ⊢ C[e], ΓC ⊢ e : | S, y singleton in S, dec(C, y) =
C y=new C (xs);, [res]S ∩ {y, xs} = ∅, and C[e] −→⋆ C ′ [v ], then y 6∈ FV(v ).
Proof. By induction on the number n of steps of the reduction C[e] −→⋆ C ′ [v ].
For n = 0, we have ΓC ⊢ v : | S. If we had y ∈ FV(v ), then, from Lemma 20, y
would be non-affine in ΓC . Hence, from Theorem 10.1, it should be hy, resi ∈ S,
contradicting the hypothesis.
Let C[e] −→ C ′ [e ′ ] and C ′ [e ′ ] −→⋆ C ′′ [v ] in n steps. From Theorem 22.2, since
ΓC ⊢ e : | S and [res]S ∩ {y, xs} = ∅ we have that ΓC ′ ⊢ e ′ : | S ′ and
[res]S ′ ∩ {y, xs} = ∅. By induction hypothesis on ΓC ′ ⊢ e ′ : | S ′ we derive the
result.
Informally, a capsule is a reachable object graph which is an isolated portion
of store, that is, it does not contain nodes reachable from the outside. In our
calculus, a reachable object subgraph is a value v , nodes reachable from the
outside are free variables, hence the condition to be a capsule can be formally
expressed by requiring that v has no free variables. However, affine free variables
are admitted, since they are temporary references which will be replaced by
an (isolated in turn) portion of store. The following theorem states that an
expression of a capsule type reduces to an isolated portion of store.

27

Theorem 24. (Capsule) If ⊢ C[e], ΓC ⊢ e : | S with capsule(S), and C[e] −→⋆
C ′ [v ] where for all y ∈ FV(v ), dec(C ′ , y) = a y= ;.
Proof. By induction on the number n of steps of the reduction C[e] −→⋆ C ′ [v ].
For n = 0, we have ΓC ⊢ v : | S. From Theorem 10.2 and Lemma 20.2,
capsule(S) implies for all y ∈ FV(v ), dec(C ′ , y) = a y= ;.
Let C[e] −→ C ′ [e ′ ] and C ′ [e ′ ] −→⋆ C ′′ [v ] in n steps. From Theorem 22.2, since
ΓC ⊢ e : | S, and [res]S = ∅, we have ΓC ′ ⊢ e ′ : | S ′ , and [res]S ′ = ∅. By
induction hypothesis on ΓC ′ ⊢ e ′ : | S ′ we derive the result.
Progress. Closed expressions are not “stuck”, that is, they either are values or
can be reduced.
We write e −→ for e −→ e ′ for some e ′ , ⊢ e : C for ∅ ⊢ e : C | ǫ, and ⊢ e
for ⊢ e : C for some C (note that an expression with no free variables has the
identity as sharing effects).
Theorem 25. (Progress) If ⊢ e, and e is not a value, then e −→.
Proof. By Lemma 14, if e is not a value, then e ∼
= E[ρ]. By rule (congr), it is
enough to show the thesis for E[ρ]. For all ρ, except field access and field update,
we have that the corresponding reduction rule is applicable, since either there
are no side conditions (cases (alias-elim) and (affine-elim)), or the side conditions
can be easily shown to hold (case (invk)).
In the proof for field access and field update, we use the following auxiliary
notation. Given an evaluation context E, the context BE is defined by
• BE = {dvs T y=[ ]; ds e} if E = {dvs T y=E ′ ; ds e} and
• BE = {dvs [ ]} if E = {dvs E ′ }.
If ρ is x .fi , from Lemma 15.1, rule (t-field-access), and rule (T-var) of Fig.3, we
have that ΓE ⊢ x .fi : Ci | ǫ where fields(C ) = C1 f1 . . . Cn fn . So, we have that
Ex is defined, and, for some E ′ , E = Ex [E ′ ]. If xi 6∈ HB(E ′ ), then rule (Field-Access)
is applicable.
Otherwise, since xi ∈ HB(E ′ ), we have that Ex′ i is defined, and E ′ [x .fi ] =
X
E1 [BEx′ [E2 [x .fi ]]] for some E1 and E2 such that BEx′ [E2 [x .fi ]] = { dvs T xi =v ; ds e}.
i
i
Using rule (alpha) of Fig.6 we have that
X [y/xi ]
{X dvs T xi =v ; ds e} ∼
dvs[y/xi ] T y=v [y/xi ]; ds ′ [y/xi ] e[y/xi ]}
={

where y can be chosen such that y 6∈ HB(E ′′ ). Therefore Ex [E ′ [x .fi ]] ∼
= Ex [E3 [x .fi ]]
where xi 6∈ HB(E3 ). So Ex [E3 [x .fi ]] −→ e2 by applying rule (field-access).
If ρ is x .fi =y, from Lemma 15.1, rule (t-field-assign), and rule (T-var) of Fig.3,
we have that ΓE ⊢ x .fi =y : Ci | {x , y} where fields(C ) = C1 f1 . . . Cn fn . So, we
have that Ex is defined, and E = Ex [E ′ ] for some E ′ . Therefore, for some E1′ ,
E = E1′ [BEx [E ′ ]]. If y 6∈ HB(E ′ ), then rule (Field-Assign) is applicable.
Otherwise, since y ∈ HB(E ′ ), Ey′ is defined, and E ′ [x .fi =y] = E1 [BEy′ [E2 [x .fi =y]]]
Y

for some E1 and E2 such that BEy′ [E2 [x .fi =y]] = { dvs |FV(v ) T y=v ; ds e}.
By induction on the number n > 0 of blocks from which we have to extrude the
declaration of y. Let dvs 1 = T y=v ; dvs |FV(v ) . If n > 1, then for some E ′′ 6= [ ],
28

X

Y

(a) either { dvs ′ T x =v ′ ; E ′′ [{ dvs 1 ds e}]}
X

Y

(b) or { dvs ′ T x =v ′ ; T z =E ′′ [{ dvs 1 ds e}]; ds ′ e ′ },
For (a), by induction hypothesis we have that
Y′

{ dvs ′ T x =v ′ ; E ′′ [{ dvs 1 ds e}]} ∼
= { dvs ′ T x =v ′ ; {
′
′
′
for some ds , e , and Y .
X

Applying rule

Y

(Body)

X

dvs 1 ds ′ e ′ }}

of Fig.6 we have that
′

∼
{X dvs ′ T x =v ′ ; {Y dvs 1 ds ′ e ′ }} =
X′
Y ′ \dom(dvs 1 ) ′ ′
′
′
{ dvs T x =v ; dvs 1 {
ds e }}
where X ′ = X ∪ (Y ′ ∩ dom(dvs 1 )).
For (b), by induction hypothesis we have that
{X dvs ′ T x =v ′ ; T z =E ′′ [{Y dvs 1 ds e}]; ds ′ e ′ } ∼
=
X
Y′
′
′ ′
′′ ′′
′
{ dvs T x =v ; T z ={ dvs 1 ds e }; ds e }
for some ds ′ , ds ′′ , e ′ , e ′′ , and Y ′ .
If y 6∈ Y ′ , from Proposition 2.3 we have that dom(dvs |FV(val) )∩Y ′ = ∅. Applying
rule (Dec) of Fig.6 we get
′

X
Y
{ dvs ′ T x =v ′ ; T z ={ dvs 1 ds ′ e ′ }; ds ′′ e ′′ } ∼
=
X
Y′
′
′ ′
′′ ′′
′
{ dvs T x =v ; dvs 1 T z ={ ds e }; ds e }.
Y

If y ∈ Y ′ , from ⊢ e1 : C | S, Lemma 15, ΓE1 ⊢ { dvs 1 ds e} : D | S for some D ,
Z , and S such that T = D µ . From ΓE ⊢ x .fi =y : Ci | {x , y}{x , y} and y ∈ Y
we also have that x ∈ Z . Therefore µ 6= a. Applying rule (Dec) we get
′

{X dvs ′ T x =v ′ ; T z ={Y dvs 1 ds ′ e ′ }; ds ′′ e ′′ } ∼
=
X
Y ′ \dom(dvs 1 ) ′ ′
{ dvs ′ T x =v ′ ; dvs 1 T z ={
ds e }; ds ′′ e ′′ }
Therefore Ex [E ′ [x .fi =y]] ∼
= Ex [E3 [x .fi =y]] for some E3 such that y 6∈ HB(E3 ). So
Ex [E3 [x .fi =y]] −→ e2 by applying rule (field-assign).
7. Related work
Capsule and lent notions. As mentioned, the capsule property has many
variants in the literature, such as isolated [6], uniqueness [19] and external
uniqueness [1], balloon [2, 3], island [5]. The fact that aliasing can be controlled
by using lent (borrowed ) references is well-known [9, 10]. However, before the
work in [6], the capsule property was only detected in simple situations, such
as using a primitive deep clone operator, or composing subexpressions with the
same property.
The important novelty of the type system in [6] has been recovery, that
is, the ability to detect properties (e.g., capsule or immutability) by keeping
29

into account not only the expression itself but the way the surrounding context
is used. In [6] an expression which does not use external mutable references is
recognized to be a capsule. However, expressions which do use external mutable
references, but do not introduce sharing between them and the final result, are
not recognized to be capsules. For instance, Example 3 and Example 7 in Sect.4
would be ill-typed in [6]. Our type system generalizes recovery by precisely
computing sharing effects.
Capabilities. In other proposals [20, 21, 22, 23, 24] types are compositions of
one or more capabilities, and expose the union of their operations. The modes
of the capabilities in a type control how resources of that type can be aliased.
By using capabilities it is possible to obtain an expressivity which looks similar
to our type system, even though with different sharing notions and syntactic
constructs. For instance, the full encapsulation notion in [20]7 , apart from
the fact that sharing of immutable objects is not allowed, is equivalent to the
guarantee of our a modifier. Their model has a higher syntactic/logic overhead
to explicitly track regions. As for all work before [6], objects need to be born
@unique (that is, with the capsule property) and the type system permits to
manipulate data preserving their uniqueness. With recovery [6] (as with our
type and effect system), instead, we can forget about uniqueness, use normal
code designed to work on conventional shared data, and then recover the aliasing
encapsulation property.
Ownership. A closed stream of research is that on ownership (see an overview
in [25]) which, however, offers an opposite approach. The ownership invariant,
which can be expressed and proved, is, however, expected to be guaranteed
by defensive cloning. In our approach, instead, the capsule concept models an
efficient ownership transfer. In other words, when an object x is “owned” by
another object y, it remains always true that y can only be accessed through
x , whereas the capsule notion is more dynamic: a capsule can be “opened”,
that is, assigned to a standard reference and modified, and then we can recover
the original capsule guarantee. Cloning, if needed, becomes a responsibility of
the client. Other work in the literature supports ownership transfer, see for
example [26, 1]. In the literature it is however applied to uniqueness/external
uniqueness, thus not the whole reachable object graph is transferred.
Full, deep and shallow interpretation. The literature on sharing control distinguishes three interpretations for properties of objects.
• Full: the whole reachable object graph respects that property.
• Shallow: only the object itself respects that property.
• Deep: the reachable object graph is divided in 2 parts: The first part is
the one that is logically “owned” by the object itself, while the second
part is just “referenced”.
In our approach, as in [2, 8, 6, 3, 7], properties have the full interpretation, in the
7 This paper includes a very good survey of work in this area, notably explaining the
difference between external uniqueness [1] and full encapsulation.

30

sense that they are propagated to the whole reachable object graph. In a deep
interpretation, instead, as in [19, 10, 27], it is possible, for instance, to reach
a mutable object from an immutable object. In this sense, approaches based
on ownership, or where it is somehow possible to have any form of “internal
mutation” are (only) deep, as in [23, 4, 28, 29]. This also includes [1], where an
unique object can point to arbitrarily shared objects, if they do not, in turn,
point back to the unique object itself.
The advantage of the full interpretation is that libraries can declare strong
intentions in a coherent and uniform way, independently of the concrete representation of the user input (that, with the use of interfaces, could be unknown
to the library). On the other side, providing (only) full modifiers means that
we do not offer any language support for (as an example) an immutable list of
mutable objects.
Destructive reads. Uniqueness can be enforced by destructive reads, i.e., assigning a copy of the unique reference to a variable and destroying the original
reference, see [6, 19]. Traditionally, borrowing/fractional permissions [10] are related to uniqueness in the opposite way: a unique reference can be borrowed, it
is possible to track when all borrowed aliases are buried [9], and then uniqueness
can be recovered. These techniques offer a sophisticate alternative to destructive reads. We also wish to avoid destructive reads. In our work, we ensure
uniqueness by linearity, that is, by allowing at most one use of an a reference.
Alias analysis. Alias analysis is a fundamental static analysis, used in compilers
and code analysers. Algorithms such as Steensgaard’s algorithm, [30], infer
equivalence classes that may alias. In [31] is presented a refined version of
such algorithm, performing a uniqueness analysis, similar to our detection of
“capsule” values. However, the aim of our work is to design a language in which
annotations, such as the affine modifier, can be used by the user to enforce
properties of its code. Then the inference system checks that such annotations
are correctly used.
Calculus. Finally, an important distinguishing feature of our work is that sharing can be directly represented at the syntactic level as a relation among free
variables, thanks to the fact that the calculus is pure. Models of the imperative
paradigm as pure calculi have been firstly proposed in [32, 33].
8. Conclusion
We have presented a type and effect system which infers sharing possibly
introduced by the evaluation of an expression. Sharing is directly represented
at the syntactic level as a relation among free variables. This representation
allows us to express in a natural way, and to generalize, widely-used notions in
literature, providing great expressivity, as shown by the examples of Sect.4.
We adopt a non standard operational model, where store is encoded directly
in the language terms. In this model, sharing properties are directly expressed
at the syntactic level. Notably, in a subterm e of a program, objects reachable
from other parts of the program are simply those denoted by free variables in e,

31

whereas local objects are those denoted by local variables declared in e. In our
opinion, this offers a very intuitive and simple understanding of the portion of
memory only reachable from e, since it is encoded in e itself. Another advantage
is that, the store being encoded in terms, most proofs can be done by structural
induction on terms, as we have exploited in the Coq implementation mentioned
below.
On the other hand, a disadvantage of our model may be that it is possibly
more esoteric for people used to the other one. Moreover, since isolation is encoded by scoping, some care is needed to avoid scope extrusion during reduction.
For this reason, reduction is defined on typechecked terms, where blocks have
been annotated with the information of which local variables will be connected
to the result. In this way, it is possible to define a rather sophisticated notion
of congruence among terms, which allows to move declarations out of a block
only when this preserves well-typedness.
Besides standard type soundness, we proved that uniqueness and lent properties inferred by the type system actually ensure the expected behaviour.
To focus on novelties and allow complete formal proofs, we illustrate our type
and effect system on a minimal language, only supporting the features which
are strictly necessary for significance. However, we expect that the approach
could be smoothly extended to typical constructs of imperative/object-oriented
languages, in the same way as other type systems or type and effect systems
(e.g., when effects are possibly thrown exceptions [34]). We briefly discuss two
key features below.
Inheritance For a method redefined in a heir class, the returned sharing relation should be contained in that of the parent, that is, less connections
should be possibly caused by the method, analogously to the requirement
that possibly thrown exceptions should be a subset (modulo subtyping)
of those of the parent.
Control flow As it is customary in type systems, control flow constructs are
handled by taking the “best common approximation” of the types obtained
by the different paths. For instance, in the case of if-then-else we would get
the union of the sharing relations of the two branches (the same happens
for possibly thrown exceptions).
Note that including control flow constructs we would get, again as it is
customary in type systems, which are never complete for exactly this reason,
examples which are ill-typed but well-behaved at runtime. For instance, an
expression of shape:
D y = new D ( y );
Ca z = {
D x = new D ( x );
if (...) x . f = x else x . f = y ;
x
};
z

32

will be ill-typed, since the sharing relation computed for the right-hand side of
the declaration of z is {y, res}, that is, the type and effect system conservatively
assumes that this expression does not denote a capsule. However, if the guard
of the conditional evaluates to true, then the right-hand side of the declaration
reduces to a capsule.
We have implemented in Coq the type and effect system and the reduction
rules. The current code can be found at //github.com/paola-giannini/sharing.
We did not include the construct of method call since, as we can see from the
typing and reduction rules, it can be translated into a block. To complete the
implementation of the operational semantics, we need an oriented version of the
congruence relation on terms to be applied before reduction steps, as explained
at the end of Sect.5. Then, we plan to mechanize the full proof of soundness.
As mentioned before, we argue that the Coq implementation nicely illustrates
the advantages of our purely syntactic model, since proofs can be carried out
inductively, without requiring more complicated techniques such as, e.g., bisimulation.
In further work, in addition to completing the formalization in Coq of the
proof of soundness, we will enrich the type system to also handle immutable
references. A preliminary presentation of this extension is in [35].
We also plan to formally state and prove behavioural equivalence of the
calculus with the conventional imperative model. Intuitively, the reachability
information which, in our calculus, is directly encoded in terms, should be reconstructable from the dependencies among references in a conventional model
with a flat global memory.
As a long term goal, it would be interesting to investigate (a form of) Hoare
logic on top of our model. We believe that the hierarchical structure of our
memory representation should help local reasoning, allowing specifications and
proofs to mention only the relevant portion, similarly to what is achieved by
separation logic [27].
References
References
[1] D. Clarke, T. Wrigstad, External uniqueness is unique enough, in:
L. Cardelli (Ed.), ECOOP’03 - Object-Oriented Programming, Vol. 2473
of Lecture Notes in Computer Science, Springer, 2003, pp. 176–200.
[2] P. S. Almeida, Balloon types: Controlling sharing of state in data types, in:
ECOOP’97 - Object-Oriented Programming, Vol. 1241 of Lecture Notes in
Computer Science, Springer, 1997, pp. 32–59.
[3] M. Servetto, D. J. Pearce, L. Groves, A. Potanin, Balloon types for safe
parallelisation over arbitrary object graphs, in: WODET 2014 - Workshop
on Determinism and Correctness in Parallel Programming, 2013.

33

[4] J. Hogg, Islands: Aliasing protection in object-oriented languages, in:
A. Paepcke (Ed.), ACM Symp. on Object-Oriented Programming: Systems, Languages and Applications 1991, ACM Press, 1991, pp. 271–285.
[5] W. Dietl, S. Drossopoulou, P. Müller, Generic universe types, in: E. Ernst
(Ed.), ECOOP’07 - Object-Oriented Programming, Vol. 4609 of Lecture
Notes in Computer Science, Springer, 2007, pp. 28–53.
[6] C. S. Gordon, M. J. Parkinson, J. Parsons, A. Bromfield, J. Duffy, Uniqueness and reference immutability for safe parallelism, in: G. T. Leavens,
M. B. Dwyer (Eds.), ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages and Applications (OOPSLA 2012), ACM
Press, 2012, pp. 21–40.
[7] M. Servetto, E. Zucca, Aliasing control in an imperative pure calculus, in:
X. Feng, S. Park (Eds.), Programming Languages and Systems - 13th Asian
Symposium (APLAS), Vol. 9458 of Lecture Notes in Computer Science,
Springer, 2015, pp. 208–228.
[8] P.
Giannini,
M.
Servetto,
E.
Zucca,
Types for immutability and aliasing control, in:
ICTCS’16 - Italian
Conf. on Theoretical Computer Science, Vol. 1720 of CEUR Workshop
Proceedings, CEUR-WS.org, 2016, pp. 62–74.
URL http://ceur-ws.org/Vol-1720/full5.pdf
[9] J. Boyland, Alias burying: Unique variables without destructive reads,
Softw. Pract. Exper. 31 (6) (2001) 533–553.
[10] K. Naden, R. Bocchino, J. Aldrich, K. Bierhoff, A type system for borrowing permissions, in: ACM Symp. on Principles of Programming Languages
2012, ACM Press, 2012, pp. 557–570.
[11] Y. Zibin, A. Potanin, P. Li, M. Ali, M. D. Ernst, Ownership and immutability in Generic Java, in: ACM SIGPLAN Conference on ObjectOriented Programming, Systems, Languages and Applications (OOPSLA
2010), 2010, pp. 598–617.
[12] P. Giannini, M. Servetto, E. Zucca, A type and effect system for sharing,
in: A. Seffah, B. Penzenstadler, C. Alves, X. Peng (Eds.), OOPS’17 Object-Oriented Programming Languages and Systems, Track at SAC’17
- ACM Symp. on Applied Computing, ACM Press, 2017, pp. 1513–1515.
doi:10.1145/3019612.3019890.
[13] P. Giannini, M. Servetto, E. Zucca, Tracing sharing in an imperative pure
calculus: extended abstract, in: FTfJP’17 - Formal Techniques for Java-like
Programs, ACM Press, 2017, pp. 6:1–6:6. doi:10.1145/3103111.3104038.
[14] A. Igarashi, B. C. Pierce, P. Wadler, Featherweight Java: a minimal core
calculus for Java and GJ, ACM Transactions on Programming Languages
and Systems 23 (3) (2001) 396–450.
34

[15] Z. M. Ariola, M. Felleisen, The call-by-need lambda calculus, Journ. of
Functional Programming 7 (3) (1997) 265–301.
[16] J. Maraist, M. Odersky, P. Wadler, The call-by-need lambda calculus,
Journ. of Functional Programming 8 (3) (1998) 275–317.
[17] R. Milner, Communicating and mobile systems - the Pi-calculus, Cambridge University Press, 1999.
[18] M. Servetto, J. Mackay, A. Potanin, J. Noble, The billion-dollar fix - safe
modular circular initialisation with placeholders and placeholder types, in:
ECOOP’13 - Object-Oriented Programming, Vol. 7920 of Lecture Notes in
Computer Science, Springer, 2013, pp. 205–229.
[19] J. Boyland, Semantics of fractional permissions with nesting, ACM Transactions on Programming Languages and Systems 32 (6).
[20] P. Haller, M. Odersky, Capabilities for uniqueness and borrowing, in:
T. D’Hondt (Ed.), ECOOP’10 - Object-Oriented Programming, Vol. 6183
of Lecture Notes in Computer Science, Springer, 2010, pp. 354–378.
[21] P. Haller, A. Loiko, Lacasa: lightweight affinity and object capabilities in
scala, in: E. Visser, Y. Smaragdakis (Eds.), ACM SIGPLAN Conference
on Object-Oriented Programming, Systems, Languages and Applications
(OOPSLA 2016), ACM Press, 2016, pp. 272–291.
[22] S. Clebsch, S. Drossopoulou, S. Blessing, A. McNeil, Deny capabilities for
safe, fast actors, in: E. G. Boix, P. Haller, A. Ricci, C. Varela (Eds.),
International Workshop on Programming Based on Actors, Agents, and
Decentralized Control, AGERE! 2015, ACM Press, 2015, pp. 1–12.
[23] E. Castegren, T. Wrigstad, Reference capabilities for concurrency control,
in: S. Krishnamurthi, B. S. Lerner (Eds.), ECOOP’16 - Object-Oriented
Programming, Vol. 56 of LIPIcs, Schloss Dagstuhl - Leibniz-Zentrum fuer
Informatik, 2016, pp. 5:1–5:26.
[24] E. Castegren, T. Wrigstad, Relaxed linear references for lock-free data
structures, in: P. Müller (Ed.), ECOOP’17 - Object-Oriented Programming, Vol. 74 of LIPIcs, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2017, pp. 6:1–6:32.
[25] D. Clarke, J. Östlund, I. Sergey, T. Wrigstad, Ownership types: A survey,
in: D. Clarke, J. Noble, T. Wrigstad (Eds.), Aliasing in Object-Oriented
Programming. Types, Analysis and Verification, Vol. 7850 of Lecture Notes
in Computer Science, Springer, 2013, pp. 15–58.
[26] P. Müller, A. Rudich, Ownership transfer in universe types, in: R. P.
Gabriel, D. F. Bacon, C. V. Lopes, G. L. S. Jr. (Eds.), ACM SIGPLAN
Conference on Object-Oriented Programming, Systems, Languages and
Applications (OOPSLA 2007), ACM Press, 2007, pp. 461–478.
35

[27] J. C. Reynolds, Separation logic: A logic for shared mutable data structures, in: Proc. IEEE Symp. on Logic in Computer Science 2002, IEEE
Computer Society, 2002, pp. 55–74.
[28] R. L. B. Jr., V. S. Adve, D. Dig, S. V. Adve, S. Heumann, R. Komuravelli,
J. Overbey, P. Simmons, H. Sung, M. Vakilian, A type and effect system for
deterministic parallel Java, in: S. Arora, G. T. Leavens (Eds.), ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages
and Applications (OOPSLA 2009), ACM Press, 2009, pp. 97–116.
[29] A. Turon, Rust: from POPL to practice (keynote), in: G. Castagna, A. D.
Gordon (Eds.), ACM Symp. on Principles of Programming Languages 2017,
ACM Press, 2017, p. 2.
[30] B. Steensgaard, Points-to analysis by type inference of programs with structures and unions, in: T. Gyimóthy (Ed.), Compiler Construction - CC’96,
Vol. 1060 of Lecture Notes in Computer Science, Springer, 1996, pp. 136–
150.
[31] A. De, D. D’Souza, Scalable flow-sensitive pointer analysis for Java with
strong updates, in: J. Noble (Ed.), ECOOP’12 - Object-Oriented Programming, Vol. 7313 of Lecture Notes in Computer Science, Springer, 2012, pp.
665–687.
[32] M. Servetto, L. Groves, True small-step reduction for imperative objectoriented languages, FTfJP’13- Formal Techniques for Java-like Programs.
[33] A. Capriccioli, M. Servetto, E. Zucca, An imperative pure calculus, Electronic Notes in Theoretical Computer Science 322 (2016) 87–102.
[34] D. Ancona, G. Lagorio, E. Zucca, A core calculus for java exceptions, in: L. M. Northrop, J. M. Vlissides (Eds.), ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages and Applications (OOPSLA 2001), ACM Press, 2001, pp. 16–30.
doi:10.1145/504282.504284.
[35] P. Giannini, M. Servetto, E. Zucca, A type and effect system for uniqueness
and immutability, in: OOPS’18 - Object-Oriented Programming Languages
and Systems, Track at SAC’18 - ACM Symp. on Applied Computing, ACM
Press, 2018, to appear.

36

Γ ⊢ c1 : C | {c1, res}
Γ ⊢ c2 : C | {c2, res}
D1 :

Γ ⊢ c2.mix(c1) : C | {c1, c2, res}

Γ ⊢ r : C | {r, res}
Γ ⊢ c3 : C | {c3, res}

D2 :

Γ ⊢ r.mix(c3) : C | {c3, r, res}

Γ ⊢ c2.mix(c1).clone() : C | {c1, c2}
Γ ⊢ c3 : C | {c3, res}
D3 :

Γ ⊢ new C(c3) : C | {c3, res}

D1

D2

Γ1 [Γ2 ] ⊢ {C c3=new C(c3); C r=c2.mix(c1).clone(); r.mix(c3)} : C | {c1, c2}

Γ1 [Γ2 ] ⊢ inner : C | ǫ
Γ1 [Γ2 ] ⊢ c2 : C | {c2, res}

Γ1 [Γ2 ] ⊢ c2 : C | {c2, res}
D4 :

Γ1 [Γ2 ] ⊢ new C(c2) : C | {c2, res} D3 Γ1 [Γ2 ] ⊢ inner.mix(c2) : C | {c2, res}
Γ1 ⊢ {C c2=new C(c2); Ca inner=ei ; inner.mix(c2)} : C | {c1, res}
Γ1 ⊢ c1 : C | {c1, res}

D : Γ1 ⊢ new C(c1) : C | {c1, res}

D4

Γ1 ⊢ outer : C | {outer, res}

⊢ {C c1=new C(c1); C outer=eo ; outer} : C | ǫ

• D3 yields eia = {{r,c3} C c3=new C(c3); C r=c2.mix(c1).clone(); r.mix(c3)}
• D4 yields eoa = {{c2} C c2=new C(c2); Ca inner=ei ; inner.mix(c2)}
• D yields e′ ={{outer} C c1=new C(c1); C outer=eo ; outer}

Figure A.8: Type derivation for Example 7
Appendix A. Type derivation for Example 7
In Fig.A.8 we give the type derivation that shows that the expression e of
Example 7 is well-typed, where Γ1 = c1:C, outer:C, Γ2 = c2:C, inner:Ca , and
Γ3 = c3:C, r:C are the type contexts corresponding to the top level, outer, and
inner block, respectively.
Derivations D1 and D2 end with an application of rule (T-Invk). Consider D2 .
The method mix produces sharing between its receiver, parameter, and result.
Then the call of mix with receiver r and parameter c3 returns a result connected
with both these variables. The call of mix with receiver c2 and parameter c1 in
the derivation D1 does the same with c2 and c1. Instead, the call of clone does
not produce any connection from its receiver and result. So the call of clone
with receiver c2.mix(c1) in the derivation D1 does not cause connections for
res.
The type derivation D3 justifies the judgment Γ1 [Γ2 ] ⊢ ei : C | {c1, c2} where
37

ei is the inner block (the initialization expression of inner). The effects of
the evaluation of initialization expressions and body are to mix the external
variables c1 and c2, and the local variables r and c3. Moreover, the result is
only connected with the two local variables. Hence, the inner block denotes
a capsule, so it can be used as initialization expression of the affine variable
inner. The sharing relation resulting from the evaluation of the declarations
and the body (before removing the local variables r and c3) is represented by
{c1, c2} {c3, r, res}. The annotation for the block, i.e., the set of local variables
connected to the result, is {r, c3}, so, when applying the congruence relation,
the variables r and c3 cannot be moved outside this block.
The type derivation D4 justifies the judgment Γ1 ⊢ eo : C | {c1, res}, where
o
e is the outer block (the initialization expression of outer). The effects of
the evaluation of initialization expressions and body are to mix the external
variable c1 with the local variable c2 (this effect propagates from the inner
block). Moreover, the result is connected with variable c2. Hence, the result
turns out to be connected with the external variable c1 as well. Therefore, this
block is not a capsule, and could not be used to initialize an affine variable.
Note that the variable inner, being affine, is not in the domain of the sharing
relation. Indeed, it will be substituted with the result of the evaluation of ei
and so it will disappear.
Finally, D is the derivation for the expression e. The block is a closed
expression, and closed expressions are capsules. The block is annotated with
the local variable outer, which is connected with its result.
Appendix B. Proofs
Proposition 9. If v is a value, then there exists v ′ such that v ∼
= v ′ and v ′ is
in canonical form.
Proof. By structural induction on values.
Consider first new C (vs). By inductive hypotheses we have that new C (vs) ∼
=
new C (vs ′ ) where all values in vs ′ are in canonical form. By induction on the
number n of v ∈ vs ′ such that v is not a variable. If n = 0 then, using rule
{x }
′
(new), we have that new C (vs ) ∼
= { C x =new C (vs ′ ); x } which is in canonX
′
ical form. Otherwise new C (vs ) = new C (xs, { dvs x }, vs′′ ) where dvs 6= ǫ
is in canonical form. We may assume, by α-renaming, that (FV(vs ′′ ) ∪ {xs}) ∩
X
dom(dvs) = ∅. Using rule (val-ctx) we have that new C (vs ′ ) ∼
= { dvs v ′ } where
v ′ = new C (xs, x , vs ′′ ). Since v ′ has n − 1 arguments which are not variables we can apply the induction hypothesis and derive that new C (vs ′ ) ∼
=
{Y dvs {X dvs ′ new C (xs, x , ys)}}. Using rule (body), by first doing α-renaming
Z
if needed, for some Z , we have that new C (vs ′ ) ∼
= { dvs dvs ′ new C (xs, x , ys)}.
Applying rule (new) followed by (body) we prove the result.
X
Consider { dvs v }. We reason by induction on the total number n of declarations C x =new C (vs); ∈ dvs which are not in canonical form.

38

n = 0 That is, dvs is in canonical form. We consider two cases.
X
X
X
Case: { dvs x }. Using rule (reorder), we have that { dvs x } ∼
= { dvs ′ dvs |x x }
for some dvs ′ . By definition of dvs |x , (FV(dvs |x ) ∪ {x }) ∩ dom(dvs ′ ) = ∅.
X′
Therefore, applying rule (garbage), {X dvs x } ∼
= { dvs |x x }, with X ′ = X \
X′

X′

dom(dvs ′ ). If dvs |x is not empty then v ′ = { dvs |x x }, and { dvs |x x } ∼
=
x applying rule (block-elim), so v ′ = x .
Case: {X dvs v } where v is a block. By induction hypothesis either v ∼
= y,
X
∼
hence v = { dvs y} and we get the thesis from the previous case, or
Y
′
′
′
′
{X dvs v } ∼
= { dvs y}, with dvs 6= ǫ, dvs = dvs and all the evalu|y

ated declarations in dvs ′ are of the required shape. In the latter case,
X
X
Y
{ dvs v } ∼
= { dvs { dvs ′ y}}. We may assume, by α-renaming, that
′
dom(dvs ) ∩ (FV(dvs) ∪ dom(dvs)) = ∅, so rule (body) can be applied to obX
X ∪Y
∅
tain { dvs v } ∼
dvs dvs ′ { y}} and with rule (block-elim) we obtain
={
X
X
∪Y
′
{ dvs v } ∼
dvs dvs y}, and we get the thesis from the previous
= {
case.
n > 0 We may assume that dvs = dvs 1 C z =new C (vs); dvs 2 with dvs 1 in
canonical form, the values in vs in canonical form, and some v ∈ vs ′
not a variable. As for the proof for constructor values we can prove that
Y
′
′
new C (vs) ∼
= { dvs new C (ys)} for some Y , ys and dvs in canonical
X
X
Y
form. Therefore { dvs v } ∼
= { dvs 1 C z ={ dvs ′ new C (ys)}; dvs 2 v }.
We may assume, by α-renaming, that dom(dvs ′ ) ∩ (FV(dvs 1 dvs 2 v ) ∪
dom(dvs 1 dvs 2 )) = ∅. Therefore, by applying rule (dec) and (block-elim)
we get
X
Y
{ dvs 1 C z ={ dvs ′ new C (vs)}; dvs 2 v } ∼
= v′
X

where v ′ = { dvs 1 dvs ′ C z =new C (ys); dvs 2 v }. Since dvs ′ is in canonical form, the number of declarations which are not in canonical form in
v ′ is n − 1, hence the thesis holds by the inductive hypothesis.

Lemma 12. (Congruence preserves types) Let e1 and e2 be annotated expressions such that Γ ⊢ e1 : C1 | S1 and Γ ⊢ e2 : C2 | S2 . If e1 ∼
= e2 , then C1 = C2 ,
and, for all x ∈ (FV(e1 ) ∩ FV(e2 )) ∪ {res}, [x ]S1 = [x ]S2 .
Proof. By cases on the congruence rule used. We do the most interesting cases,
which are rule (dec) and (garbage) of Fig.6.
Rule (dec). In this case
(1)
(2)
(3)
(4)

Y

X

e1 = { ds C µ x ={ ds 1 ds 2 e}; ds ′ e ′ },
e2 = {Y ds ds 1 C µ x ={X \dom(ds 1 ) ds 2 e}; ds ′ e ′ },
FV(ds 1 ) ∩ dom(ds 2 ) = ∅,
FV(ds ds ′ e ′ ) ∩ dom(ds 1 ) = ∅, and

39

(5) if µ = a then dom(ds 1 ) ∩ X = ∅.
Let Γ ⊢ e1 : C1 | S1 , define Γ1 = Γ[Γds , x :C µ , Γds ′ ], and Zd = dom(ds) ∪
dom(ds ′ ) ∪ {x }. From (1) and rule (T-block) we have that
(a) Γ1 ⊢ e ′ : C1 | S ′ for some S ′ , and
X

(b) Γ1 ⊢ ds C µ x ={ ds 1 ds 2 e}; ds ′ : Sd , where Sd = Sds + Sx + Sds ′ for some
Sds , Sx , and Sds ′ .
Therefore, Y = [res](Sd +S ′ ) ∩ Zd , and S1 = (Sd + S ′ )\Zd . From (b) we have
X
that Γ1 ⊢ { ds 1 ds 2 e} : C | Sx , for some Sx , and if µ = a, then capsule(Sx ).
′
Let Γ1 = Γ1 [Γds 1 , Γds 2 ], and Z = dom(ds 1 ) ∪ dom(ds 2 ) from rule (T-Block)
(c) Γ′1 ⊢ e : C | S for some S,
(d) Γ′1 ⊢ ds 1 : Sds 1 for some Sds 1 ,
(e) Γ′1 ⊢ ds 2 : Sds 2 for some Sds 2 , and
(f ) let Sx′ = Sds 1 + Sds 2 + S, we have that Sx = Sx′ \Z , and X = [res]Sx′ ∩ Z .
From (4) we may assume that dom(Γ1 ) ∩ dom(ds 1 ) = ∅. So Γ′1 = Γ1 , Γds 1 [Γds 2 ].
Let Sx′′ = Sds 2 + S. From (c) and (e) applying rule (T-Block) we have that
(∗) Γ1 , Γds 1 ⊢ {

[res]S ′′ \dom(ds 2 )
x

ds 2 e} : C | Sx′′ \dom(ds 2 ).

If µ = a, then capsule(Sx ). From (5) and (f) we get that capsule(Sx′ ). Finally,
since Sx′ = Sx′′ + Sds 1 , and so [res]Sx′′ \dom(ds 2 ) ⊆ [res]Sx′ \dom(ds 2 ) we derive
that capsule(Sx′′ ).
Define Γ′′1 = Γ[Γds , Γds 1 , x :C µ , Γds ′ ]. From (4) we have that Γ′′1 = Γ1 , Γds 1 .
From (a) and Lemma 11.1, we derive
(a1) Γ′′1 ⊢ e ′ : C1 | S ′ .
From (d), (3), (4), and Lemma 11.2, we have that Γ′′1 ⊢ ds 1 : Sds 1 . Therefore,
from (b), (∗), and Lemma 11.1, we derive
[res]

\dom(ds 2 )

′′
Sx
(b1) Γ′′1 ⊢ ds ds 1 C µ x ={
Sds 1 + (Sx′′ \dom(ds 2 )) + Sds ′ .

ds 2 e}; ds ′ : Sd′ , where Sd′ = Sds +

Let Z ′ = dom(ds)∪dom(ds ′ )∪dom(ds 1 )∪{x }. From (a1), (b1) and rule (T-block)
we get
Y′

Γ⊢{

ds ds 1 C µ x ={

[res]S ′′ \dom(ds 2 )
x

ds 2 e}; ds ′ e ′ } : C1 | S1′

where, Y ′ = [res](Sd′ +S ′ ) \Z ′ , and S1′ = (Sd′ + S ′ )\Z ′ . From (4) and Proposition 2.2 we have that the domain of Sds +(Sx′′ \dom(ds 2 ))+Sds ′ does not contain
variables in dom(ds 1 ). Therefore Y ′ = Y , S1′ = S1 , and Γ ⊢ e2 : C1 | S1 .
In a similar way we can prove that Γ ⊢ e2 : C2 | S2 implies Γ ⊢ e1 : C2 | S2 , which
proves the result.
Rule (garbage). In this case
40

X

(1) e1 = { dvs ds e},
(2) e2 = {X \dom(dvs) ds e},
(3) (FV(ds) ∪ FV(e)) ∩ dom(dvs) = ∅.
From (3), and the definition of declarations connected to a set of variables, we
have that, dvs |(FV(e)∪FV(ds)) = ǫ. Therefore, from Proposition 2.3, we have that
X = X \ dom(dvs).
Let Γ ⊢ e1 : C1 | S1 , from (1) and rule (T-block) we have that
(a) Γ[Γdvs , Γds ] ⊢ e : C1 | S for some S,
(b) Γ[Γdvs , Γds ] ⊢ ds : S ′ for some S ′ , and
(c) Γ[Γdvs , Γds ] ⊢ dvs : S ′′ for some S ′′ .
Let Z = dom(dvs) ∪ dom(ds), we have that X = [res](S+S ′ +S ′′ ) ∩ Z , and
S1 = (S + S ′ + S ′′ )\Z . From (3), (a), (b), and Lemma 11.2, we have that
(a1) Γ[Γds ] ⊢ e : C1 | S, and
(b1) Γ[Γds ] ⊢ ds : S ′ .
X

From (a1), (b1), and rule (T-block) we get Γ ⊢ { ds e} : C1 | S1′ where X1′ =
[res](S ′ +S) \dom(ds) and S1′ = (S ′ +S)\dom(ds). From (3), and Proposition 2.2,
we have that the domain of S ′ + S does not contain variables in dom(dvs).
Therefore, X1′ = X1 , and S1′ = S1 . Therefore, Γ ⊢ e2 : C1 | S1 .
On the other side, assume that Γ ⊢ e2 : C2 | S2 , from (2), and rule (T-block) we
have that
(a2) Γ[Γds ] ⊢ e : C2 | S for some S,
(b2) Γ[Γds ] ⊢ ds : S ′ for some S ′ .
where S2 = (S + S ′ )\dom(ds). From Γ ⊢ e1 : C1 | S1 , and rule

(T-Block),

(c2) Γ[Γdvs , Γds ] ⊢ dvs : S ′′ for some S ′′ .
From (3), (a2), (b2), and Lemma 11.1, we have that
(a3) Γ[Γdvs , Γds ] ⊢ e : C2 | S, and
(b3) Γ[Γdvs , Γds ] ⊢ ds : S ′ .
X

Therefore, from (a3), (b3), (c2), and rule (T-block) we get Γ ⊢ { dvs ds e} :
C2 | S2′ , where S2′ = (S + S ′ + S ′′ )\(dom(ds) ∪ dom(dvs)). From (3), and Proposition 2.2, we have that the domain of S ′ + S does not contain variables in
dom(dvs). Therefore, S2′ = S2 , which proves the result.
Lemma 14. (Decomposition) If e is not a value, then there are E and ρ such
that e ∼
= E[ρ].

41

Proof. By structural induction on expressions.
X
If v .f =v ′ , then from Proposition 9 we have that v = x or v = { dvs x } and
Y
X
Y
v ′ = y or v ′ = { dvs ′ y}. If v = { dvs x } and v ′ = { dvs ′ y}, we may
′
assume, by α-renaming, that dom(dvs) ∩ dom(dvs ) = ∅. From rule (val-ctx)
X ∪Y
dvs dvs ′ x .f =y}. So v .f =v ′ ∼
(applied twice) v .f =v ′ ∼
= E[x .f =y] where
={
X ∪Y
′
E={
dvs dvs [ ]} The other cases are easier.
For field access the proof is similar.
Method call is a redex so the result holds with E = [ ].
If {X ds e} is not a value, then either
(1) ds = dvs T x =e1 ; ds 1 where e1 is not new C (xs) for some C and xs or
(2) ds = dvs and e is not a value.
In case (1), either
(a) e1 is not a value or
(b) e1 is a value but not new C (xs) for some C and xs.
In case (a), by induction hypothesis, there are E, and ρ such that e1 ∼
= E[ρ].
Applying rule (reorder) of Fig.6 we have that
{ dvs dvs 1 T x =e1 ; ds 2 e} ∼
= { dvs T x =e1 ; ds 1 e}
X

X

where dvs 1 are all the evaluated declarations of ds 1 . Therefore { ds e} ∼
= E ′ [ρ]
X
′
where E = { dvs dvs 1 T x =E; ds 2 e}.
X
In case (b), by Proposition 9, either e1 ∼
= { dvs ′ y}. If T = D a for
= y or e1 ∼
X
some D , then the block is a redex, else either e1 ∼
= { dvs ′ y}.
= y or e1 ∼
X
X
If e1 ∼
= y, then { ds e} is congruent to { dvs T x =y; ds 1 e}, which is a redex.
X
X
X
X
′
′
∼
If e1 = { dvs y}, then { dvs T x =e1 ; ds 1 e} ∼
= { dvs T x ={ dvs y}; ds 1 e}
Since T = D for some D , with a suitable renaming of the bound variables in
dvs ′ , applying congruence rule (Dec) we have
X

{ dvs T x =e1 ; ds 1 e} ∼
= { dvs dvs ′ T x =y; ds 1 e}
X

X

and the expression on the right is a redex.
In case (2), by induction hypothesis, there are E, and ρ such that e ∼
= E[ρ].
X
Therefore {X ds e} ∼
= E ′ [ρ] where E ′ = { dvs E}.
The following lemma asserts that subexpressions of typable expressions are
themselves typable, and may be replaced with expressions that have the same
type and the same or possibly less sharing effects.
Lemma 15. (Context) Let Γ ⊢ E[e] : C | S, then
1. Γ[ΓE ] ⊢ e : D | S1 for some D and S1 ,
2. if Γ[ΓE ] ⊢ e ′ : D | S2 where S2 ⊑ S1 (S2 = S1 ), then Γ ⊢ E[e ′ ] : C | S ′ with
S ′ ⊑ S (S ′ = S).
Proof.

1. Easy, by induction on evaluation contexts.
42

2. Let Γ ⊢ E[e] : C | S. By (1) Γ[ΓE ] ⊢ e : D | S1 for some D and S1 . By
induction on evaluation contexts.
If E = [ ], then C = D and S1 = S. The result is immediate.
If E = {X dvs T x =E ′ ; ds eb }, then Γ ⊢ {X dvs T x =E ′ [e]; ds eb } : C | S.
(a) From rule (T-block) we have Γ[Γdvs , x :T , Γds ] ⊢ E ′ [e] : C3 | S3 for some
C3 and S3 where T = C3µ , and
(b) from (1) we derive that Γ[Γdvs , x :T , Γds ][ΓE ′ ] ⊢ e : D | S1 for some D
and S1 .
Let Γ[Γdvs , x :T , Γds ][ΓE ′ ] ⊢ e ′ : D | S2 where S2 ⊑ S1 (S2 = S1 ). From(a),
by induction hypothesis on E ′ , we have that Γ[Γdvs , x :T , Γds ] ⊢ E ′ [e ′ ] :
X
C3 | S ′ where S ′ ⊑ S3 (S ′ = S3 ). From Γ ⊢ { dvs T x =E ′ [e]; ds eb } :
C | S, if µ = a, then capsule(S3 ), and so also capsule(S ′ ). Therefore,
X
applying rule (T-block) we have Γ ⊢ { dvs T x =E ′ [e ′ ]; ds eb } : C | S ′′ for
′′
some S . Moreover, from Proposition 1.1 and Proposition 1.2 we derive
that S ′′ ⊑ S (S ′′ = S).
If E = {X dvs E}, then the proof is similar to the previous one.

Lemma 17. Let Γ ⊢ v : C | S where v is a canonical value. If capsule(S), then
S = ǫ.
Proof. By case analysis on the shape of canonical values.
Let v = x . [res]S = {res} if and only Γ ⊢ x : C | S is derived using rule
(T-affine-var). Therefore S = ǫ.
Let v = {X dvs x } where dvs = T1 x1 =new C1 (xs 1 ); . . . Tn xn =new Cn (xs n ); 6= ǫ
and dvs |x = dvs. Let Γ′ = x1 :T1 , . . . , x1 :Tn . From rule (T-block) and (T-new)
we have that Γ[Γ′ ] ⊢ new Ci (xs i ) : C | Si where Si = {xs i , res} (1 ≤ i ≤ n).
If Si′ = (Si + {xi , res})\res, then Si′ = {xs i , xi }. From dvs |x = dvs we get
that x = xj for some j, 1 ≤ jS≤ n. So Γ[Γ′ ] ⊢ x : C | {xj , res}. Therefore
S = S ′ \dom(Γ′ ) where S ′ = 1≤i≤n {xs i , xi } ∪ {xj , res}, i.e., in S ′ all the
variables are in
S the same equivalence class of res. If [res]S = {res}, then it
must be that 1≤i≤n {xs i , xi } ⊆ dom(Γ′ ). Therefore we get that S = ǫ.
Lemma 18. If Γ ⊢ E[e] : C | S and Γ ⊢ e : D | S ′ , then S ′ \X ⊑ S where
X = {res} ∪ HB(E).
Proof. By induction on E.
For E = [ ] is obvious.
Let E = {X dvs C1µ x =E ′ ; ds eb }. From Γ ⊢ E[e] : C | S and rule
Γ′ = Γdsds ′ [x :T ]
(a) Γ[Γ′ ] ⊢ E ′ [e] : C1 | S1 ,
(b) Γ[Γ′ ] ⊢ dvs ds : S2 , and
(c) Γ[Γ′ ] ⊢ eb : | S3 .
43

(T-Block),

let

(d) S = (S1′ + S2 + S3 )\dom(Γ′ ) where S1′ = (S1 + {x , res})\res.
Let Γ ⊢ e : D | S ′ and Y = {res} ∪ HB(E ′ ). By induction hypothesis, we
have that S ′ \Y ⊑ S1 , and so also S ′ \Y ⊑ S1′ . From Proposition 1.1 we
derive that S ′ \Y ⊑ S1′ + S2 + S3 . Since HB(E) = HB(E ′ ) ∪ dom(Γ′ ) we get
that (S ′ \Y )\dom(Γ′ ) = S ′ \X . Therefore from Proposition 1.2 we derive that
S ′ \Y ⊑ S.
X
Similar (and simpler) for E = { dvs E ′ }.
Lemma 19. If
• Γ ⊢ E[e1 ] : C | S1 , Γ ⊢ E[e2 ] : C | S2 ,
• Γ ⊢ e1 : D | X1 and Γ ⊢ e2 : D | X2 with
– res ∈ X1 iff res ∈ X2 , and
– (X1 ∪ X2 ) ∩ HB(E) = ∅
then S1 + Y = S2 + Y where Y = (X1 ∪ X2 ) \ {res}.
Proof. Let E = [ ]. Then Si = Xi (1 ≤ i ≤ 2) and HB(E) = ∅.
• If res ∈ X1 , then S1 + Y = X1 ∪ X2 , and since also res ∈ X2 we have
that S2 + Y = X1 ∪ X2 .
• If res 6∈ X1 , since Y = X1 ∪ X2 we have that S1 + Y = X1 ∪ X2 and since
also res 6∈ X2 we have that S2 + Y = X1 ∪ X2 .
X

X

Let E = { dvs D µ x =E ′ ; ds eb }, Γ ⊢ { dvs D µ x =E ′ [e1 ]; ds eb } : C | S1 ,
X
Γ ⊢ { dvs D µ x =E ′ [e2 ]; ds eb } : C | S2 , Γ ⊢ e1 : C | X1 , and Γ ⊢ e2 : C | X2 .
From rule (T-Block), let Γ′ = Γdsds ′ [x :T ]
(a) Γ[Γ′ ] ⊢ E ′ [e1 ] : C1 | S3 , and Γ[Γ′ ] ⊢ E ′ [e2 ] : C1 | S4
(b) Γ[Γ′ ] ⊢ dvs ds : S5 , and
(c) Γ[Γ′ ] ⊢ eb : | S6 .
(d) S1 = (S1′ + S5 + S6 )\dom(Γ′ ) and S2 = (S2′ + S5 + S6 )\dom(Γ′ ) where
S1′ = (S3 + {x , res})\res and S2′ = (S4 + {x , res})\res.
Let Y = (X1 ∪X2 )\{res}. By induction hypotheses we have that S3 +Y = S4 +
Y . Therefore we have that S3 +{x , res}+Y = S4 +{x , res}+Y . Since res 6∈ Y
we have that (Si + {x , res} + Y )\res = (Si + {x , res})\res+ Y (3 ≤ i ≤ 4). So
we have that S1′ +Y = S2′ +Y and therefore S1′ +S5 +S6 +Y = S2′ +S5 +S6 +Y ,
which implies (S1′ + S5 + S6 + Y )\dom(Γ′ ) = (S2′ + S5 + S6 + Y )\dom(Γ′ ).
Since Y ∩ dom(E) = ∅ we have that Y ∩ dom(Γ′ ) = ∅, and Y \dom(Γ′ ) = Y .
Therefore from Proposition 1.3 we have that ((S1′ + S5 + S6 ) + Y )\dom(Γ′ ) =
(S1′ + S5 + S6 )\dom(Γ′ ) + Y ) = S1 + Y = (S2′ + S5 + S6 + Y )\dom(Γ′ ) =
(S2′ + S5 + S6 )\dom(Γ′ ) + Y ) = S2 + Y .
Similar (and simpler) for E = {X dvs E ′ }.
Theorem 22. (Subject reduction) If Γ ⊢ e1 : C | S and e1 −→ e2 , then
44

1. Γ ⊢ e2 : C | S ′ where S ′ ⊑ S, and
2. for all x such that e1 = Cx [e], e2 = Cx′ [e ′ ], and ΓCx ⊢ e : D | Sx we
have that: ΓCx′ ⊢ e ′ : D | Sx′ and (Sx′ + Sdvs ′ ) ⊑ (Sx + Sdvs ) where dvs =
dec(C, FV(e)) and dvs ′ = dec(C ′ , FV(e ′ )).
Proof. By Lemma 14, e1 ∼
= E[ρ], and, since we may have applied rule (congr) of
E
Fig.7, we have that e2 ∼
= ′ [e ′ ] where E[ρ] −→ E ′ [e ′ ] has been derived by one of
the other rules. Let Γ ⊢ E[ρ] : C | S. By case analysis on the rule of Fig.7 used
for E[ρ] −→ E ′ [e ′ ].
Rule (field-access) and Rule (field-assign) are in the main paper.
Rule (invk).
1. In this case ρ = v0 .m(v1 , .., vn ) and
e ′ = {C0µ this=v0 ; C1µ1 x1 =v1 ; ..Cnµn xn =vn ; eb }
where meth(C0 , m)=hD | Sb , µ0 , C1µ1 x1 . . . Cnµn xn , eb i. From Lemma 15.1
we have that Γ[ΓE ] ⊢ v0 .m(v1 , .., vn ) : D | S ′′ for some S1′ . From typing
rule (T-invk)
(1) Γ[ΓE ] ⊢ vi : Ci | Si ( 0 ≤ i ≤ n)
(2) ∀ 0 ≤ i ≤ n µi = a =⇒ capsule(Si )
(3) S0′ = (S0 + {this, res})\res
(4) Si′ = (Si + {xi , res})\res (1 ≤ i ≤ n)
n
P
(5) S ′′ = ( Si′ + Sb )\{this, x1 , . . . , xn }
i=1

From the fact that the class table is well-typed we have that Γ′ ⊢ eb : D | Sb
where Γ′ = this:C0µ , x1 :C1µ1 , . . . , xn :Cnµn . Moreover, since we may assume
that {this, x1 , . . . , xn } ∩ dom(Γ[ΓE ]) = ∅, from Lemma 11 we have that
(a) Γ[ΓE ][Γ′ ] ⊢ eb : D | Sb , and
(b) Γ[ΓE ][Γ′ ] ⊢ vi : Ci | Si ( 0 ≤ i ≤ n).
Therefore by typing rule (T-block), (1)÷(5), (a) and (b) we have that
Γ[ΓE ] ⊢ e ′ : D | S ′′ . From Lemma 15.2 we derive Γ ⊢ E[e ′ ] : D | S.
2. The result is proved as in the case of (field-assign) just replacing Sx′ ⊑ Sx
with Sx′ = Sx since the sharing relation of the redex is equal to the one of
the block to which it reduces.
Rule

(alias-elim).

1. In this case
(1) ρ = {X ds ′ eb } where ds ′ = dvs C1 x =y; ds
X\{x }
(2) e ′ = {
dvs ds[y/x ] eb [y/x ]}
X
From Lemma 15.1 we have that Γ[ΓE ] ⊢ { ds ′ eb } : D | S1 for some S1 .
Therefore from typing rule (T-block) we have that
(a) Γ[ΓE ][Γds ′ ] ⊢ dvs : S2 for some S2 ,
(b) Γ[ΓE ][Γds ′ ] ⊢ C1 x =y; : {x , y},
(c) Γ[ΓE ][Γds ′ ] ⊢ ds : S3 for some S3 ,
(d) Γ[ΓE ][Γds ′ ] ⊢ eb : D | S4 for some S4 ,

45

(e) S1 = S1′ \dom(ds ′ ) where S1′ =
dom(ds ′ ).

4
P
i=2

Si + {x , y} and X = [res]S1′ ∩

Since x cannot be free in dvs, from Lemma 11.2 and (a) we derive
(a1) Γ[ΓE ][Γds ′ \x ] ⊢ dvs : S2 \x .
From Lemma 16.1 and (c) and (d) we have that
(c1) Γ[ΓE ][Γds ′ ]\x ⊢ ds[y/x ] : S3 \x and
(d1) Γ[ΓE ][Γds ′ ]\x ⊢ eb [y/x ] : S4 \x .
Moreover,
(e1) let S ′′ =

4
P

(Si \x ),

i=2

from (a1), (c1)-(e1) and rule (T-block) we have that
Y
Γ[ΓE ][Γds ′ ] ⊢ { dvs ds[y/x ] eb [y/x ]} : D | S ′′ \dom(dvs ds)
where Y = [res]S ′′ ∩ dom(dvs ds). If x 6∈ [res]S1′ , then [res]S1′ = [res]S ′′ ,
and since dom(dvs ds) ∪ {x} = dom(ds ′ ) we have that X = Y . If x ∈
[res]S1′ , then [x ]S1′ = [res]S1′ and from (e) we have that [x ]S1′ = [res]S1′ =
[y]S1′ . Therefore [res]S ′′ = [res]S1′ \{x } and Y = X \{x }. From Si \x ⊑ Si
(2 ≤ i ≤ 4) and Proposition 1.1 we have that S ′′ ⊑ S1′ . Therefore from
Proposition 1.2 we derive S2 ⊑ S1 .
2. The result is proved as in the case of (field-assign) since from S2 ⊑ S1 by
Lemma 15 we derive Sx′ = Sx .
Rule

(affine-elim).

1. In this case
X
(1) ρ = { ds ′ eb } where ds ′ = dvs C1a x =v ; ds
X\{x }
(2) e ′ = {
dvs ds[v /x ] eb [v /x ]}
From Lemma 15.1 we have that Γ[ΓE ] ⊢ {X ds ′ eb } : D | S1 for some S1 .
Therefore from typing rule (T-block) we have that
(a) Γ[ΓE ][Γds ′ ] ⊢ dvs : S2 for some S2 ,
(b) Γ[ΓE ][Γds ′ ] ⊢ v : C1 | Sv where capsule(Sv ), therefore also Γ[ΓE ][Γds ′ ] ⊢
C1a x =v ; : Sv
(c) Γ[ΓE ][Γds ′ ] ⊢ ds : S3 for some S3 ,
(d) Γ[ΓE ][Γds ′ ] ⊢ eb : D | S4 for some S4 ,
(e) S1 = S1′ \dom(ds ′ ) where S1′ =

4
P

Si + Sv and X = [res]S1′ ∩ dom(ds
i=2
C1a , and Lemma 17 we have that Sv =

From (b), the fact that Γds ′ (x ) =
Since x cannot be free in dvs, from Lemma 11.2 and (a) we derive
(a1) Γ[ΓE ][Γds ′ \x ] ⊢ dvs : S2 \x .
From (b) with Sv = ǫ, Lemma 16.2 and (c) and (d) we have that
(c1) Γ[ΓE ][Γds ′ ]\x ⊢ ds[v /x ] : S3 \x and
46

′

).
ǫ.

(d1) Γ[ΓE ][Γds ′ ]\x ⊢ eb [v /x ] : S4 \x .
Moreover,
(e1) let S ′′ =

4
P

(Si \x ),

i=2

from (a1), (c1)-(e1) and rule (T-block) we have that
Γ[ΓE ][Γds ′ ] ⊢ {Y dvs ds[v /x ] eb [v /x ]} : D | S ′′ \dom(dvs ds)
where Y = [res]S ′′ ∩ dom(dvs ds). Since [x ]S1′ = {x }, we have that x 6∈
[res]S1′ . Moreover dom(dvs ds) ∪ {x} = dom(ds ′ ). therefore we have that
X = X \x = Y . From Si \x ⊑ Si (2 ≤ i ≤ 4) and Proposition 1.1 we have
that S ′′ ⊑ S1′ .
2. The result is proved as in the case of (field-assign) since from S2 ⊑ S1 by
Lemma 15 we derive Sx′ = Sx .

47

