Inheritance in the
Join Calculus
Cédric Fournet^{*}
Cosimo Laneve^{#}
Luc Maranget^{%}
Didier Rémy^{%}
April 23, 2004 
Abstract:
We design an extension of the join calculus with classbased inheritance.
Method calls, locks, and states are handled in a uniform manner, using
asynchronous messages. Classes are partial message definitions that can be
combined and transformed by means of operators for behavioral and
synchronization inheritance.
We also give a polymorphic type system that statically enforces basic
safety properties.
Our language and its type system are compatible with the JoCaml
implementation of the join calculus.
The join calculus is a simple namepassing calculus, related to the pi
calculus but with a functional
flavor [10, 9]. In this calculus,
communication channels are statically defined: channels are created together
with a set of reaction rules that specify, once
and for all, how messages sent on these names will be synchronized and
processed.
These design choices favor the integration of concurrency and distribution
within a programming language. Indeed, a typed language based on join
calculus has been implemented as an extension of OCaml [17],
called JoCaml [11, 15].
However, the above integration does not address objectoriented
features. Precisely, JoCaml objects are just imported from OCaml and
therefore they are sequential. The main contribution of this work is an
extension of the join calculus with object oriented features that is
compatible with the JoCaml implementation.
Although the join calculus does not have a
primitive notion of object, definitions encapsulate the details of
synchronization much as concurrent objects.
Applying the wellknown objectsasrecords paradigm to the join
calculus, we obtain a simple language of objects with asynchronous
message passing. Method calls, locks, and states are handled in a
uniform manner, using labeled messages.
There is no primitive notion of functions, calling sequences, or
threads (they can all be encoded using continuation messages).
Our languagethe objective join calculusallows finegrained
internal concurrency, as each object may send and receive several
messages in parallel.
For every object of our language, message synchronization is defined
and compiled as a whole. This allows an efficient compilation of
message delivery into automata [16] and simplifies
reasoning on objects.
However, the complete definition of object can be overly restrictive
for the programmer. This suggests some compiletime mechanism for
assembling partial definitions.
To this end, we promote partial definitions into classes. Classes can
be combined and transformed to form new classes. They can also be
closed to create objects.
Objects can be
created by instantiating definition patterns called classes, and
in turn complex classes can be built from simpler ones.
To make this approach effective, the assembly of classes should rely
on a small set of operators with a clear semantics and should support
a typing discipline.
In a concurrency setting, such promises can be rather hard to achieve.
The class language is layered on top of the core objective calculus,
with a semantics that reduces classes into plain object definitions.
We thus retain strong static properties for all objects at runtime.
Some operators are imported from sequential languages and adapted to a
concurrent setting. For instance, multiple inheritance is expressed as
a disjunction of join definitions, but some disjunctions have no
counterpart in a sequential language.
In addition, we propose a new operator, called selective refinement.
Selective refinement applies to a parent class and rewrites the parent
reaction rules according to their synchronization patterns. Selective
refinement treats synchronization concretely, but it handles the parent
processes abstractly.
The design of our class language follows from common programming patterns in
the join calculus. We also illustrate this design by coding some standard
problematic examples that mix synchronization and inheritance.
Our approach to computing classes is compatible with the JoCaml
implementation of the join calculus [15], which
relies on runtime representation of synchronization patterns as
bitfields [16] and, on the contrary compiles
processes into functional closures. As a consequence, synchronization
patterns can be scanned and produced at runtime, while processes
cannot be scanned (but still can be produced), as required by our
operators on classes.
We then define a type system for objects and classes.
We introduce types at the end of the paper
only, to separate design issues and typing issues.
The type system improves on our previous work on polymorphism in the join
calculus [12].
As discussed in [12],
message synchronization potentially weakens polymorphism.
With classes, however, message synchronization may not be entirely
determined as we type partial definitions. In order to
preserve polymorphism, we thus rely on synchronization information in
class types.
In addition to standard safety properties, the type system enforces
privacy.
Indeed, the untyped objective join calculus lacks expressiveness as regards
encapsulation^{1}.
In order to restrict access to the internal state of objects,
we distinguish public and private labels. Then,
the type system guarantees that private labels are accessed only
from the body of a class used to create the object. The correctness
of the type system is established for an operational semantics
supplemented with privacy information.
As concern class operators, there is a tradeoff between expressiveness and
simplicity of both the static and dynamic semantics. In this paper, we favor
expressiveness, while preserving type soundness and compositionality
(with respect to compilation).
As a consequence, we get a better understanding of
inheritance and concurrency, and a
touchstone for other design choices.
Most of the complexity of our class operators stays within
selective refinement. However, selective refinement is often used in rather
simple patterns. This leaves place for simpler design choices
(some of them will be discussed in Section 5).
The paper is organized as follows.
In Section 2, we present the objective join calculus
and develop a few examples.
In Section 3, we supplement the language with classes
and give a rewriting semantics for the class language.
In Section 4
we present more involved examples of inheritance and concurrency.
In Section 5, we discuss other design choices.
In Section 6, we provide a static semantics for our
calculus and state its correctness.
In Section 7, we discuss related works and possible
extensions.
Appendix A presents
crossencodings between the plain and objective join calculus.
Appendix B gathers the main typing proofs.
2 
The objective join calculus 

We first focus on a core calculus dealing with objects.
This calculus is a variant of the join calculus [10].
We illustrate the operations of the calculus, then we define its
syntax and semantics.
The basic operation of our calculus is asynchronous message passing. For
instance, the process out.print_int(n)
sends a message with label print_int
and content n
to an object named out
, meant to print integers on the terminal.
Accordingly, the definition of an object describes how messages
received on some labels can trigger processes.
For instance,
obj continuation = reply(n) > out.print_int(n)
defines an object that reacts to messages on reply by
printing their content on the terminal.
Another example is the rendezvous, or synchronous buffer:
obj sbuffer = get(r) & put(n,s) > r.reply(n) & s.reply()
The object sbuffer has two labels get and
put; it reacts to the simultaneous presence of one
message on each of these labels by passing a message to the
continuation r, with label reply
and
content n, and passing an empty message to s.
(Object r may be the previouslydefined
continuation; object s is another continuation
taking no argument on reply.)
As regards the syntax, message synchronization and concurrent execution are
expressed in a symmetric manner, on either side of >, using the same
infix operator &.
Some labels may convey messages representing the internal state of an
object, rather than an external method call. This is the case of
label Some in the following unbounded, unordered,
asynchronous buffer:
obj abuffer =
put(n,r) > r.reply() & abuffer.Some(n)
or get(r) & Some(n) > r.reply(n)
The object abuffer can react in two different ways: a message
(n,r) on put may be consumed by storing the value
n in a selfinflicted message on Some;
alternatively, a message on get and a message on
Some may be jointly consumed, and then the value stored on
Some
is sent to the continuation received on get
. The
indirection through Some makes abuffer behave
asynchronously: messages on put
are never blocked, even if no
message is ever sent on get
.
In the example above, the messages on label Some encode the
state of abuffer. The following definition illustrates a
tighter management of state that implements a oneplace buffer:
obj buffer =
put(n,r) & Empty() > r.reply() & buffer.Some(n)
or get(r) & Some(n) > r.reply(n) & buffer.Empty()
init buffer.Empty()
Such a buffer can either be empty or contain one element. The state
is encoded as a message pending on Empty or Some,
respectively. Object buffer is created empty, by sending a
first message on Empty in the (optional)
init part of the
obj construct. As opposed to abuffer
above, a put
message
is blocked when the buffer is not empty.
To keep the buffer object consistent, there should be a single
message pending on either Empty or Some.
This invariant holds as long as external users cannot send messages on
these labels directly.
In Section 6, we describe a refined semantics and a type
system that distinguishes private labels (such as Empty and
Some) from public labels and restricts access to private
labels.
In the examples, private labels conventionally bear an initial capital
letter.
Once private labels are hidden, each of the three variants of buffer
provides the same interface to the outside world (two methods labeled
get and put) but their concurrent behaviors are very
different.
We use two disjoint countable sets of identifiers for object names x,
z, u Î O and labels l Î L. Tuples are
written x_{i}^{i Î I} or simply x.
The grammar of the objective join calculus (without classes)
is given in Figure 1; it has syntactic categories for
processes P, definitions D, and patterns M.
We abbreviate obj x = D \ init P_{1} in P_{2} by omitting init P_{1} when
P_{1} is 0.
Figure 1: Syntax for the core objective join calculus


P ::= 





Processes 







0 



null process 





x.M 



message sending 





P_{1} & P_{2} 



parallel composition 





obj x = D init P_{1} in P_{2} 



object definition 



D ::= 





Definitions 







M > P 



reaction rule 





D_{1} or D_{2} 



disjunction 



M ::= 





Patterns 







l(u) 



message 







M_{1} & M_{2} 



synchronization 


A reaction rule M > P associates a pattern M with a guarded
process P. Every message pattern l(u) in M binds the
object names u with scope P.
As in join calculus, we require that every pattern M guarding a reaction
rule be linear, that is, labels and names appear at most once in M.
In addition, the object definition obj x = D init P_{1} in
P_{2} binds the name x to D. The scope of x is
every guarded process in D (here x means ``self'') and the
processes P_{1} and P_{2}.
Free names in processes and definitions, written fn( · ),
are defined accordingly;
a formal definition of free names appears in Figure 4.
Terms are taken modulo renaming of bound
names (or aconversion).
The operational semantics is given as
a reflexive chemical abstract machine [10].
Each rewrite rule of the machine applies to configurations of objects and
processes, called chemical solutions. A solution D  P
consists of a set of named definitions D (representing objects in
solution) and of a multiset of
processes P running in parallel. We write x.D for a named definition
in D, and always assume that there is at most one definition for x in
D.
Chemical reductions are obtained by composing
rewrite rules of two kinds:
structural rules º represent the syntactical
rearrangement of terms; reduction rules ¾® represent
the basic computation steps.
Figure 2: Chemical semantics
Obj 
 obj x = D init P in Q
º x. D  P, Q 


Join 
 x.(M & M') º  x.M, x.M' 


Red 
x.[ M > P]  x.Ms
¾® x.[ M > P]  Ps 


Chemistry 
D_{0}  P_{1} º stackrel ¾® D_{0}  P_{2} 


D, D_{0}  P_{1}, P º stackrel ¾® D, D_{0}  P_{2}, P 


ChemistryObj 
 P º x.D  P' x Ïfn( D) È fn( P ) 


D  P , P º D , x.D  P' , P 



The rules for the objective join calculus are given in
Figure 2, with side conditions for rule Red:
[ M > P] abbreviates a
definition D that contains the reaction rule M > P;
s is a substitution with domain fn(M); the processes Ms
and Ps denote the results of applying s to M and P,
respectively.
Rules Par and Nil make parallel composition of
processes associative and commutative, with unit 0.
Rule Obj describes the introduction of an object.
(Preliminary aconversion may be required to pick a fresh name
x.)
Here, according to Obj and Par, expressions
obj x = D \ init P in Q and obj x = D in P & Q are
equivalent.
However, P and Q have different meaning in the semantics with
privacy, where Q cannot access private names of D (see Section 6.1).
Rule Join gathers messages sent to the same object.
Rule Red states how messages can be jointly
consumed and replaced by a copy of a guarded process, in which the
contents of these messages are substituted for the formal parameters
of the pattern.
In chemical semantics, each rule usually mentions only the
components that participate to the rewriting, while the rewriting
applies to every chemical solution that contains them.
More explicitly, we provide two context rules Chemistry
and ChemistryObj.
In rule Chemistry, the symbol º stackrel ¾®
stands for either º or ¾®.
In rule ChemistryObj,
the side condition x Ï fn( D)È fn( P) prevents name capture
when introducing new objects
(the sets fn( D) and fn( P) are defined in
Figure 4).
3 
Inheritance and concurrency 

We now extend the calculus of concurrent objects with classes
and inheritance.
The behavior of objects in the join calculus is statically defined:
once an object is created, it cannot be extended with new labels or
with new reaction rules synchronizing existing labels. Instead, we
provide this flexibility at the level of classes.
Our operators on classes can express various object paradigms, such
as method overriding (with late binding) or method extension. As
regards concurrency, these operators are also suitable to define
synchronization policies in a modular manner.
3.1 
Refining synchronization 

We introduce the syntax for classes in a series of simple examples.
We begin with a class buffer defining the oneplace buffer of
Section 2.1:
class buffer = self(z)
get(r) & Some(n) > r.reply(n) & z.Empty()
or put(n,r) & Empty() > r.reply() & z.Some(n)
As regards the syntax, the prefix
self(z) explicitly binds the name z
to
self. The class buffer can be used to create objects:
obj b = buffer init b.Empty()
Assume that, for debugging purposes, we want to log the buffer content
on the terminal. We first add an explicit log method:
class logged_buffer = self(z)
buffer
or log() & Some(n) > out.print_int(n) & z.Some(n)
or log() & Empty() > out.print_string("Empty") & z.Empty()
The class above is a disjunction of an inherited class and of
additional reaction rules.
The intended meaning of disjunction is that reaction rules are
cumulated, yielding competing behaviors for messages on labels
that appear in several disjuncts. The order of the disjuncts does not
matter.
The programmer who writes logged_buffer must have some
knowledge of the parent class buffer, namely the use of
private labels Some and Empty for representing the
state.
Some other useful debugging information is the synchronous
log of all messages that are consumed on put. This log
can be produced by selecting the patterns in which put occurs and
adding a
printing message to the corresponding guarded processes:
class logged_buffer_bis =
match buffer with
put(n,r) => put(n,r) > out.print_int(n)
end
The match construct can be understood by analogy with
pattern matching à la ML, applied to the reaction rules of
the parent class.
In this example, every reaction rule from the parent buffer
whose synchronization pattern contains the label put is
replaced in the derived logged_buffer_bis by a rule with
the same synchronization pattern (since put appears on both
sides of Þ) and with the original guarded process in
parallel with the new printing message (the original guarded process
is left implicit in the match syntax). Every
other parent rule is kept unchanged. Hence, the class above
behaves as the definition:
class logged_buffer_bis = self(z)
get(r) & Some(n) > r.reply(n) & z.Empty()
or put(n,r) & Empty() > r.reply() & z.Some(n) & out.print_int(n)
Yet another kind of debugging information is a log of put
attempts:
class logged_buffer_ter = self(z)
match buffer with
put(n,r) => Parent_put(n,r) > nil
end
or put(n,r) > out.print_int(n) & z.Parent_put(n,r)
In this case, the match construct performs a renaming of
put into Parent_put in every pattern of class
buffer, without affecting their guarded processes.
The overall effect is similar to the overriding of the method put
of buffer
with a latebinding semantics.
Namely, should there be a message z.put(u) in a guarded process
of the parent class, then, at runtime, z.put(u) would reach the new
definition of put.
The examples above illustrate that the very idea of class refinement
is less abstract in a concurrent setting than in a sequential one. In
the first logged_buffer example, logging the buffer state
requires knowledge of how this state is encoded; otherwise, some states
might be forgotten or logging might lead the buffer into
deadlock. The other two examples expose another subtlety: in a
sequential language, the distinction between logging put
attempts and put successes is irrelevant.
Thinking in terms of sequential object invocations, one may be unaware
of the concurrent behavior of the object, and thus write
logged_buffer_ter instead of logged_buffer_bis.
The language with classes extends the core calculus of
Section 2; its grammar is given in
Figure 3.
We refer to
Sections 2.1, 3.1,
and 4 for explanations and examples.
Classes are taken up to the associativecommutative laws for
disjunction.
We use two additional sets of identifiers for class names c Î
C and for sets of labels L Î 2^{ L}. Such sets L are
used to represent abstract classes that declare the labels in L but
do not necessarily define them.
Figure 3: Syntax for the objective join calculus


P ::= 





Processes 







0 



null process 





x.M 



message sending 





P_{1} & P_{2} 



parallel composition 





obj x = C init P_{1} in P_{2} 



object definition 





class c = C in P 



class definition 



C ::= 





Classes 







c 



class variable 







L 



abstract class 







J > P 



reaction rule 





C_{1} or C_{2} 



disjunction 





self(x) C 



self binding 





match C with S end 



selective refinement 



S ::= 





Refinement clauses 







(K_{1} Þ K_{2} > P)  S 



refinement sequence 





Ø 



empty refinement 



J ::= 





Join patterns 







l(u) 



message 







J_{1} & J_{2} 



synchronization 







J_{1} or J_{2} 



alternative 





K ::= 





Selection patterns 







0 



empty pattern 







J 



join pattern 


Join patterns J generalize the syntactic category of patterns M
given in Figure 1 with an or operator that
represents alternative synchronization patterns.
Selection patterns K are either join patterns or the empty
pattern 0.
All patterns are taken up to equivalence laws:
& and or are associativecommutative, & distributes over or,
and 0 is the unit for &.
Hence, every pattern K can be written as an
alternative of patterns or_{i Î I} M_{i}. We sometimes use the notation K_{1} & K_{2} for decomposing patterns
M.
Figure 4: Free names fn(·) and declared labels dl(·)
In patterns M, join patterns J, and selection patterns K: 


fn(0) 

= 
Ø 



fn( l(u)) 

= 
u 



fn( J & J' ) 

= 
fn( J ) È fn( J' ) 



fn( J or J' ) 

= 
fn( J )
(also = fn( J' )) 



dl(0) 

= 
Ø 



dl( l(u) ) 

= 
{ l } 



dl( J & J' ) 

= 
dl( J ) + dl( J' ) 



dl( J or J' ) 

= 
dl( J ) È dl( J' ) 

In refinement clauses S: 


fn(^{i Î I} (K_{i} Þ K_{i}' > P_{i})) 

= 
È_{i Î I} fn(P_{i}) \ fn(K_{i}') 



dl(^{i Î I} (K_{i} Þ K_{i}' > P_{i})) 

= 
È_{i Î I} dl(K_{i}') \ dl(K_{i}) 

In classes C: 


fn( c ) 

= 
{ c } 



fn( L ) 

= 
Ø 



fn( J > P) 

= 
fn( P ) \ fn( J ) 



fn( C_{1} or C_{2} ) 

= 
fn(C_{1}) È fn(C_{2}) 



fn( self(z) C ) 

= 
fn(C) \ { z } 



fn( match C with S end ) 

= 
fn(C) È fn(S) 



dl( c ) 

= 
Ø 



dl( L ) 

= 
L 



dl( J > P ) 

= 
dl( J ) 



dl( C_{1} or C_{2} ) 

= 
dl( C_{1} ) È dl( C_{2}) 



dl( self(z) C ) 

= 
dl( C ) 



dl( match C with S end ) 

= 
dl(C) È dl(S) 

In processes P: 


fn( 0 ) 

= 
Ø 



fn( x. M ) 

= 
{x} È fn(M) 



fn( P & Q ) 

= 
fn(P) È fn(Q) 



fn( obj x = C init P in Q ) 

= 
(fn(C) È fn(P) È fn(Q)) \ { x } 



fn( class c = C in P ) 

= 
fn(C) È (fn(P) \ { c }) 

In solutions: 


fn( D ) 

= 
È_{x.D Î D} ({x} È fn(D)) 



fn( P ) 

= 
È_{P Î P} fn(P) 


We always assume that processes meet the following
wellformedness conditions:
 All conjuncts M_{i} in the normal form of K are linear
(as defined in Section 2.2) and binds the same names
(i.e. have the same set of free names, as defined in Figure 4). By extension, we say that K binds the names fn(M_{i})
bound in each M_{i}, and write fn(K) for these names.
 In a refinement clause K_{1} Þ K_{2} > P, the pattern K_{1}
is either M or 0, the pattern K_{2} binds at least the
names of K_{1} (fn(K_{1})Í fn(K_{2})), and
K_{1} is empty whenever K_{2} is empty
(so as to avoid the generation of empty patterns).
Binders for object names
include object definitions (binding the defined object) and
patterns (binding the received names).
In a reaction rule J > P, the join pattern
J binds fn(J) with scope P.
In a refinement clause K_{1} Þ K_{2} > P, the selection pattern
K_{1} binds fn(K_{1}) with scope K_{2} and P; the modification
pattern K_{2} binds fn(K_{2})\ fn(K_{1}) with scope P.
Finally, self(x) C binds the object name x to the receiver (self) with
scope C.
Class definitions class c = C in P are the only binders for class
names c, with scope P.
The scoping rules appear in Figure 4; as usual,
+ means disjoint union.
Processes, classes, and reaction rules are taken up to
aconversion.
Labels don't have scopes.
Labels declared in patterns and classes, written dl(K) and dl(C),
are specified in Figure 4. We say that a label is
declared but undefined when it is declared only in abstract classes.
3.3 
Rewriting semantics of the class language 

Figure 5: Rewriting semantics of the class language
Rules for processes ( ® )
ClassRed 


obj x = C init P in P'
® obj x = C' init P in P' 


Rules for classes ( ^{x}® )
Self 
self(z) C ^{x}® C {^{x}/_{z}} 


OrPat 
J or J' > P ^{x}® J > P or J' > P 


Match 
C with S ® C' dl(S) Í dl(C') 


match C with S end ^{x}® C' 



Evaluation contexts for classes
E{·} ::= {·} 
match E{·} with S end  E{·} or C  C or E{·}
Rules for filters ( ® )
to 0em (Side conditions in the text)
1em 
FilterApply 
K_{1} & K > P with K_{1} Þ K_{2} > Q  S
®
K_{2} & K > P & Q or dl(K_{1}) \ dl(K_{2}) 


FilterNext 
M > P with S 

C'
dl(K_{1}) ¬ Ídl(M) 



M > P with K_{1} Þ K_{2} > Q  S


C' 




FilterOr 
C_{1} with S ® C_{1}' C_{2} with S ® C_{2}' 


(C_{1} or C_{2}) with S ® C_{1}' or C_{2}' 



The semantics of classes is defined by reduction to the core calculus.
The rules are given in Figure 5. Rules ClassSubst and ClassRed describe class rewritings for
processes. Rule ClassRed lifts an auxiliary reduction on
classes ^{x}® to processes. This auxiliary reduction
is parameterized by the name of the object and replaces
the (outermost) self names with the reduction parameter.
Rule Self removes inner bindings for the name of self.
Rule OrPat lifts or constructs from patterns to classes.
The next two rules for classes simplify abstract classes,
rule ClassAbstract discards empty abstract classes;
rule AbstractCut discards abstract labels that are declared elsewhere.
Rule Match reduces selective refinements
match C with S end by means of an auxiliary relations, described below.
Rule ClassContext applies rewriting under disjunctions and
selective refinements.
The auxiliary reduction ® computes filters of the form C with S.
Every reaction rule M > P in C is rewritten according to the leftmost
clause of S that matches M, that is, whose selection pattern K
is a subpattern of M (rules FilterNext and
FilterApply). If no clause of S matches M, then the
reaction rule is left unchanged (rule FilterEnd).
Abstract classes L in C are also left unchanged
(rule FilterAbstract).
Note that rule FilterApply can be used only if the pattern K_{2} & K introduced by rule
FilterApply is wellformed, i.e.,
(1) K_{2} and K are not both empty,
(2) fn(K_{2}) Ç fn(K) = Ø, and
(3) dl(K_{2}) Ç dl(K)= Ø.
Condition (1) is enforced by syntactic restriction
2 of Section 3.2.
Condition (2) can be enforced by aconversion.
Condition (3) will be checked by the type system.
The rewriting C with S ® C' may erase every reaction rule
defining a label of C. Specifically, rule FilterApply
removes the labels dl(K_{1}) \ dl(K_{2}). To prevent those
labels from being undeclared in C', rule FilterApply
records them as abstract labels.
The type system of Section 6 will compute an approximation
of abstract names to statically ensures that every erased label is
actually redefined before the class is instantiated.
Conversely, the rewriting C with S ® C' may introduce labels in C' that
are undeclared in C. Specifically, rule FilterApply
introduces the labels dl(K_{2}) \ dl(K_{1}).
The set dl(S) defined in Figure 4 statically collects all such labels.
However, some clauses of S may not be used, hence some label of dl(S) may not
be declared in C'.
This situation often corresponds to a programming error. To prevent
it, we supplement rule Match with the premise dl(S) Í
dl(C') that blocks the rule, and we interpret this situation as a
dynamic refinement error.
Next, we summarize the outcome of class reduction for processes.
One can easily check that the rewriting semantics is deterministic and
always terminates.
Using rule ClassSubst, any class construct can be eliminated, so
we focus on object creations:
Lemma 1 [Rewriting]
Let P be a process of the form obj x = C init Q in Q' such that
rule ClassRed does not apply to P. One of the following holds:

Completion:
 C is a disjunction of reaction rules
(C = or_{i = 1}^{n} M_{i} > P_{i}).
 Failure:
 For some evaluation context E, we have:

C = E{c} and c is free (undefined class).
 C = E{L} and L is not under a
match (undefined label).
 Refinement error:
 C contains a blocked refinement in evaluation
context:
C = E { match C' with S end}, C' with S ® C'',
and dl(S) ¬ Ídl(C'').
The distinction between failures and refinement errors matters only in the
typed semantics, which prevents all failures but not necessarily
refinement errors.
Like in Section 2, we call ``definition'' and write D
instead of C for any class of the form given in the Completion case.
3.4 
Implementation issues 

In order to compile disjunctions and selective refinements, one
must access the patterns of parent classes. This hinders the abstract
compilation of patterns, but does not otherwise preclude separate
compilation.
As in a functional setting, the guarded processes attached to
individual reaction rules can be immediately compiled into closures
abstracted with respect to their free names, including formal message
parameters.
This approach is compatible with the JoCaml implementation, which
keeps a concrete representation of join patterns as vectors of bits;
the control of the synchronization of messages and the activation of
guarded processes is then realized by interpreting these bit vectors at
runtime [16].
In an implementation of the object calculus with classes, such vectors
of bits would serve as a basis of a data structure for representing classes
at runtime.
In the core objective join calculus, patterns do not contain
alternatives `` or''. To eliminate them, rule OrPat
duplicates reaction rules whose patterns contain alternatives.
Alternatively, we could have supplemented the object calculus with
orpatterns, but we view this as an optimization issue.
Perhaps more importantly, the unsharing of reaction rules
performed by rule OrPat
does not mean that guarded processes are duplicated by the compiler.
Since guarded processes are compiled as closures, duplicating P in
the semantics means duplicating an indirection to the closure that
implements P.
4 
Solving challenging examples 

As remarked by many authors, the classical point of view on class
abstractionmethod names and signatures are known, method bodies are
abstractdoes not mix well with concurrency.
More specifically, the signature of a parent class does not usually
convey any information on its synchronization behavior. As a result,
it is often awkward, or even impossible, to refine a concurrent
behavior using inheritance.
(More conservatively, objectoriented languages with plain concurrent
extensions usually require that the synchronization properties be
invariant through inheritance, e.g., that all method calls be
synchronized. This strongly constrains the use of concurrency.)
This wellknown problem is often referred to as the inheritance
anomaly.
Unfortunately, inheritance anomaly is not defined formally, but by
means of problematic examples.
In [18] for instance, Matsuoka and Yonezawa
identify three patterns of inheritance anomaly.
For each pattern, they propose a refinement of the class language that
suffices to express the particular synchronization property at hand:
they identify the parts of the code that control synchronization in
the parent class (which are otherwise hidden in the body of the
inherited methods); they express this ``concurrency control'' in the
interface of the class; and they rely on the extended interface to
refine synchronization in the definition of subclasses.
In principle, it should be possible to fix any particular anomaly by
enriching the class language in an ad hoc manner. However, the overall
benefits of this approach are unclear.
Our approach is rather different: we start from a core calculus of
concurrency, rather than programming examples, and we are primarily
concerned with the semantics of our inheritance operators.
Tackling the three patterns of inheritance anomaly
of [18], as we do in this section, appears to be a
valuable test of our design. Indeed, the issue of inheritance anomaly is
out of the scope of this paper. We refer to other studies, such as [20], for analyses of this issue, which,
however, concern different and untyped frameworks.
We consider the same running example as Matsuoka and Yonezawa: a FIFO
buffer with two methods put and get to store and
retrieve items. We also adopt their taxonomy of inheritance anomaly:
inheritance induces desirable modifications of ``acceptable states''
[of objects], and a solution is a way to express these modifications.
In the following examples, we use a language extended with basic datatypes.
Booleans and integers are equipped with their usual operations.
Arrays are created by create(n)
, which gives an
uninitialized array of size n
. The size of an
array A is given by A.size
.
Finally, the array A[i] < v
is
obtained from A
by overwriting its ith entry with
value v.
The FIFO buffer of [18] can then be written as follows:
class buff = self (z)
put(v,r) & (Empty(A, i, n) or Some(A, i, n)) >
r.reply() & z.Check(A[(i+n) mod A.size] < v, i, n+1)
or get(r) & (Full(A, i, n) or Some(A, i, n)) >
r.reply(A[i]) & z.Check(A, (i+1) mod A.size, n1)
or Check(A,i,n) >
if n = A.size then z.Full(A, i, n)
else if n = 0 then z.Empty(A, i, n)
else z.Some(A, i, n)
or Init(size) > z.Empty(create(size), 0, 0)
The state of the buffer is encoding a circular array represented
by a message with label Empty,
Some, or Full.
These labels carry three arguments. The first one, A is the array;
the second one, i is the index of the first element of the buffer;
the third one, n is the number of elements in the buffer.
The buffer may react to messages on put when nonfull, and to
messages on get when nonempty; this is expressed in a concise
manner using the
or operator in patterns.
Once a request is accepted, the state of the buffer is recomputed by
sending an internal message on Check. Since Check
appears alone in a join pattern, message sending on Check
acts like a function call.
Partitioning of acceptable states.
The class buff2
supplements buff
with a new method
get2
that atomically retrieves two items from the buffer.
For simplicity, we assume size
> 2.
Since get2 succeeds when the buffer contains two elements or
more, the buffer state needs to be refined. Furthermore, since for
instance a successful get2 may disable get or
enable put, the addition of get2 has an impact on
the ``acceptable states'' of methods get and put,
which are inherited from the parent buff. Therefore, label
Some is not detailed enough and is replaced with two labels
One and Many. One represents a state with
exactly one item in the buffer; Many
represents a state with two
items or more in the buffer.
class buff2 = self(z)
get2(r) & (Full(A,i,n) or Many(A, i, n)) >
r.reply(A[i], A[(i+1) mod A.size])
& z.Check(A, (i+2) mod A.size, n2)
or match buff with
Some(A, i, n) => (One(A, i, n) or Many(A, i, n)) > nil
end
or Some(A, i, n) >
if n > 1 then z.Many(A, i, n) else z.One(A, i, n)
In the program above, a new method get2 is defined, with its
own synchronization condition.
The new reaction rule is cumulated with those of buff, using
a selective refinement that substitutes ``One(...) or
Many(...)'' for every occurrence of
``Some(...)'' in a join pattern.
The refinement eliminates Some from any inherited pattern,
but it does not affect occurrences of Some in inherited
guarded processes: the parent code is handled abstractly, so it cannot
be modified.
Instead, the new class provides an adapter rule that consumes any
message on Some and issues a message on either One
or Many, depending on the value of n.
Historydependent acceptable states.
The class gget_buff alters buff as follows: the new
method gget returns one item from the buffer (like
get), except that a request on gget can be served
only immediately after serving a request on put. More
precisely, a put transition enables gget, while
get and gget transitions disable it. This condition
is reflected in the code by introducing two labels AfterPut
and NotAfterPut. Then, messages on gget are
synchronized with messages on AfterPut.
class gget_buff = self (z)
gget(r) & AfterPut() & (Full(A, i, n) or Some(A, i, n)) >
r.reply(A[i]) & z.NotAfterPut()
& z.Check(A, (i+1) mod A.size, n1)
or match buff with
Init(size) => Init(size) > z.NotAfterPut()
 put(v, r) =>
put(v, r) & (AfterPut() or NotAfterPut()) > z.AfterPut()
 get(r) =>
get(r) & (AfterPut() or NotAfterPut()) > z.NotAfterPut()
end
The first clause in the match construct refines initialization,
which now also issues a message on NotAfterPut. The two other
clauses refine the existing methods put and get,
which now consume any message on AfterPut or
NotAfterPut and produce a message on AfterPut
or NotAfterPut, respectively.
Modification of acceptable states.
We first define a generalpurpose lock with the following locker class:
class locker = self (z)
suspend(r) & Free() > r.reply() & z.Locked()
or resume(r) & Locked() > r.reply() & z.Free()
This class can be used to create locks, but it can also
be combined with some other class such as buff to temporarily prevent message
processing in buff.
To this end, a simple disjunction of buff and locker is
not enough and some refinement of the parent class buff is required:
class locked_buff = self (z)
locker
or match buff with
Init(size) => Init(size) > z.Free()
 nil => Free() > z.Free()
end
The first clause in the match construct supplements the
initialization of buff with an initial Free message
for the lock.
The second clause matches every other rule of buff, and
requires that the refined clause consume and produce a message on
Free.
(The semantics of clause selection follows the textual priority scheme
of ML patternmatching, where a clause applies to all reaction rules
that are not selected by previous clauses, and where the empty
selection pattern acts as a default case.)
As a consequence of these changes, parent rules are blocked between a
call to suspend and the next call to resume, and
parent rules leave the state of the lock unchanged.
In contrast with previous examples, the code above is quite general;
it applies to any class following the same convention as buff
for initialization.
Further anomalies
Dealing with the examples above does not mean that we solved the
inheritance anomaly problem. Indeed, most limitations of
expressiveness can be interpreted as inheritance anomalies. We
conclude this section with a more difficult example, for which we
only have a partial solution. The difficulty arises when we try to
delegate privileged access to an object.
Consider a class with some mutable state, such as the oneplace buffer
of Section 3.1:
class buffer = self(z)
get(r) & Some(n) > r.reply(n) & z.Empty()
or put(n,r) & Empty() > r.reply() & z.Some(n)
We want to supplement buffer
with an incr
method that
increments the buffer content. One might also require
incr
to be performed by using get
and put
from another object server
:
obj server =
do_incr(x,r) > obj s = reply(n) > x.put(n+1,r) in x.get(s)
Furthermore, we require that the call to put
from inside
do_incr
never block. Thus, any other call to put
should
be blocked during the execution of do_incr
.
To enforce this partial exclusion, we introduce an Exclusive
flag,
we take two copies of the parent class, and we specialize their
definitions of put
for external calls (disallowed during
an increment) and privileged calls (performed only from the
server). In the latter refinement clause, the
conflicting method put
is renamed to Put_priv
, and a
``proxy object'' that forwards
put
calls to Put_priv
is passed to the server.
class counter = self(z)
match buffer with
put(n,r) => put(n,r) & Exclusive() > z.Exclusive()
end
or match buffer with
put(n,r) => Put_priv(n,r) > nil
end
or incr(r) & Exclusive() >
obj s = reply() > r.reply() & z.Exclusive() in
obj proxy = get(r) > z.get(r)
or put(n,r) > z.Put_priv(n,r) in
server.do_incr(proxy,s)
or Init() > z.Empty() & z.Exclusive()
Our solution is not entirely satisfactory. In particular, the
duplication of method put
forces further refinements of counter
to treat the two methods put
and Put_priv
in a consistent
manner.
For instance, if we refine counter
in order to
log successful puts, as we do in example logged_buffer_bis
of Section 3.1, then the puts from server
are not logged.
We can improve this by keeping a single copy of put
the private
one and make the public method pub
synchronously forwarding its
call to the private version (synchrony is required to ensure that
the Exclusive
lock is only released when the forwarded call to the
private version of put
has returned.)
class counter = self(z)
match buffer with
put(n,r) => Put_priv(n,r) > nil
end
or put(n,r) & Exclusive() >
obj s = reply(x) > r.reply(x) & z.Exclusive() in
z.Put_priv(n,s)
or incr(r) & Exclusive() >
obj s = reply() > r.reply() & z.Exclusive() in
obj proxy = get(r) > z.get(r)
or put(n,r) > z.Put_priv(n,r) in
server.do_incr(proxy,s)
or Init() > z.Empty() & z.Exclusive()
The class can not be inherited as long as the clients operates on
the private version Put_private
instead of the public name put
that is just used as an entry point.
A more elegant approach is to stick to views in the style of [27, 30].
A view is a map from method names to method slots. Method slots are
positions for method implementations in a class, which are
used for selfreferencing other methods of the same object.
Overriding of a method amounts to change the method implementation,
thus affecting the other methods that reference the overridden
method slot. Overriding must preserve method slot types.
Therefore method slots
cannot be hidden in classes, since otherwise, they could be redefined
with another incompatible type.
On the contrary, a method name can be safely erased from a view,
leaving its slot unreachable (in that view). A
later redefinition of the same name will simply allocate a new unrelated
slot.
In the traditional approachthe one that we followednames and slots are
in a onetoone correspondence. Hence, methods cannot be forgotten in
classes (they can only become abstract and will have to be redefined later
before taking an instance of the class).
Views are a much more powerful mechanism, but they require a significant
complication of the type system.
5 
Variations on the class language 

Our language of classes favor expressiveness while retaining type soundness
and modularity. Thus, several other design choices, which could allow
significant simplifications or enforce stronger invariants, can be derived
from our proposal either by small variations or restrictions.
5.1 
Object initialization 

Usually, object initialization is defined at the class level, rather than at
the object level, which is hidden to users. Instead, in our proposal
objects are visible because they provide the basic semantics.
Regarding the object initialization, we enriched the object language
as little as needed by splitting names into private and public. Hereafter,
we illustrate a more standard approach to object initialization by means
of straightforward translation of a higherlevel language. (Indeed,
examples of Section 4 conform with this approach.)
In the userlanguage we replace class
and obj
declarations by
the following ones:
 Class definitions are written
class c(x) = I C in P where
the name c of the class takes a list of arguments (x);
 I is a list of inheritance clauses of the form
( inherits c_{i}(u_{i}) as d_{i})^{ i Î I} where
each c_{i} is a previsouly defined class and
d_{i} a local name for the body of c_{i}.
 C is as before, except that it contains exactly one rule of the form
c^{init}(x)> Q.
The names c^{init} are private and special in the sense that they cannot
occur (in the userlanguage) anywhere else. Indeed, c^{init} play the role
of class constructors.
 P is as before.
 Object definitions are written obj x = c(u) in P where c has been
defined as above.
The translation of the above declarations are, respectively:
 class c(x) =
match C with c^{init}(x) Þ
c^{init}(x) &^{i Î I} c_{i}^{init} (u_{i})
end
in P
 obj x = c \ init c^{init}(u) in P.
In this user language, the class is responsible for object initialization.
Moreover, by constructions, subclasses always invoke the initialization
methods of its parent classes.
Indeed, other design choices are possible. For instance, this design
easily generalizes to allow multiple class constructors.
5.2 
Restriction of selective refinements 

The examples in Section 4 only use selective
refinement in a restrictive and simple form. In particular, refinement
clauses K Þ K' > P always uses K with 0 or 1 message.
Restricting to such cases simplifies rule FilterApply in the
rewriting semantics (Figure 5) and the static semantics of
classes given below in Section 10.
A different approach has been taken in Polyphonic C [3].
This language extends C with reaction rules a la join
calculus (called chords).
As inheritance is concerned, Polyphonic C is quite severe with respect
to join patterns: if a method is overridden, then all join patterns
concerning that method must be overridden, and so on, transitively.
This apporach is significantly different than ours. In particular, while we
allow overriding of as few methods as possible during inheritance, they
instead require overriding of too many methods. For instance, in the
common pattern where every method synchronizes with a global object state,
overriding any method would require overriding all of them.
The static semantics of our calculus extends those of the core
join calculus for concurrency and
synchronization [12] and of OCaml for
the classlayer [26], respectively.
As regards polymorphism, the type system supports ML parametric polymorphism
and uses row variables to enable some form of
subtyping [32, 26].
It also improves on [12],
so as to match at least the implementation [15]
and avoid the limitation pointed out in [24].
As regards classes, we supplement the typing
of [26] in order to deal with the new operator of
selective refinement and to collect some synchronization information.
6.1 
A semantics with privacy 

In this section, we specify the dynamic errors that are detected by
typing.
For instance, the type system detects messagenotunderstood
errors: no message can be sent to an object with a label that is
undefined at that object. (Of course, the type system does not ensure
any processing of messages.)
In addition, the type system enforces object encapsulation; this is
stated for a chemical semantics extended with a notion of privacy.
We partition labels l Î L into
private labels f Î F and
public labels m Î M.
Informally, a message on a private label can only be sent
internally, that is, from within either a reaction rule or the init
part of the object.
Conversely, a message on a public label can be sent from any context
that has access to the object name.
However, the origin of a message is a static notion, which is not
preserved in the original chemical semantics given in
Section 2.
For instance, rule Obj in Figure 2,
used to create new
objects, immediately mixes its privileged init process with all
other running processes.
In order to express subject reduction and type safety with privacy, we
thus supplement our chemical semantics with privacy annotations at runtime.
In the state of the refined machine, every running process P and
active definition D is prefixed by a string of object
names y that records the nesting of objects. Precisely, the
string y_{1}... y_{n} x indicates that object x was created
within the definition (or the init process) of objects y_{1}, ...,
y_{n} and thereby can access their private labels.
The chemical state, or solution, is written D  P. It
consists of a set D of prefixed definitions y x # D
and a multiset of prefixed processes y # P.
A solution is wellformed when all prefixes agree on object nesting,
i.e., if y x and j x appear in prefixes, then y =
j. As before, we also assume that there is a single definition
for every object in the solution. These properties are preserved by
chemical rewriting.
We use the rules of Figure 6, with the following
side conditions: for Obj, D is a definition, i.e., a class of
the form or_{i = 1}^{n} M_{i} > P_{i}; for Red, [ M >
P] abbreviates a definition that contains the rule M > P and
s is a substitution on the names bound in M.
Except for the bookkeeping on static environments, rules Nil,
Par, Join, Obj, Red,
Chemistry, and ChemistryObj are the same as in
Section 2.
Note that Red consumes only messages with a prefix that matches
the object definition, and triggers a process in the same environment
as the object definition.
Since messages can be sent from other objects, an intermediate routing step is called for. Such steps are modeled by rules
PublicComm and PrivateComm that carry messages from
their emitter to their receiver.
This semantics is a refinement of the previous semantics. (Formally,
every reduction in this semantics can be mapped into zero or one
reduction in the previous semantics after removing all prefixes.)
Figure 6: Chemical semantics with privacy

Par 
 y # (P & Q)
º  y # P, y # Q 



Join 
 y # x.(M & M')
º  y # x.M, y # x.M' 


Obj 
 y # obj x = D init P in Q
º y x # D  y x # P, y # Q 


PublicComm 
y x # D  y' # x. m(u)
¾® y x # D  y x # x. m(u) 


PrivateComm 
y x # D  y x y' # x. f(u)
¾® y x # D  y x # x. f(u) 


Red 
y x # [ M > P]  y x # x.(Ms)
¾® y x # [ M > P]  y x # (Ps) 


Chemistry 
D_{0}  P_{1} º stackrel ¾® D_{0}  P_{2} 


D, D_{0}  P_{1}, P º stackrel ¾® D, D_{0}  P_{2}, P 


ChemistryObj 
 P º y x # D  P' x Ïfn( D) È fn( P ) 


D  P , P º D , y x # D  P' , P 



Our privacy policy states that a message sent from object y to
object x on a private label is valid as long as y has been created
by a process of x (cf. rule PrivateComm). We take the
presence of
nonroutable messages as our definition of a privacy error.
We also give a formal definitions for other errors, which do not
depend on privacy information.
Definition 1
A solution D  P fails
when one of the following holds:
 Free variables:
 the solution contains a free class variable, or
a free object name that is not defined in D.
 Runtime Failure:

for some y #
x.l(u) Î P and y'x # D Î D, we have

Failed privacy:
l Î F and y' is not a prefix of
y.
 Undeclared label:
l Ïdl(D).
 Arity mismatch:
l(y) appears in a pattern of D with different arities for
y and u.
 Class rewriting failure:

for some y # P Î P, the process P is a failure, as defined
in Lemma 1 of Section 3.3.
Figure 7: Syntax for type expressions

t 
::= 
q  [ r ] 

Object types 
r 
::= 
Ø  h  m : t; r 

Row types 
s 
::= 
" X. t 

Type schemes 
a 
::= 
q  h 

Variables 
t 
::= 
(t_{i}^{i Î I}) 

Tuple types 
B 
::= 
Ø  l : t; B 

Internal types 


The grammar for type expressions is given in Figure 7.
We build types out of a countable set of type variables, ranged over
by q and a countable set of row variables, ranged over by h.
In the sequel, we write a for variables, regardless of their kinds, and
g for either object types t or row types r. We write X and Y
for sets of type variables. We also abbreviate type schemes " Ø. t
as t.
Object types [r] collect the types of public labels.
For instance the type of the object continuation from
Section 2.1
is [reply:(int)].
Object types may end with a
row variable (open object types), as in
OCaml [26].
For instance, consider a simple rendezvous object join, with
an internal counter:
obj join = sync1(r1) & sync2(r2) & Count(x) >
r1.reply() & r2.reply() & join.Count(x+1)
The type of the object join is [sync1 : ([reply
: (); h]); sync2 : ([reply : (); h'])], telling that the
sync labels accept messages composed of any object with a
reply label which in turn accepts empty messages. We assumed that
the label Count is private, hence it does not appear in the type
of join.
Internal types B are used to describe both public and private labels. Such
internal types appear in class types (see below). They are also used to
describe the internal type of self while typechecking class bodies where
sending messages on private names is
allowed (Section 6.4). We observe that B is a
partial function from labels to tuple types; therefore we will address types
of labels by function application.
We use the following standard notations. The operator l : _;
_ associates to the left. We often skip the trailing Ø,
i.e. we abbreviate l_{1} : t_{1}; ... l_{n} : t_{n}; Ø by
l_{1} : t_{1}; ... l_{n} : t_{n} and we abstract away from the
order of labels l_{1},... l_{n}.
For a given set of labels L, we write B  L for the
restriction of B to the labels of L.
We also write B_{1} Å B_{2} for the union of B_{1} and B_{2}, with
the statement that B_{1} and B_{2} coincide on their common labels,
and state B_{1} Í B_{2} when there is B_{1}' such that B_{1}
Å B_{1}' = B_{2}. We write dom(B) for the set of labels listed in B.
Class types have the form " X. z(r)B^{W,V}.
The set X collects all object type variables and row type variables
appearing in r or B that are polymorphic.
The row type r collects all the constraints on the type [r] of
self, i.e. an object of the class being defined. (These constraints
originate from recursive calls, and also from passing self as a
parameter in messages.)
The internal type B lists the types for
all public and private labels declared in the class.
The consistency between r and B is checked only when objects are
created.
The set W collects the coupled labels of the class,
as explained below.
The set V Í dom(B) contains labels that are declared but
undefined; we call these labels ``virtual labels''; classes with
virtual labels cannot be instantiated.
Given the sophistication of class types, we delay the presentation of
a complete example until section 6.7. However,
if the previous definition of the join object is lifted into
a class definition, then the B component of its type is
sync1 : ([reply : (); h]); sync2 :
([reply : (); h']); Count : (int), there are no
virtual nor coupled labels, and both variables h and h' can be
made polymorphic. Moreover, the internal type for the
objet join should also contain Count : (int).
6.3 
Polymorphism and inheritance 

We now discuss the interaction between synchronization, inheritance,
and polymorphism, in order to define the generalization conditions for
type variables. (The reader not interested in polymorphism may skip
these definitions and their usage in the type system.)
In contrast with functional method types, the types of messages sent
on labels appearing in the same pattern must agree on the
instantiation of any shared type variables.
Consider, for instance, the sbuffer of
Section 2.1:
obj sbuffer = get(r) & put(n,s) > r.reply(n) & s.reply()
The types of get and put are ([ reply : (q);
h]) and (q, [ reply : (); h']), respectively.
In order to retain type consistency for messages on r.reply
, the
two occurrences of q in get
and put
must be
instantiated to the same type. Hence, variable q cannot be generalized.
Conversely, type variables h and h' appearing in the type
of a single method can be generalized; this is the main source of
polymorphism in the objective join calculus^{2}.
We introduce auxiliary definitions to capture the sharing of messages
and type variables in patterns.
Let K be a pattern. The pattern é Kù is obtained from K by
erasing every message that carries an empty tuple.
The set of coupled labels of K, written cl(K),
collects the
labels whose contents are effectively synchronized in K: we let cl(M) = dl(é Mù) when the pattern é Mù contains at least two
messages, and cl(M) = Ø otherwise.
For more complex patterns of the form K = or_{i Î I} M_{i},
we let cl(K) = È_{iÎ I} cl(M_{i}).
Similarly for types, é Bù is obtained from B by removing every
label with an empty tuple type.
We write ftv(_) for the the set of free type variables occurring
in a type, a tuple type, a type scheme, or a typing environment
(defined in Section 6.4).
We let ctv(B) be the subset of type variables in ftv(B) that occur
in at least two labeled entries of B:
ctv 
(B) =


ftv(B(l)) Ç ftv(B(l'))

Assuming that B gathers the types for all messages that can be
sent to an object, the set ctv(B) contains any variable that
cannot be generalized because of synchronization, independently of the
patterns for that object.
When the synchronization patterns are known, however, one can usually
compute a smaller set of such variables.
Since objects and classes can refine other classes, we compute a safe
approximation of nongeneralizable variables in contexts where the
patterns for the objects are still unsettled.
To this end, the type of each class carries a set W of coupled labels, such that cl(J) Í W for all patterns
J that may appear in an object of a class of that type.
Eventually, the typing rule for object definition will generalize all
type variables except those that appear in ctv(B  W) ,
where B gathers the types for all messages of the object and W
collects all potentiallycoupled labels.^{3}
The main issue is to compute the coupled labels for a refined class, of the
form match C with S end.
Instead of the patterns for C, we only know B and W from its
class type. Since the refinement may leave unchanged some rules of
C, the refined class retains at least the coupled labels of W.
In addition, for every filter K Þ K' > P of S, some
labels may become coupled as the filter matches a pattern K & K''
in C (for some K'') and produces a rule with
pattern K' & K''.
By definition of cl(_), the new coupled labels are:
cl( K' & K'' ) 
= 
cl(K')
È cl(K'')
È 
ì
í
î 
Ø when é K'ù = 0 or é K''ù = 0 
dl(é K'ù) È dl(é K''ù) otherwise 


The three subsets correspond to the labels that appear in distinct pairs
in é K'ù×é K'ù,
é K''ù×é K''ù (with cl(é K''ù) Í W), and
é K'ù×é K''ù, respectively.
We define a safe approximation of the union of cl( K' & K'' ) for
all welltyped K & K'', written cls(B^{W},K Þ K'). The
definition is by cases:

If é K'ù = 0, we use cls(B^{W},K Þ K') = W.
(In this case, no new message with arguments is introduced.)
 If dl(K) Ç W = Ø and é Kù ¹ 0, we use
cls(B^{W},K Þ K') = cl(K').
(In this case, é Kù is a single message and é K''ù is empty.)
 If dl(K) Ç W ¹ Ø, we use
cls(B^{W},K Þ K') = dl(é K'ù) È W.
(In this case, all labels in é K''ù already appear in W.)
 Otherwise (é Kù = 0 and é K'ù ¹ 0),
we use cls(B^{W},K Þ K') = dl(é K'ù) È dom(é Bù).
Note that cls(B^{W},K Þ K') only depends on the domain of B and
not on its type assignment.
For example, consider the selective refinement of the class
locked_buff
of Section 4. Informally,
we may assume that the type of
buff is of the form B^{W} where dom(B) = dom(é Bù) = {put,
get, Empty, Some, Full, Check, Init} and W = {put, get, Empty, Some,
Full} (every label of W synchronizes with at least another one). The
refinement involves the two rewriting clauses Init(size)
Þ Init(size) > z.Free() and 0 Þ Free() > z.Free().
By item 2 of the definition of cls, we get
cls(B^{W}, Init(size) Þ Init(size)) = cl( Init(size)) = Ø,
which means that this refinement will not introduce any
new synchronization.
By item 1 of the definition of cls, since Free()
is 0, we obtain cls(B^{W}, 0 Þ Free()) = W (label
Free may synchronize with other labels but it cannot exchange values
with them).
These two independent results may be combined together by taking their
union to get an approximation of the type of the whole
refinement.
6.4 
Type checking processes and classes 

Figure 8: Typing judgments
A  x : t 
the object x has type t in environment A; 
A  x.l : t 
the label l conveys messages of type t for object x in
environment A; 
A  P 
the process P is welltyped in environment A; 
A  K :: B 
the pattern or selection pattern K binds variables welltyped in A
and joins labels in B. 
A  C :: z(r)B^{W, V} 
the class C is welltyped in environment A, declares the labels
of B, has coupled labels in W,
and has virtual labels V (with V Í dom(B) and W Í
dom(é Bù)). 
A  S :: B^{W}Þ B'^{W', V} 

the refinement clauses S are welltyped in environment A, refine
patterns with labels in B and coupled labels W into patterns
with labels in B', coupled labels in W',
and virtual labels V
(with W' Í dom(é Bù) È dom(é B'ù) and V Í
dom(B)). 

The typing judgments are described in Figure 8.
They rely on type environments A that bind class names c to
class type schemes and bind object names x to (external) type
schemes s or to (internal) type schemes " X. B with dom(B)
Í F. In a given environment A, an object x can
have two complementary bindings x : " X. [r] and x : " X.
B. The binding x : " X. [r] represents the typing of public
labels, x : " X. B is the binding of private labels.
Since X is a set of type and row variables, we write
{a ¬ g_{a}^{a Î X}} for replacing
variables in X with object and row types, correspondingly.
We write dom(A) for the set of names bound in A.
We let A + A' be (A \ dom(A')) È A', where A
\ X removes from A all the bindings of names in X
and let A + x : " X. [r], x : " X. B be
A\ {x} È x : " X. [r] È x : " X. B.
The typing rules appear in figures 9 and 10. Generalization in objects and classes relies on
a standard auxiliary definition: Gen(r, B, A) is the set of free
type variables of r or B that are not free in A.
Figure 9: Typing rules for
names, messages, and processes
Rules for names and messages
Rules for processes

Send 
A  x.l : (t_{i} ^{i Î I}) (A  x_{i} : t_{i}) ^{i Î I} 


A  x.l (x_{i} ^{i Î I}) 


Class 
A  C :: z(r)B^{W,V} 
A + c : " Gen (r, B, A). z(r)B^{W,V}  P 

 

Object 


A  obj x = C init P in Q 



Figure 10: Typing rules for patterns, classes, and refinement
clauses
Rules for patterns

MessagePattern 
(x_{i} : t_{i} Î A)^{i Î I} 


A  l(x_{i} ^{i Î I}) :: (l : t_{i}^{i Î I}) 


Synchronization 
A  J_{1} :: B_{1} A  J_{2} :: B_{2} 


A  J_{1} & J_{2} :: B_{1} Å B_{2} 


Alternative 
A  J_{1} :: B_{1} A  J_{2} :: B_{2} 


A  J_{1} or J_{2} :: B_{1} Å B_{2} 


2
Rules for classes
Sub 


A  c :: z(r)B^{W È W', V È V'} 


ClassVar 


A  c :: (z(r)B^{W,V}) {a ¬ g_{a}^{a
Î X}} 


Reaction 
A'  J :: B A + A'  P dom(A') = fn(J) 


A  J > P :: z(r)B^{cl(J),Ø} 


SelfBinding 
A + x : [r], x : (B  F)  C :: z(r)B^{W,V} 


A  self(x) C :: z(r)B^{W,V} 



Disjunction 
A  C_{1} :: z(r)B_{1}^{W1, V1} V_{1}' = V_{1} \ ( dom(B_{2}) \ V_{2}) 
A  C_{2} :: z(r)B_{2}^{W2, V2} V_{2}' = V_{2} \ ( dom(B_{1}) \ V_{1}) 


A  C_{1} or C_{2} :: z(r)(B_{1} Å B_{2})^{W1 È W2,
V1' È V2'} 


Refinement 
A  C :: z(r)B_{1}^{W1, V1} 
A  S :: B_{1}^{W1} Þ B_{2}^{W2, V2} dl(S) Ç dom(B_{1}) = Ø 


A  match C with S end :: z(r)(B_{1} Å B_{2})^{W1 È W2, V1 È V2} 


2
Rules for refinement clauses
Modifier 
(A  S_{i} :: B^{W}Þ B_{i}^{Wi, Vi})^{i Î I} 


A   
^{i Î I} S_{i} ::
B^{W}Þ (Å_{i Î I}B'_{i}) 





Processes.
In rule Class, all type variables can be generalized, regardless of
synchronization. This is safe because classes are templates for object
definitions: the set W in the class type of c is used to restrict
polymorphism, but only at object instantiation.
In rule Object, the class C is first typechecked and yields a
class type z(r)B^{W,Ø}. The shape of this type excludes
virtual labels, thus preventing the instantiation of a
partiallydefined object.
The object type is the restriction of labels declared in B to public
ones. The constraint r = B  M checks, for each public label
m of B, that the type given to m in B and in r are the same.
The process Q is typed in an environment extended with the
object x bound to a generalized [r].
The process P is typed as Q, except that P can also use the private
labels of x.
Patterns.
Typing rules for join patterns check that the patterns are
wellformed, collect their typed labels, and check that the
environment agrees with received objects.
Classes.
Rule Reaction checks that join patterns and guarded
processes agree on the typing environment extended with the received
variables.
Rule SelfBinding folds two bindings for self, accounting for
public and private bindings, respectively.
Rules Disjunction and Refinement merge
virtuallabel informations, as a disjunct or a parent class may
effectively define a virtual label.
Rule Refinement types match C with S end, out of typings of C and S.
It uses the auxiliary judgment for selection clauses
A  S :: B_{1}^{W1} Þ B_{2}^{W2, V2};
This premise will ensure that labels in the selection
patterns are all defined in B_{1}, hence declared in C.
On the contrary, the premise dl(S) Ç dom(B_{1}) = Ø implies
that names in dl(S) are not already declared in C. In particular,
this ensures that the pattern of every refined reaction rule is linear
(condition (2) in Section 3.3).
Refinement clauses.
Refinement clauses are typed much like reaction rules and
class disjuncts.
Rule Modifier types a series of selection clauses and builds a superset
of the coupled labels after the refinement, as detailed in
Section 6.3.
Rule Modifier also checks that labels in the
pattern K_{i}' agree with those K_{i} of the parent class; the set of
virtual labels accounts for labels potentially eliminated by the
clause.
6.5 
Type checking solutions 

We finally extend typing from programs to chemical solutions.
The typing judgment  ( D  P) states that the chemical
solution D  P is welltyped. The auxiliary judgments A 
D :: A' deals with active object definitions.
The typing rules appear in Figure 11.
Rule ChemicalSolution uses an additional notation A^{y}.
Let N be a set of object names
and A be a typing environment of the form
A = 

(x : s_{x}) È 

(x: " Y_{x}. B_{x})

For any string y of names in N,
we define the restricted environment:
A 
^{y} = 

(x : s_{x}) È


(x : " Y_{x}. B_{x})

Namely, A^{y} removes from the environment A the private
labels of objects which did not create x. Actually, x
cannot access these labels.
Figure 11: Typing rules for solutions
ChemicalSolution 
A = È_{y x # D Î D} A_{x} 
(A^{y}  D :: A_{x})^{y x # D Î D} 
(A^{y}  P)^{y # P Î P} 

 

Definition 
r = B  M 
X = Gen (r, B, A) \ ctv(BW) 
A  self(x) D :: z(r)B^{W,Ø} 


A  D ::
x : " X. [ r ], x : " X. (B  F) 



Rules ChemicalSolution and Definition are similar to
rule Object. The main difference is that, in A  D ::
A', the typing environment A' is polymorphic. This allows polymorphic
typechecking for solutions.
6.6 
Subject reduction with privacy 

We are now ready to state our main results on types for the chemical
semantics and the class rewriting, respectively. Additional lemmas
and the proofs appear in Appendix B.
Theorem 1 [Subject reduction]

Chemical reductions
preserve chemical typings:
if  D  P and D  P º D'  P' or
D  P ¾® D'  P', then  D'  P'.

Class rewriting
preserve typings:
if A  P and P ® P' then A  P'.
In combination, any interleaving of chemical reductions and class
rewritings preserves chemical typing.
Precisely, we can lift class rewriting steps from processes to chemical
solutions ( D  P, P ® D  P', P' when P ®
P') and we have that,
if D  P is welltyped and D  P (º stackrel ¾® È
®)^{*} D'  P', then D'  P' is also
welltyped.
The next theorem guarantees that chemical typing prevents any
runtime failure and class rewriting failure, as detailed in Definition 1 (Section 6.1):
Theorem 2 [Safety]
Welltyped chemical solutions
do not fail.
While we do not address type inference in this paper, our type system
has been carefully designed to allow type inference. We conjecture
that, given a typing environment A and a process P (or a class
C), it is decidable whether P (or C) is typable in A;
moreover, we conjecture that if C is typable then it has a principal
type.
We infer a type for the class buffer of
Section 3.1:
class buffer = self(z)
get(r) & Some(a) > r.reply(a) & z.Empty()
or put(a,r) & Empty() > r.reply() & z.Some(a)
The body of this class definition is of the form self(z) (J_{1} > P_{1} or
J_{2} > P_{2}).
First, consider the typing of pattern J_{1}.
By rules MessagePattern and
Synchronization we have:
A_{1}  get(r) & Some(a) :: B_{1} (1)
where the
type environment A_{1} and internal type B_{1} are
A_{1} = r:q_{1}, a:q_{2}
and
B_{1} = get : (q_{1}) ; Some : (q_{2}),
reflecting the presence of labels and their arities.
However, pattern J_{1} is not typed in isolation
but as the pattern of a reaction rule whose guarded process P_{1}
includes r.reply(a).
Rule Reaction requires that P_{1} be typed
in an environment that subsumes A_{1}.
Moreover, r.reply(a) connects
the types for r and a
(rule Send). Thus, we get:
q_{1} = [ reply : (q) ; h ] (reflecting that r is an
object with at least a reply label) and q_{2} = q.
Then, the type variable q is free in the types of both
Some and get which are joined in the same pattern
J_{1}.
Skipping some details,
rule Reaction yields the following
typing of J_{1} > P_{1}:
A  J_{1} > P_{1} :: z(r)B_{1}^{{get, Some}, Ø} (2)
where r is the public type for self, A is
described below,
and B_{1} is get : ([ reply : (q) ; h ]) ;
Some : (q).
Similarly, the second reaction rule is typed as:
A  J_{2} > P_{2} :: z(r)B_{2}^{ Ø, Ø} (3)
where
B_{2} = put : (q',[ reply : () ; h' ]) ;
Empty : ().
Note that the set of coupled labels is empty, since pattern J_{2}
contains only one label of nonzero arity.
Environment A must be the same in both (2) and (3) because these two
judgments are premises of a Disjunction rule:
A  J_{1} > P_{1} or J_{2} > P_{2} :: z(r)B^{{get,Some}, Ø} (4)
The internal type B is B_{1} Å B_{2}. Here, this amounts to
B_{1} È B_{2} since patterns J_{1} and J_{2} have no label in common.
(In the general case where a label is declared in several patterns,
the ``Å'' operator enforces a compatibility check on label
types.)
Hence B = get : ([ reply : (q) ; h ]) ;
Some : (q) ; put : (q',[ reply : () ; h' ]) ;
Empty : ().
Rule SelfBinding
implies that environment A contains two bindings for
the self name z,
namely, z:[r] and z:B_{r}.
The internal type of z, B_{r} is the
restriction of B to private labels, i.e. we get
B_{r}= Some : (q) ; Empty : ().
We can now detail the typing for P_{2} (which is an hypothesis for (3)).
Listing only pertinent parts of the typing environment A +
A_{2}, we have:
... a:q', z:(Some:(q), ...)
 P_{2} (5)
Now, observe that P_{2} includes the message
z.Some(a), which requires
the types for a and for any message on Some
to be equal. Thus, q = q'.
Hence, the type for class variable buffer finally is:
" {h, h', q}. z(r)B^{{get,
Some}, Ø} (6)
where B is as before (after equating q and q'). That is:
B = get : ([ reply : (q) ; h ]) ;
Some : (q) ; put : (q,[ reply : () ; h' ]) ;
Empty : ().
Observe that, according to Class, all the type variables
(h, h' and q) are generalized. As a consequence
the type for class buffer is as polymorphic as it can be.
Also observe that the public type r is yet unconstrained.
Nevertheless, polymorphism will be restricted and
r will be made precise while
creating objects from class buffer (rule Object).
7 
Related and future works 

The design and implementation of concurrent objectoriented
languages, e.g.
[2, 33, 1, 6],
has recently prompted the investigation of the theoretical foundations
of concurrent objects.
Several works provide encodings of objects in process
calculi [31, 28, 14, 8, 19]
or, conversely, supplement objects with concurrent
primitives [23, 4, 13, 29].
These works promote a unified framework for reasoning about objects and
processes, but they do not address the incremental definition of concurrent
objects or its typechecking. (When considered, inheritance is treated as in
a sequential language and does not deal with synchronization.) In
particular, the TyCO language, developed by Vasconcelos and his collegues,
relies on a core calculus which is very close to the objective join
calculus in Section 2, with few differences due to name
definitions. However the two languages differ when classes are considered.
In particular, TyCO [29] only allows simple forms of
inheritance, namely extensions of classes with new methods, and updates
of old methods with new ones. No mechanism is provided to access
methods in the super class and, therefore, to reuse their bodies. As regards
the type system, both the languages stick to a predicative
polymorphism discipline. However, in our calculus, polymorphism
originates from class and obj operations and regards
objects and classes as a whole;
in TyCO polymorphism originates from a different
operatorthe letwhich allows to define one (polymorphic)
function at a time, and regards single methods.
The addition of classes to the join calculus enables a modular
definition of synchronization. Different receivers for the same labels
can thus be introduced at different syntactic positions in a program.
In that respect, we partially recover the ability of the pi calculus
to dynamically introduce receivers on channels [21]. However,
our layered design confines this modularity to classes, which are
resolved at compile time.
From a programminglanguage viewpoint, this strikes a good balance
between flexibility and simplicity, and does not preclude type
inference or the efficient compilation of
synchronization [16].
Odersky independently proposed an objectoriented
extension of the join calculus [24, 25].
As in Section 2, they use join patterns to define
objects and synchronization between labeled messages.
The main difference lies in the encapsulation of methods within
objects.
In our proposal, a definition binds a single object, with all the
labels appearing in the definition, and we rely on types to hide
some of those labels as private.
In their proposal, a definition may bind any number of objects, and
each object explicitly collects some of the declared labels as its
methods. As a result, a label that is not collected remains
syntactically private.
Besides, their synchronization patterns can express matching on the
values carried in messages (strings, integers, lists, trees, etc.)
rather than matching on just the message labels.
For instance, a rule l(h::t) > P reacts provided l carries a
nonempty list.
Those design decisions may lead to different implementation
strategies. However, they do not deeply affect typing.
As regards polymorphism, our generalization rule
Object corresponds to the one currently implemented in
JoCaml [15].
It is more expressive
than the generalization rule initially proposed in [12] and seems
equivalent to the generalization rule of [7].
In [12], nongeneralizable type variables
were computed altogether for all clauses of a definition, which may be
too conservative.
In both [15]
and [7], nongeneralizable
type variables are computed one rule at a time, which is more precise.
This latter approach is natural in our setting, since
recursion is left open till object instantiation.
In ML, this amounts to typing
let rec x_{1} = a_{1} and x_{2} = a_{2} in a as let x = fix
(l (x_{1},x_{2}). (a_{1}, a_{2})) in a. The latter term separates
typechecking the body of the recursion
from typechecking recursion itself.
Our language supports multiple inheritance of classes,
but not mixin inheritance [5], which
amounts to parameterize classes by other
classes. As in OCaml, we can only combine existing classes,
but obtain mixin inheritance indirectly through modules
and functors.
In sequential languages, deep method renaming, i.e. rewriting of
recursive calls or method hiding, can be expressed using
dictionaries [27] or views [30].
In concurrent languages, views offer additional benefits. For
example, one can duplicate the synchronization patterns of a
superclass by inheriting several copies of the class, independently
refine their synchronization, and use different views to access the
copies.
For instance, one could distinguish internal and external views in
the last example of Section 4.
The integration of views in the objective join calculus deserves
further investigation.
Since classes are just object templates, our typing system allows
polymorphic variables in class types, and defer any monomorphic
restriction till object instantiation.
For type safety, one must check that, in every join pattern of an
object, any variable occurring in the type of several labels is
monomorphic.
To this aim, our class types collect a superset W of these coupled
labels, but other approaches are possible.
A plain solution is to assume that all labels are coupled. Then,
class types don't convey any synchronization information, and
generalization is as in [12].
Conversely, the class types could detail the labels of each join
pattern. This would allow us to detect refinement errors at compile
time.
However, the resulting types would be very precise, and we would also
need some form of subtyping to get rid of excessive information.
This is another promising direction for research.
We have designed a simple, objectbased variant of the join calculus.
Every object is defined as a fixed set of reaction rules that describe
its synchronization behavior.
The expressiveness of the language is significantly increased by
adding classesa form of open definitions that can be incrementally
assembled before object instantiation.
In particular, our operators for inheritance can express
transformations on the parent class, according to its synchronization
patterns.
We motivated our design choices using standard, problematic examples
that mix inheritance and synchronization.
We gave operational semantics for objects and classes, and a type
system that prevents standard errors and also enforces privacy.
Acknowledgments.
This work benefited from fruitful discussions with Sylvain Conchon,
Fabrice Le Fessant, and François Pottier.
 [1]

G. Agha, P. Wegner, and A. Yonezawa.
Research Directions in Concurrent ObjectOriented Programming.
MIT Press, 1993.
 [2]

P. America.
Issues in the design of a parallel objectoriented language.
Formal Aspects of Computing, 1(4):366411, 1989.
 [3]

N. Benton, L. Cardelli, and C. Fournet.
Modern Concurrency Abstractions for c.
In Informal Proceedings of the FOOL 9 workshop. ACM, January
2002.
 [4]

P. D. Blasio and K. Fisher.
A calculus for concurrent objects.
In U. Montanari and V. Sassone, editors, Proceedings of the 7th
International Conference on Concurrency Theory (CONCUR '96), LNCS 1119,
pages 406421, 1996.
 [5]

G. Bracha and W. Cook.
MixinBased Inheritance.
In N. Meyrowitz, editor, European Conference on
ObjectOriented Programming: Systems, Languages, and Applications,
pages 303311, Otawa, 1990. ACM press.
 [6]

L. Cardelli.
Obliq A language with distributed scope.
Computing Systems, 8(1):2759, 1995.
 [7]

G. Chen, M. Odersky, C. Zenger, and M. Zenger.
A functional view of join.
Technical Report ACRC99016, University of South Australia, 1999.
 [8]

S. DalZilio.
Quiet and bouncing objects: Two migration abstractions in a simple
distributed blue calculus.
In H. Hüttel and U. Nestmann, editors, Proceedings of the
Worshop on Semantics of Objects as Proceedings (SOAP '98), pages 3542,
June 1998.
 [9]

C. Fournet.
The JoinCalculus: a Calculus for Distributed Mobile
Programming.
PhD thesis, Ecole Polytechnique, Palaiseau, Nov. 1998.
 [10]

C. Fournet and G. Gonthier.
The reflexive chemical abstract machine and the joincalculus.
In Proceedings of POPL '96, pages 372385, Jan. 1996.
 [11]

C. Fournet, G. Gonthier, J.J. Lévy, L. Maranget, and D. Rémy.
A calculus of mobile agents.
In U. Montanari and V. Sassone, editors, Proceedings of the 7th
International Conference on Concurrency Theory (CONCUR '96), LNCS 1119,
pages 406421, 1996.
 [12]

C. Fournet, C. Laneve, L. Maranget, and D. Rémy.
Implicit typing à la ML for the joincalculus.
In A. Mazurkiewicz and J. Winkowski, editors, Proceedings of the
8th International Conference on Concurrency Theory, LNCS 1243, pages
196212, 1997.
 [13]

A. D. Gordon and P. D. Hankin.
A concurrent object calculus: reduction and typing.
In Nestmann and Pierce [22].
 [14]

J. Kleist and D. Sangiorgi.
Imperative objects and mobile processes.
In Proc. IFIP Working Conference on Programming
Concepts and Methods (PROCOMET'98). NorthHolland, 1998.
 [15]

F. Le Fessant.
The JoCaml system prototype.
Software and documentation available from
http://pauillac.inria.fr/jocaml, 1998.
 [16]

F. Le Fessant and L. Maranget.
Compiling joinpatterns.
In Nestmann and Pierce [22].
 [17]

X. Leroy, D. Doligez, J. Garrigue, D. Rémy, and J. Vouillon.
The Objective Caml system, documentation and user's manual 
release 3.04.
Technical report, INRIA, December 2001.
Documentation distributed with the Objective Caml system.
 [18]

S. Matsuoka and A. Yonezawa.
Analysis of inheritance anomaly in objectoriented concurrent
programming languages.
In G. Agha, P. Wegner, and A. Yonezawa, editors, Research
Directions in Concurrent ObjectOriented Programming, chapter 4, pages
107150. The MIT Press, 1993.
 [19]

M. Merro, J. Kleist, and U. Nestmann.
Mobile objects as mobile processes.
Information and Computation, To appear.
 [20]

J. Meseguer.
Solving the inheritance anomaly in concurrent objectoriented
programming.
In O. M. Nierstrasz, editor, 7th European Conference on Object
Oriented Programming, number 707 in LNCS, pages 220246. SRI International,
Springer Verlag, 1993.
 [21]

R. Milner, J. Parrow, and D. Walker.
A calculus of mobile processes, parts I and II.
Information and Computation, 100:140 and 4177, Sept. 1992.
 [22]

U. Nestmann and B. C. Pierce, editors.
HLCL '98: HighLevel Concurrent Languages, volume 16(3) of
Electronic Notes in Theoretical Computer Science, Nice, France, Sept.
1998.
 [23]

O. Nierstrasz.
Towards an object calculus.
In O. N. M. Tokoro and P. Wegner, editors, Proceedings of the
ECOOP'91 Workshop on ObjectBased Concurrent Computing, LNCS 612, pages
120, 1992.
 [24]

M. Odersky.
Functional nets.
In Proc. European Symposium on Programming, number 1782 in
LNCS, pages 125. Springer Verlag, Mar. 2000.
 [25]

M. Odersky.
An overview of functional nets.
In APPSEM Summer School, Caminha, Portugal, LNCS. Springer
Verlag, Sept. 2000.
To appear.
 [26]

D. Rémy and J. Vouillon.
Objective ML: A simple objectoriented extension to ML.
In Proceedings of POPL '97, Jan. 1997.
Available electronically at
ftp://ftp.inria.fr/INRIA/Projects/cristal/
Didier.Remy/objectiveml!tapos98.ps.gz.
 [27]

J. G. Riecke and C. A. Stone.
Privacy via subsumption.
Theory and Practice of Object Systems, 1999.
 [28]

D. Sangiorgi.
An interpretation of typed objects into typed pcalculus.
Information and Computation, 143(1):3473, 1998.
 [29]

V. T. Vasconcelos.
Typed concurrent objects.
In 8th European Conference on Object Oriented Programming,
volume 821 of Lecture Notes in Computer Science, pages 100117.
SpringerVerlag, July 1994.
 [30]

J. Vouillon.
Combining subsumption and binary methods: An object calculus with
views.
In Proceedings of POPL '01, Jan. 2001.
 [31]

D. J. Walker.
Objects in the picalculus.
Information and Computation, 116(2):253271, 1995.
 [32]

M. Wand.
Complete type inference for simple objects.
In Proceedings of the IEEE Symposium on Logic in Computer
Science, Ithaca, NY, June 1987.
 [33]

A. Yonezawa, J.P. Briot, and E. Shibayama.
Objectoriented concurrent programming in ABCL/1.
ACM SIGPLAN Notices, 21(11):258268, Nov. 1986.
Proceedings of OOPSLA '86.
A 
Crossencodings to the join calculus 

In the join calculus of [10], each definition
binds one or several channel names that can be passed
independently whereas, in the objective join calculus of
Section 2, each definitions binds a single object. This
difference is not very deep; we briefly present crossencodings
between these two variants.
We recall a syntax for the join calculus:
P 
::= 
0

x(u)

P & P

defD in P 
D 
::= 
M > P

D or D 
M 
::= 
x(u)

M & M 
Join calculus processes can be encoded by introducing singlelabel
forwarder objects and passing those object names instead of channel
names.
(The encoding given below works for nonrecursive definitions in the
join calculus; recursive definitions can easily be eliminated
beforehand [9].)
[[0]] 
= 
0 
[[x (u)]] 
= 
x.send (u) 
[[P_{1} & P_{2}]] 
= 
[[P_{1}]] & [[P_{2}]] 
[[ defD in P]] 
= 
obj o = [[D]] in 


obj x_{1} = send (u_{1}) > o.m_{1} (u_{1}) in ... 


obj x_{n} = send (u_{n}) > o.m_{n} (u_{n}) in [[P]] 
where we assume that D defines the channel names x_{1}, ..., x_{n}. Accordingly,
we encode channel reaction rules and patterns as follows:
[[D_{1} or D_{2}]] 
= 
[[D_{1}]] or [[D_{2}]] 

[[M_{1} & M_{2}]]^{} 
= 
[[M_{1}]]^{} & [[M_{2}]]^{} 
[[M >P]] 
= 
[[M]]^{}> [[P]] 

[[x (u)]]^{} 
= 
m_{x}(u) 
Conversely, one can encode objective join processes into a join
calculus enriched with records.
Join calculus values then consist of both names and records, written
{l_{i} = x_{i}}^{i Î I}; we use # for record projection. The
encoding substitutes explicit records of channels for defined
objects.
[[0]] 
= 
0 
[[x.l (u)]] 
= 
x # l (u) 
[[P_{1} & P_{2}]] 
= 
[[P_{1}]] & [[P_{2}]] 
[[ obj x = D \ init P_{1} in P_{2}]] 
= 
( def[[D]]_{x} in [[P_{1} & P_{2}]])
{x ¬ {l = x_{l}, l Î dl(D)}} 
[[D_{1} or D_{2}]]_{x} 
= 
[[D_{1}]]_{x} or [[D_{2}]]_{x} 

[[M_{1} & M_{2}]]_{x} 
= 
[[M_{1}]]_{x} & [[M_{2}]]_{x} 
[[M > P]]_{x} 
= 
[[M]]_{x} > [[P]] 

[[l (u)]]_{x} 
= 
x_{l}(u) 
The encoding above treats all methods as public; it can be refined
to preserve the scope of private labels using two records of channels
instead of a single one.
In the following lemmas, we let D range over any right hand
side of a judgment, except for the chemical judgment.
Lemma 2 [Useless variable]
For any judgment of the form A  D, and any
name x that is not free in D we have:
A  D Û A + A'  D
where A' is either x : s or x: s, x : " X. B.
Lemma 3 [Renaming of type variables]
Let h be a substitution on type variables. We have:
A  D Þ h(A)  h(D)
We say that a type scheme " X . t is more general than
" X'. t' if t' is of the form h (t) for some
substitution h replacing type and row variables by types and rows,
respectively.
This notion is also lifted to set of assumptions as follows:
A' is more general than A if A and
A' have the same domain and for each u in their domain,
A'(u) is more general than A(u).
Lemma 4 [Generalization]
If A  D and A' is more general than A, then A'  D.
Lemma 5 [Substitution of a name in a term]
If A + x : t  D and A  u : t then A  D
{^{u}/_{x}}.
Similarly, if A + x : [m_{i} : t_{i} ^{i Î I}],
x : (l : t_{l}^{l Î S})  D and
A  y : t,
(A  y.m_{i} : t_{i}) ^{i Î I}, and
(A  y.l : t_{l})^{l Î S} then A  D{x
¬ y}.
Lemma 6 [Substitution of a class name in a term]
Let A + c : " X . z(r)B^{W,V}  D and
A + B  C :: z(r)B^{W,V} and
X Í Gen (r, B, A).
Then A  D {c ¬ C}.
B.2 
Subject reduction for the chemical semantics (Theorem 1.1) 

Proof:
Let  ( D  P) and D  P º stackrel ¾® D' 
P'. We demonstrate that  ( D'  P'). According to the rules in
Figure 6, there are two cases for the proof of
D  P º stackrel ¾® D'  P':

an instance of rule Obj, followed by
a sequence of ChemistryObj;
 an instance of one of the rules Par, Nil,
PublicComm, PrivateComm, Red, followed by a
sequence of Chemistry.
We discuss the two cases separately.
Case 1.
The reduction is D  y # obj x = D init P in Q, P
º D, y x # D  y x # P, y # Q, P,
where x Ïfn( D) È fn( P).
On the one hand, if  ( D  y
# obj x = D init P in Q, P) (1) and rule
ChemicalSolution, we obtain
(A^{j}  D' :: A_{z})^{j z # D' Î
D} (2), A^{y}  obj x = D init P in Q and
(A^{j}  P')^{j # P' Î P} (3),
where A = È_{j z # D' Î D} A_{z}.
A derivation of A^{y}  obj x = D init P in Q
must have the form:
[Object] 
A^{y}  self( x) D :: z( r) B ^{W,Ø} (4) 
X = Gen ( r, B, A^{y}) \ ctv( B W) (5) A^{y} + x : " X. [ r],
x : " X. ( B  F)  P (7) 
r = B  M (8) A^{y}+ x : " X. [ r]  Q (9) 


A^{y}  obj x = D init P in Q 


On the other hand, if  ( D, y x # D  y x # P, y # Q,
P) (10) and rule ChemicalSolution, we obtain
(A'^{j}  D' :: A'_{z})^{j z # D' Î
D} (11), A'^{y}  D :: A'_{x},
A'^{y x}  P (12), A'^{y} 
Q (13) and
(A'^{j}  P')^{j # P' Î P} (14)
where A' = (È_{j z # D' Î D} A'_{z}) È A'_{x}.
A derivation of A'^{y}  D :: A'_{x} must have the form:
[Definition] 
A' ^{y}  self( x) D :: z( r') B' ^{W',Ø} (15) 
r' = B'  M (16) X' = Gen ( r', B', A' ^{y}) \ ctv( B' W') (17) 

 

where A'_{x} = x : " X'. [ r ] Å x : " X'. (B' 
F).
Note that, by definition, A does not bind x because
x Ïfn( D). Therefore, by
Lemma 2, if either (1) or (10)
hold, then we can always choose A or A' such that
A' = A + A'_{x}, the judgments
(2) and (11) be equivalent, as well as the judgments (3)
and (14).
We now focus on the other judgments.
Then, since A'^{y}
= A^{y} + x : " X'. [r'],
the following premises can be made equivalent to one another:
 (4)º (15):
By Lemma 2 and identifying B' with B, r' with r, and W' with W.
 (5)º (17):
By definition, we now have
X = (ftv(B) È ftv(r)) \ (ftv(A^{y}) È ctv(BW)) 
X' = (ftv(B) È ftv(r)) \ (ftv(A'^{y}) È
ctv(BW)) 
Since A'^{y} is equal to A^{y} + x : " X. r and
A^{y} does not bind x, we have X' Í X.
Conversely, we have X \ X' Í ftv(" X. r). Since by
definition ftv(" X.r) does not intersect X, it follows that
X \ X' is empty, thus X Í X'.
 (7)º (12): Using the previous equivalences, we now have A_{x} = A'_{x}.
Therefore, A'^{y x} is equal to A^{y x}.
 (9)º (13): Same reasoning as the previous case.
 (8)º (16): The two equalities are now identical.
To conclude, if (1) holds, then (10) holds by taking
A + x : " X. [ r ], x : " X. (B  F)
for A', and conversely, if (10) holds, then (1)
holds by taking A' \ x for A.
Case 2.
The reduction is D  P_{1}, P º stackrel ¾®
D  P_{2}, P. There are several subcases, according to the
leaf node in the proof tree.
The equivalence is D  y # 0, P º D  P.
Indeed the judgment A  y # 0
is always true, for any environment A.
The equivalence is D  y # (P & Q),
P º D  y # P, y # Q, P. We apply rule
ChemicalSolution, then it suffices to prove that the two
judgments A^{y}  P & Q and A^{y}  P, A^{y}  Q are equivalent. This follows by rules Parallel and
ChemicalSolution.
This is similar to the above case, and relies on rules
ChemicalSolution,
Parallel and JoinParallel.
The reduction is D, y x # D  y' # x. m(u), P
¾® D, y x # D  y x #
x. m(u), P.
Let us assume that A^{y}  D :: A_{x} and A^{y'} 
x. m(u) (1).
We must show that A^{y x}  x.m (u_{i} ^{i Î I})
where u = u_{i} ^{i Î I}.
A complete derivation of (1) must be of the form:
[Send] 
[Message] 
[ObjectVar] 


A^{y'}  x : [ m : (t_{i} ^{i Î I}); r ] 





A^{y'}  x.m : (t_{i} ^{i Î I}) 



( 


) 
^{i Î I} 



A^{y'}  x.m (u_{i} ^{i Î I}) 


This derivation, which does not use any internal type assumption of
A (any PrivateMessage rule),
is not affected by replacing A^{y'} with A^{y x}. Thus,
A^{y x}  x.m (u_{i} ^{i Î I}) holds.
The reduction is D, y x # D  y x y' # x. f(u), P
¾® D, y x # D  y x # x. f(u), P.
Let us assume that A^{y}  D :: A_{x}
and A^{y x y'}  x. f(u) (1).
We must show that A^{y x}  x.f (u_{i} ^{i Î I})
where u = u_{i} ^{i Î I}.
A complete derivation of (1) must be of the form:
[Send] 

PrivateMessage
x : " X. (f : (t_{i} ^{i Î I}); B) Î A^{y x y'} 


A^{y x y'} 
x.f : (t_{i}{a ¬ g_{a}^{a Î X}}^{i Î I}) 



( 

ObjectVar 

A^{y x y'} 
u_{i} : t_{i} {a ¬ g_{a}^{a Î X}} 





) 
^{i Î I} 



A^{y x y'}  x.f (u_{i} ^{i Î I}) 


Note that, the only internal type assumption in the premise is on x, which
remains in A^{y x}. Thus, as in case PublicComm,
we can replace A^{y x y'} by A^{y x} in this
derivation and conclude that A^{y x}  x. f(u_{i} ^{i Î I}).
The reduction is D, y x # D  y x # x.(Ms), P ¾®
D, y x # D  y x # (Ps), P, where D is of the form
M > P or D' and M is of the form &_{iÎ I}l_{i}(x_{i}).
A derivation of  ( D, y x # D  y x # x.(Ms), P)
must follow from rule ChemicalSolution with the following
premises:

A = (È_{j z # D'' Î D} A_{z}) È A_{x} 
(1) 
(A^{j}  D'' :: A_{z}) ^{j z # D'' Î D} 
(2) 
A^{y}  D :: A_{x} 
(3) 
A^{y x}  x.(M s) 
(4) 
(A^{j}  P')^{j # P' Î P} 
(5) 

The derivation of (3) must end with rule Definition
with the premises

A_{x} = x : " X. [ r ], x : " X. (B  F) 
(6) 

r = B  M 
(7) 

X = Gen (r, B, A^{y}) \ ctv(BW) 
(8) 

A^{y}  self(x) D :: z(r)B^{W,Ø} 
(9) 
To demonstrate  ( D, y x # D  y x # (Ps), P)
it suffices to show that A^{y}  Ps.
Note that A^{y x} = A^{y} + A_{x} follows from (1).
The derivation of (4) must end with a rule JoinParallel. Hence, for each message l_{i} (s (x_{i})) of M
s, we have A^{y} + A_{x}  x.l_{i} (s(x_{i})).
In turn, this must be derived by rule Send with the premises
A^{y} + A_{x}  x.l_{i} : t_{i} (10)
and A^{y} + A_{x}  s(x_{i}) : t_{i} (11).
The judgment (10) is derived by either rule PrivateMessage or Message,
depending on whether l is private or public.
In both cases, each tuple t_{i} is an instance of the generic
type " X. B(l_{i}), with a substitution h_{i} of domain in
X Ç ftv(B(l_{i})).
The derivation of (9) must contain a subderivation

Reaction 
A'  M :: B_{0} (12) A^{y}+ x : [ r], x :( B F) + A'  P (13) dom( A') = fn( M) 


Sub
A^{y} + x : [r], x :(B F)
 M > P :: z(r)B_{0}^{cl(M),Ø} 


A^{y} + x : [ r], x :( B F)
 M > P :: z( r) B_{0}^{W,Ø} (14) 




where cl(M) Í W (15)
(the judgment (14) is then combined with other judgments for
other reaction rules of D
by a sequence of Disjunction rules, followed by a rule
Self, to end up with (9)).
The internal type B_{0} is therefore a subset of B.
As regards the premise (12), it is derived by a combination of rules
Synchronization, MessagePattern, and EmptyPattern.
Hence, we have:
A'  l_{i}( x_{i}) :: l_{i} : B( l_{i}) (16) 
for every i Î I.
By (15) and the definitions of cl(B) and
ctv(BW), we have
ftv(B (l_{i})) Ç ftv(B(l_{j})) Í ctv(BW), hence by
(8),
ftv(B (l_{i})) Ç ftv(B(l_{j})) Ç X = Ø,
for every distinct i and j in I.
Thus,
the sets (X Ç ftv(B(l_{i})))^{i Î I}, i.e. dom(h_{i})^{i Î I} form a
partition of X.
Let h be the sum of substitutions Å^{i Î I} h_{i}.
Observe that the domain of h is included in X and is thus disjoint
from free type variables of A^{y} (17).
Applying Lemma 3 to (13), we have
h (A^{y} + x : [r], x :(B F)) + h (A')
 P, that is,
A^{y} + x : [h(r)], x : h (B F) +
h (A')  P.
By Lemma 4, we can let x be used
polymorphically, i.e. A^{y} + A_{x} + h (A')  P.
Similarly, we have
(A^{y} + A_{x}  s(x_{i}) : h(t_{i}'))^{ xi : ti' Î A'}
by Lemmas 3 and 4 successively applied to
the collection of judgments (11).
Thus, by Lemma 5, we derive A^{y} + A_{x}
 Ps.
B.3 
Subject reduction for the rewriting semantics (Theorem 1.2) 

We first show a couple of properties relating typing and
the set of declared labels.
Lemma 7 []
For any class C such that A  C : z(r)B^{V,W},
then dl(C) = dom(B).
The proof of this lemma is omitted because it is a straighforward induction on
the depth of A  C : z(r)B^{V,W}.
Lemma 8 []
For any selective refinement clauses S such that
A  S :: B^{W} Þ B'^{W', V'}, we have
dom(B') \ dom(B) Í dl(S).
Proof:
Selective refinement clauses can always be written as _{i Î I} K_{i}
Þ K'_{i} > P.
A proof of
A  S :: B^{W} Þ B'^{W', V'} can only end with rule Modifier in which the derivation of each premise ends with a rule ModifierClause. Hence, we have at least the judgments



A_{i}  K_{i} :: B_{i} 
(18) 


B_{i} Í B 
(19) 


A_{i}  K_{i}' :: B'_{i} 
(20) 


B' = Å^{i Î i} B'_{i} 
(21) 

Hence,



dom(B') \ dom(B) 

Í 
dom(B') \ (È^{i Î I} dom(B_{i})) 

by (19) 




= 
(È^{i Î I} dom(B'_{i})) \ (È^{i Î I} dom(B_{i})) 

by (21) 




= 
È^{i Î I} ( dom(B'_{i}) \ (È^{jÎ I} dom(B_{j}))) 





Í 
È^{i Î I} ( dom(B'_{i}) \ dom(B_{i})) 





= 
È^{i Î I} (dl(K'_{i}) \ dl(K_{i})) 





= 
dl(S) 


We now show that filter rewriting ^{ }® preserves typing.
We denote with B \ L the set of pairs l :
t that belongs to B and such that l ÏL.
Lemma 9 [Filter rewriting]
If all the following conditions hold
C with S ® C' A  C :: z(r)B^{W,V} 
A  S :: B_{1}^{W1} Þ B_{2}^{W2,V2} dl(S) Ç dom(B_{1}) = Ø B Í B_{1} B_{2}  dom(B_{1}) Í B_{1} 

then A  C' :: z(r)(B Å (B_{2} \ L))^{W',V'}
for some W' Í W È (W_{2} Ç
dom(B Å (B_{2} \ L))),
V' Í V È (V_{2} Ç ( dom(B_{1}) \ L)),
and L Í (dl(S) \ dl(C')) È ( dom(B_{1})
\ dom(B)).
Proof:
In this proof, we abbreviate dom(B)
by ëBû, for sake of conciseness.
Basic cases.
Let us assume that


K_{1} & K > P with K_{1} Þ K_{2} > Q  S



®
K_{2} & K > P & Q or dl(K_{1}) \ dl(K_{2}) 
(1) 


A  K_{1} & K > P :: z(r)B^{W, V} 
(2) 


A  K_{1} Þ K_{2} > Q  S ::
B_{1}^{W1} Þ B_{2}^{W2,V2} 
(3) 


((dl(K_{2}) \ dl(K_{1})) È dl(S)) Ç ëB_{1}û = Ø 
(4) 


B Í B_{1} 
(5) 


B_{2}  ëB_{1}û Í B_{1} 
(6) 
The judgments (2) and (3) are respectively
derived by
[Sub] 
[Reaction] 

A + A'  P (10) ëA' û = fn( K_{1} & K) (11) 


A  K_{1} & K > P :: z(r)(B_{1}' Å B_{0})^{cl(K1 & K),Ø} 





A  K_{1} & K > P :: z(r)(B_{1}' Å B_{0})^{W,V} 


and,
[Modifier]+[Sub] 

A''  K_{1} :: B_{1}' (12) 
A''  K_{2} :: B_{2}' (14) 



W_{2}' = cls(B_{1}^{W1}, K_{1} Þ K_{2}) 


A  K_{1} Þ K_{2} > Q :: B_{1}^{W1} Þ
B_{2}'^{W2',dl(K1) \ dl(K2)} 


··· 



A  K_{1} Þ K_{2} > Q  S :: B_{1}^{W1}
Þ B_{2}^{W2,V2} 


where B = B_{1}' Å B_{0} (17), cl(K_{1} & K)
Í W (18),
B_{2}' Í B_{2} (19), W_{2}' Í W_{2} and dl(K_{1})
\ dl(K_{2}) Í V_{2} (20).
From (7) and (12), A' and A'' coincide on
fn(K_{1}) because they assign the same types to fn(K_{1}). Moreover,
due to the scope rules of reaction rules and the selection operator, we
can safely assume that ëA'û Ç ëA''û = fn(K_{1}).
Thus, by Lemma 2 applied to (8),
and (14)
we derive A'+A''  K :: B_{0} (21) and
A'+A''  K_{2} :: B_{2}' (22).
Similarly, by lemma 2 applied to
(10) and (15), we also derive
A + A' + A''  P (23) and A + A' + A''  Q (24).
Foremost we prove the linearity of K_{2} & K.
Notice that dl(K_{2}) = (dl(K_{2}) \ dl(K_{1})) È (dl(K_{2}) Ç
dl(K_{1})) and both left and right handsides of the È
have an empty intersection with dl(K). This follows from (4) and
from the linearity of K_{1} & K.
By rule Synchronization with premises (22) and
(21), we derive
A' + A''  K_{2} & K :: B_{2}' Å B_{0} (25).
Also, combining the judgments (23) and (24)
yields A + A' + A''  P & Q (26) using rule Parallel.
By premises (11) and (16) we have ëA'û È ëA''û = fn(K) È fn(K_{1})È fn(K_{2}).
By (16) and (12), we have
fn(K_{1}) Í fn(K_{2}). Hence
ëA' + A''û = fn(K_{2} & K) (27).
Therefore, by Reaction with premises (25), (26), and (27) we derive
A 
K_{2} &
K > P &
Q ::
z(
r)(
B_{2}'
Å B_{0})
^{cl(K2 & K),Ø}
(28).
By rule Abstract, we also deduce
A 
dl(
K_{1}) \
dl(
K_{2}) ::
z(
r)
B_{1}''
^{Ø,dl(K1) \ dl(K2)}
(29)
where B_{1}'' = B_{1}' \ dl(K_{2}) (30).
Hence, Disjunction allows to derive:
A 
K_{2} &
K > P &
Q or L' ::
z(
r)(
B_{2}'
Å B_{0} Å B_{1}'' )
^{cl(K2 & K), dl(K1) \ dl(K2)}
(31)
and by rule Sub:
A 
K_{2} &
K > P &
Q or L' ::
z(
r)(
B_{2}'
Å B_{0} Å B_{1}'' )
^{W', V'}
(32)
where W' = W È cl(K_{2} & K) and V' = V È (dl(K_{1})
\ dl(K_{2})).
Let L be
(dl(S) \ (dl(K_{2}) È dl(K) È dl(K_{1})))
È ((ëB_{1}û \ ëBû) \ dl(K_{2})),
or equivalently,
(dl(S) \ (ëB'_{2}û È ëB_{0}û È ëB'_{1}û))
È ((ëB_{1}û \ ëBû) \ ëB'_{2}û) (33).
Observe that L is choosen so as to satisfy the condition
L Í (dl(S) \ dl(C')) È (ëB_{1}û
\ ëBû).
To conclude, we verify that other constraints of the lemma are
satisfied for the judgment (32). That is,

B_{2}' Å B_{0} Å B_{1}'' = B Å (B_{2} \ L).
By (6), (13), (17), (19)
it is enough to check the set equality:
ëB'_{2}ûÈ ëB_{0}û È ëB''_{1}û = ëBû È
(ëB_{2}û \ L).
Since both sides of (33) are
restrictions outside of the set ëB'_{2}û, we have
L Ç ëB'_{2}û Ì ëBû (34).
Therefore,

ëB_{2}'û È ëB_{0}û È ëB_{1}''û 

= 
ëB_{2}'û È ëB_{0}û È (ëB_{1}'û \ dl(K_{2})) 
by definition of B'_{1} 

= 
ëB_{2}'û È ëB_{0}û È (ëB_{1}'û \ ëB'_{2}û)) 
by (16) 

= 
ëB_{2}'û È ëB_{0}û È ëB_{1}'û 

= 
ëB_{2}'û È ëBû 
by definition of B 

= 
ëBû È (ëB_{2}û \ L) 
by (34) 

 W' Í W È (W_{2} Ç
(ëB Å (B_{2} \ L)û).
Because W' = W È cl(K_{2} & K) and cl(K_{2} & K)
Í W_{2} by (18), and
cl(K_{2} & K) Í
dl(K_{2} & K) = ëB'_{2}û È ëB_{0}û Í
ëB Å (B_{2} \ L)û by the equality above.
 V' Í V È (V_{2} Ç (ëB_{1}û \ L)). By
definition, V' = V È (dl(K_{1}) \ dl(K_{2})) and dl(K_{1})
\ dl(K_{2}) Í V_{2} by (20). It remains to
prove that dl(K_{1}) \ dl(K_{2})Í
ëB_{1}û \ L. Since dl(K_{1}) \ dl(K_{2})Í
ëB_{1}û, it suffices to show that (dl(K_{1}) \ dl(K_{2}))
Ç L = Ø. Obviously, (dl(K_{1}) \ dl(K_{2})) Ç
(dl(S) \ dl(K_{2} & K & K_{1})) = Ø, whilst (dl(K_{1})
\ dl(K_{2})) Ç ((ëB_{1}û \ ëBû) \ dl(K_{2}))= Ø, since dl(K_{1}) = ëB'_{1}û Í ëBû.
Let us assume


M > P with 0 ® M > P 
(1) 


A  M > P :: z(r)B^{W,V} 
(2) 


A  0 :: B_{1}^{W1} Þ B_{2}^{W2,V2} 
(3) 


dl(0) Ç ëB_{1}û = Ø 
(4) 


B Í B_{1} 
(5) 
Since in (3) ëB_{2}û must be the empty set,
we conclude from (2) by choosing L = ëB_{1}û \ ëBû,
W' = W, and V' = V.
Let us assume


L' with S ® L' 


A  L' :: z(r)B^{W,V} 
(1) 


A  S :: B_{1}^{W1} Þ B_{2}^{W2, V2} 


dl(S) Ç ëB_{1}û = Ø 
(2) 


B Í B_{1} 
(3) 


B_{2}  ëB_{1}û Í B_{1} 
(4) 
A derivation of (1) must contain an instance of rule
Abstract, hence A  L' ::
z(r)B^{Ø,V} and ëBû = V = L' (5).
Let L be (dl(S) \ L') È (ëB_{1}û \
ëBû).
We show that (1) satisfies the lemma:

B Å (B_{2} \ L) =B.
Since by (4) B_{2} is compatible with B_{1} and with B by (3), it suffices to show that ëB_{2}û \ L Í ëBû.
By (5), it follows that L is equal to (dl(S) È ëB_{1}û)
\ ëBû (6).
Hence:

ëB_{2}û \ L 
= 
((ëB_{2}û  ëB_{1}û) È (ëB_{2}û \ ëB_{1}û))
\ L 

Í 
(ëB_{1}û È dl(S)) \ L 
by (4) and Lemma 8 

= 
(ëB_{1}û È dl(S))
\ ((ëB_{1}û È dl(S)) \ ëBû) 

= 
(ëB_{1}û È dl(S)) Ç ëBû 

 W Í W È (W_{2} Ç (ëB Å B_{2}û \
L)). Obvious.
 V Í V È (V_{2} Ç (ëB_{1}û \ L)). Obvious.
Inductive cases.
Let us assume


M > P with K_{1} Þ K_{2} > Q  S ® C' 
(1) 


dl(K_{1}) ¬ Ídl(M) 
(2) 


A  M > P :: z(r)B^{W,V} 
(3) 


A  K_{1} Þ K_{2} > Q  S ::
B_{1}^{W1} Þ B_{2}^{W2, V2} 
(4) 


((dl(K_{2}) \ dl(K_{1})) È dl(S)) Ç ëB_{1}û = Ø 
(5) 


B Í B_{1} 
(6) 


B_{2}  ëB_{1}û Í B_{1} 
(7) 
The selection clauses S are of the form _{iÎ I}K_{i}' Þ
K''_{i} > Q_{i}.
A derivation of (4) must contain an instance of Modifier, with premises:


A  K_{1} Þ K_{2} > Q :: B_{1}^{W1} Þ B_{2}'^{W2', V2'} 
(8) 


(A  K_{i}' Þ K_{i}'' > Q_{i} :: B_{1}^{W1} Þ
B_{i}''^{Wi'', Vi''})^{i Î I} 
where


B_{2}'' = 

Å_{i Î I} B''_{i} 




B_{2} = 

B_{2}' Å B_{2}'' 

(9) 


W_{2}'' = 

È_{iÎ I} W_{i}'' 




W_{2} = 

W_{2}' È W_{2}'' 

(10) 


V_{2}'' = 

È_{i Î I} V_{i}'' 




V_{2} = 

V_{2}' È V_{2}'' 

(11) 


Hence, by rule Modifier, we derive
A 
S ::
B_{1}^{W1} Þ B_{2}''
^{W2'', V2''}
(12)
A derivation of (1) must end with an instance of rule FilterNext, hence M > P with S ® C' (13).
By induction hypothesis applied to (13),
(3), (5),
(12), (6), and (7)
there must exist some L', W', and V' such that


A  C' :: z(r)(B Å (B''_{2} \ L'))^{W', V'} 
(14) 


L' Í (dl(S) \ dl(C')) È (ëB_{1}û \ ëBû) 
(15) 


W' Í W È (W''_{2} Ç (ëB Å (B''_{2}
\ L')û)) 
(16) 


V' Í V È (V''_{2} Ç (ëB_{1}û \ L')) 
(17) 
Let us prove that A  C' :: z(r)(B Å
(B_{2} \ L))^{W', V'} (18), for
L = L' È ëB'_{2}û \ (ëB_{1}û È ëB''_{2}û) and check that
L, W', V' satisfy the conditions of the lemma.
We first prove that L Í
(((dl(K_{2}) \ dl(K_{1})) È dl(S)) \
dl(C')) È (ëB_{1}û \ ëBû) (19).
By Lemma 8 applied to (8), we have
ëB_{2}'û\ ëB_{1}û Í dl(K_{2}) \ dl(K_{1}) (20).
Notice that
dl(C') = ëBû È ëB''_{2} \ L'û
by Lemma 7 and (14),
hence dl(C') Í ëBû È ëB''_{2}û (21).
Thus, we have:


L = 

L' È ëB'_{2}û \ (ëB_{1}û È ëB''_{2}û) 



= 

L' È (ëB'_{2}û \ ëB_{1}û) \ ëB''_{2}û 




Í 

L' È (dl(K_{2}) \ dl(K_{1})) \ ëB''_{2}û 

by (20) 


= 

L' È (dl(K_{2}) \ dl(K_{1})) \
(ëBû È ëB''_{2}û) 

by (5) 


Í 

L' È (dl(K_{2}) \ dl(K_{1})) \ dl(C') 

by (21) 


= 

(dl(S) \ dl(C')) È (ëB_{1}û \ ëBû)
È (dl(K_{2}) \ dl(K_{1})) \ dl(C') 

by (15) 


= 

((dl(K_{2}) \ dl(K_{1})) È dl(S)) \ dl(C')
È ëB_{1}û \ ëBû 

To conclude, we check the following properties:

B Å (B_{2} \ L) =B Å (B''_{2} \ L').
Since by (7) B_{2} and B_{1} agree, and so do B''_{2} and B
by (6) and (9), it suffices to check the equality of
their domains.
By
ëBû È (ëB_{2}û \ L) = 
ëBû È (ëB_{2}û \ (L' È ëB'_{2}û
\ (ëB_{1}û È ëB''_{2}û))) 
= 
ëBû È (ëB_{2}û \ (ëB'_{2}û \
(ëB_{1}û È ëB''_{2}û))) \ L' 
= 
ëBû È ((B'_{2} Å B''_{2}) \ (ëB'_{2}û
\ (ëB_{1}û È ëB''_{2}û))) \ L' 
= 
ëBû È ((ëB'_{2}û \ (ëB'_{2}û \ (ëB_{1}û
È ëB''_{2}û)))
È 

(ëB'_{2}û \ (ëB'_{2}û \ (ëB_{1}û È ëB''_{2}û)))
) \ L' 
= 
ëBû È ((ëB_{1}û È ëB''_{2}û)  ëB'_{2}û È B''_{2})
\ L' 
= 
ëBû È 

(ëB_{1}û  ëB'_{2}û) \ L' 


Í B 

È 

(ëB''_{2}û  ëB'_{2}û) \ L' 


Í
B''_{2} \ L' 

È (ëB''_{2}û \ L') 

= 
ëBû È (ëB''_{2}û \ L') 
 W' Í W È (W_{2} Ç ëB Å (B_{2} \
L)û). This follows from (16), W_{2}'' Í W_{2} (by
(10)), and B Å (B_{2} \ L) =B Å (B''_{2} \
L').
 V' Í V È (V_{2} Ç (ëB_{1}û \ L)).
This follows from (17), V_{2} Í V_{2}' (by (11))
and L' Í L (by definition of L').
Let us assume that:


C_{1} or C_{2} with S ® C' 
(1) 


A  C_{1} or C_{2} :: z(r)B^{W,V} 
(2) 


A  S :: B_{1} Þ B_{2}^{W2,V2} 
(3) 


dl(S) Ç ëB_{1}û = Ø 
(4) 


B Í B_{1} 
(5) 


B_{2}  ëB_{1}û Í B_{1} 
(6) 
A derivation of (2) must end with an instance
of rule
Disjunction, followed by a sequence of rules Sub. Hence B
is of the form B'_{1} Å B'_{2} (7) and:


A  C_{1} :: z(r)B'_{1}^{W'1, V'1} 
(8) 


A  C_{2} :: z(r)B'_{2}^{W'2, V'2} 
(9) 


W'_{1} È W'_{2} Í W 
(10) 


(V'_{1} \ (ëB'_{2}û \ V'_{2})) È
(V'_{2} \ (ëB'_{1}û \ V'_{1})) Í V 
(11) 
The condition (4) implies that
dl(S) Ç ëB_{i}û = Ø for i Î {1,2} (12).
The reduction (1) implies that C' is of the form C'_{1} or C'_{2}
such that C_{i} with S ® C'_{i} for i Î {1,2} (13).
By induction hypothesis applied to (13),
(8) and (9),
(3),
(12),
(5),
and (6),
it follows that
there exist some L_{i}, W''_{i}, and V''_{i} such that


A  C'_{i} :: z(r)(B'_{i} Å (B_{2} \ L_{i}))^{W''i, V''i} 
(14) 


L_{i} Í
(dl(S) \ dl(C'_{i})) È (ëB_{1}û \ ëB'_{i}û) 
(15) 


W''_{i} Í W'_{i} È (W_{2} Ç ëB'_{i} Å (B_{2}
\ L_{i}û)) 
(16) 


V''_{i} Í V'_{i} È (V_{2} Ç (ëB_{1}û \ L_{i})) 
(17) 
for i Î {1,2}.
By rule Disjunction applied to the two cases of (14)
and since B'_{1}, B'_{2} and B''_{2} are compatible by (6),
(5) and by the definition of B'_{1} and B'_{2}, we have:
A 
C'
_{1} or C'
_{2} ::
z(
r)(
B'
_{1} Å B'
_{2} Å (
B_{2} \
L_{1})
Å
(
B_{2} \
L_{2})
^{W', V'}
(18)
where


W' = 

W''_{1} È W''_{2} 



V' = 

V''_{1} \ (ëB'_{2} Å (B_{2} \ L_{2})û \ V''_{2})
È V''_{2} \ (ëB'_{1} Å (B_{2} \ L_{1})û \
V''_{1}) 

Let L be L_{1} Ç L_{2}. Then


L = 

L_{1} Ç L_{2} 



Í 

((dl(S) \ dl(C_{1})) È (ëB_{1}û \ ëB'_{1}û))
Ç ((dl(S) \ dl(C_{2})) È (ëB_{1}û \ ëB'_{2}û)) 

by (15) 


Í 

(dl(S) \ dl(C_{1})) Ç (dl(S) \ dl(C_{2})) È
(ëB_{1}û \ ëB'_{1}û) Ç (ëB_{1}û \ ëB'_{2}û) 

by distributivity 


= 

(dl(S) \ (dl(C_{1}) È dl(C_{2}))) È (ëB_{1}û \ (ëB'_{1}û È ëB'_{2}û)) 



= 

(dl(S) \ dl(C)) È (ëB_{1}û \ ëBû) 

(19) 
To conclude, we prove that (18) satisfies the constraints of
the lemma. Indeed, we have:

B Å (B_{2} \ L) = B'_{1} Å B'_{2} Å (B_{2} \
L_{1}) Å (B_{2} \ L_{2}). Since B = B'_{1} Å B'_{2} and
B_{2} \ L = B_{2} \ L_{1} Å B_{2} \ L_{2}.
 W' Í W È (W_{2} Ç ëB Å (B_{2} \
L)û). Since W' = W''_{1} È W''_{2}, it suffices to show that W''_{i}
Í W È (W_{2} Ç ëB Å (B_{2} \
L)û), for i Î {1,2}. This follows by (16), (10)
and because B'_{i} Å (B_{2} \ L_{i}) Í B Å (B_{2}
\ L) (by previous item).
 V' Í V È (V_{2} Ç (ëB_{1}û \ L)). It suffices
to show that both
V''_{1} \ (ëB'_{2} Å (B_{2} \ L_{2})û \ V''_{2})
Í V È (V_{2} Ç (ëB_{1}û \ L))
and
V''_{2} \ (ëB'_{1} Å (B_{2} \ L_{1})û \ V''_{1})
Í V È (V_{2} Ç (ëB_{1}û \ L))
Each of these two containments follows by (17), which establishes
a stronger relation between a superset of the left hand side
and two subsets of the two right hand sides.
Theorem 3 [Process Reduction]
Process rewriting ^{ }® preserves typing.
We show that
class reduction ^{x}® and
process reduction ^{ }® preserve typing, simultaneously.
That is, we prove that

if A + x : [r] , x.(B  F)  C:: z(r)B^{W,V} and C ^{x}® C'
then A + x : [r] , x.(B  F)  C':: z(r)B^{W,V};
 if A  P and P ® P' then A  P'.
Proof:
We reason by induction on the depth of the proofs of C ^{x}® C'
and P ® P'.
We write A_{x} for A + x : [r] , x.(B  F).
Basic cases for class reduction.
Let self(z) C ^{x}® C {z ¬ x} and let
A_{x}  self(z) C :: z(r)B^{W,V}.
A derivation of this judgment must end with an instance of
SelfBinding, followed by a sequence of Sub rules.
Hence,
A_{x} + z : [r] , z.(B  F)  C :: z(r)B ^{W',V'}
with W' Í W and V' Í V.
Then, by Lemma 5, we have:
A_{x}
 C {z ¬ x} :: z(r)B ^{W',V'}
We conclude A_{x}  C {z ¬ x} :: z(r)B^{W,V} by
rule Sub.
Let J_{1} or J_{2} > P ^{x}® J_{1} > P or J_{2} > P
and let A_{x}  J_{1} or J_{2} > P :: z(r)B^{W, V} (1).
The derivation of this judgment must end with the following
derivation followed by a sequence of Sub rules:
[Reaction] 
[Alternative] 
A'  J_{1} :: B_{1} A'  J_{2} :: B_{2} 


A'  J_{1} or J_{2} :: B 



A_{x} + A'  P dom( A') = fn( J_{1} or J_{2}) (2) 


A_{x}  J_{1} or J_{2} > P :: z(r)B^{cl(J1) È cl(J2), Ø} 


where B is B_{1} Å B_{2} and cl(J_{1}) È cl(J_{2}) Í
W. Since fn(J_{1} or J_{2}) = fn(J_{1}) =
fn(J_{2}), we have:
[Disjunction] 


A'  J_{i} :: B_{i} A_{x}+ A'  P dom(A') = fn(J_{i}) 


A_{x}  J_{i} > P :: z(r)B_{i}^{cl(Ji), Ø} 


i = 1, 2 




A_{x}  J_{1} > P or J_{2} > P :: z(r)B^{cl(J1)
È cl(J2), Ø} 


The we conclude A_{x}  J_{1} > P or J_{2} > P :: z(r)B^{W,
V} by rule Sub.
Let C or L ^{x}® C or L' and A_{x}  C or L :: z(r)B^{W,V} and L' = L \ dl(C), with L ¹ L'.
Therefore L' Í L (1).
The derivation of the judgment A_{x}  C or L :: z(r)B^{W,V} must end with the following derivation followed by a
sequence of Sub rules:
[Disjunction] 
[Abstract] 


A_{x}  L :: z(r)B_{2}^{Ø, L} 


A_{x} C :: z(r)B_{1}^{W1,V1} 

L'' = L \ ( dom( B_{1}) \ V_{1}) (2) 


A_{x}  C or L :: z(r)(B_{1} Å B_{2})^{W1, V1 È L''} 


where B = B_{1} Å B_{2}, W_{1} Í W (3) and
V_{1} È L'' Í V (4).
We first observe that B_{1} Å B_{2} = B_{1} Å (B_{2}  L').
Therefore we can derive:
[Disjunction] 
[Abstract] 


A_{x}  L' :: z(r)(B_{2}  L')^{Ø, L'} 


A_{x} C :: z(r)B_{1}^{W1,V1} 

L''' = L' \ ( dom( B_{1}) \ V_{1}) (5) 


A_{x}  C or L' :: z(r)(B_{1} Å B_{2})^{W1, V1 È L'''} 


By (2), (5) and (1), we derive V_{1} È L'''
Í V_{1} È L''. Hence, by (3), (4) and
rule Sub, we obtain
A_{x}  C or L' :: z(r)(B_{1} Å B_{2})^{W, V}.
Let C or Ø ^{x}® C and
A_{x}  C or Ø :: z(r)B^{W,V}. The derivation of this
judgment must end with rule Disjunction followed by a sequence of
Sub rules:
[Disjunction] 
A_{x}  C :: z(r)B^{W', V'} A_{x} Ø :: z(r)Ø^{Ø, Ø} 


A_{x}  C or Ø :: z(r)B^{W',V'} 


where W' Í W and V' Í V. Then, by rule
Sub applied to A_{x}  C :: z(r)B^{W',V'}, we
obtain A_{x}  C :: z(r)B^{W,V}.
Basic cases for processes.
Let us assume A  class c = self(z) C in P (1) and
class c = C in P ® P {x ¬ C}.
The final part of the derivation of (1) must have the
form
Class 
A  C :: z( r) B^{W,V} (2) 
A + c : " Gen ( r, B, A). z( r) B^{W,V}  P (3) 



By Lemma 6 applied to (2)
and (3), we derive A  P {c ¬ C}.
Inductive cases for classes.
Let A_{x}  E {C} :: z(r)B^{W,V} and
E {C} ^{x}® E {C'}. By inductive hypothesis, if
A_{x}  C :: z(r)B'^{W', V'} then A_{x}  C' :: z(r)B'^{W',V'}, since C ^{x}® C'. The judgment A_{x}  E {C'} :: z(r)B^{V} follows by induction on the structure of E
{·}. The details are omitted.
Let us assume that A  match C with S end : z(r)B^{W, V} (1) and match C with S end ¾® C' (2). We must prove that
A  C' : z(r)B^{W, V} (3)
A derivation of (1) must end with an instance of rule
Refinement followed by a sequence of Sub.
Hence, B is of the form B_{1} Å B_{2} (4) and


A  C :: z(r)B_{1}^{W1, V1} 
(5) 


A  S :: B_{1}^{W1} Þ B_{2}^{W2, V2} 
(6) 


dl(S) Ç dom(B_{1}) = Ø 
(7) 


W_{1} È W_{2} Í W 
(8) 


V_{1} È V_{2} Í V 
(9) 
The derivation of (2) must contain a rule Match with the
premises:
From (4) it follows that B_{2}  dom(B_{1}) Í dom(B_{2}) (12).
Lemma 9 applied to (10),
(5), (6), (7), and (12)
implies that


A  C' :: z(r)(B_{1} Å (B_{2} \ L))^{W',V'} 
(13) 


L Í (dl(S) \ dl(C')) È ( dom(B_{1}) \ dom(B_{1})) 
(14) 


W' Í W_{1} È (W_{2} Ç dom(B_{1} Å (B_{2} \
L))) 
(15) 


V' Í V_{1} È (V_{2} Ç ( dom(B_{1}) \ L)) 
(16) 
The property (11) combined with (14)
imply that L is empty. Therefore W' Í W_{1} È W_{2}
and V' Í V_{1} È V_{2}.
Hence (3) follows by (13),
(8), (9) and rule Sub.
Inductive cases for processes.
Let A  obj x = C init P in Q (1) and
obj x = C init P in Q ^{ }® obj x = C' init
P in P', under the assumption that C ^{x}® C' (2).
A derivation of (1) has the shape
[Object] 
[SelfBinding] 
A + x : [ r], x :( B  F)  C :: z( r) B^{W,Ø} (3) 


A  self(x) C :: z(r)B^{W,Ø} 



r = B  M X= Gen (r, B, A) \ ctv(BW) 
A + x : " X. [r], x : " X. (B  F)  P A + x : " X. [r]  Q 


A  obj x = C init P in Q 


By induction hypothesis applied to (2) and (3), we
obtain the judgment A + x : [r], x :(B  F)  C' :: z(r)B^{W,Ø},
which we can substitute in the previous derivation, thus
concluding A  obj x = C' init P in Q.
Proof:
Let us assume  ( D  P).
By ChemicalSolution and
Definition,  ( D  P) holds provided
( A^{y} D :: A_{x}) ^{y x # D Î D} (1) 
( A^{y} P) ^{y # P Î P} (2) 
A = È_{y x # D Î D} A_{x} (3) 
We check that no case listed in
Definition 1 (Section 6.1)
can occur.
No free variables.
By definition of type judgments, since (1) hold,
every free object name in D, with y x # D Î D,
should appear as a leaf of the proof tree of A^{y} D :: A_{x}.
This leaf must be of the form A^{y}+ A'  x : t. This implies
that x belongs to the domain of A^{y} because x is free in D.
Similarly, every class variable in D should belong to the domain of A^{y},
which actually only contains object names.
The proof is similar for free names in P using (2).
No runtime failure.
Let y # x. l (u) Î P
and
y' x # D Î D (4).
 (no privacy failure)
Let l be a private label f. We prove that y'x is a
prefix of y. A derivation of A^{y}  x.l (u_{i}^{i Î I}) must be:
[Send] 
((5)) 


A^{y}  x.f : (t_{i} ^{i Î I}) 


(A^{y}  u_{i} : t_{i})^{i Î I} 



A^{y}  x.l (u_{i}^{i Î I}) 


where (5) is an instance of PrivateMessage. The premise
of (5) requires that x : " X.(l : (t_{i}^{i Î I}); B') be in A^{y}. Therefore, by definition of A^{y}, variable x must
appear in y. Furthermore, by wellformedness of chemical solutions, a
name can have a unique prefix. Since y' is already a prefix of x, then
y must be of the form y' x y''.
 (no undeclared label) We show that l Î dl(D).
Given (4), the judgment A^{y'}  D :: A_{x}, where
A_{x} = x: " X. r, x: " X.(B  F ),
follows by rule Definition applied to (1) with the premises
below:
A^{y'}  self( x) D :: z( r) B^{W,Ø} (6) 
X = Gen (r, B, A^{y'}) \ ctv(BW) 
Since A^{y} x.l (u) by (2), either r is of the form [l : t; r'] or B is of the
form (l : t; B') depending on whether l is public or
private. In each case, using (7), l is in dom(B).
The conclusion follows by Lemma 7.
 (no arity mismatch)
Let D be of the form [M > P] where M is itself
of the form l(y) & J. We show that y and u have the
same arities.
For that purpose, it suffices to show that the type of u and
the type of y in A are instances of a same tuple type.
A leaf of (6) must be
[Reaction] 


( 

MessagePattern
(y_{i} : t'_{i} Î A')^{i Î I} 


A'  l (y):: l : (t'_{i}^{i Î I}) 



) 



 


dom(A') = fn(M) A^{y'} + x : [r], x : (B  F)+ A'  P 




A^{y'} + x : [r], x : (B  F)  M > P :: z(r)B^{cl(M),Ø} 


Therefore, the type of y in A' is B(l). By rules
ChemicalSolution and Definition, A contains a
generalization of
x : [r], x : (B  F).
Thus,
the type of x.l in A^{y} is a generalization of B(l). The proof tree illustrated
in item 1 is required to prove A^{y}  x.l (u_{i}^{i Î I}).
Then, as a consequence of rule (5),
the type of u is an instance of the type of x.l in A^{y}, i.e. of the generalization of the type of y in A'.
No class rewriting failure.
Let y # P Î P, P = obj x = C init Q in Q', rule
ClassRed does not apply to P, i.e. there is no C' such that C
^{x}® C',
and P is not a refinement error. We show that P is not a failure;
namely, for every evaluation context E,

C ¹ E{c}, and c is free.
By (1), dom(A) only contains object names. Therefore, by (2),
P cannot contain free class names.
 Let E {L} = C' or L (the case
E {L} = L or C' is similar). We demonstrate that, if A'  C' or L
:: z(r)B^{W,V} then L Í V.
By rule Abstract, A'  L :: z(r)B_{1}^{Ø,L} (8).
Let A'  C' :: z(r)B_{2}^{W2,V2} (9) and
V_{1}' = L \( dom(B_{2}) \ V_{2}) (10) and
V_{2}' = V_{2} \( dom(B_{1}) \ L) (11).
Since there does not exists C'' such that C ^{x}® C'',
the rule AbstractCut cannot be applied.
This means that L = L \
dl(C') = L \ dom(B_{2}), which implies V_{1}' = L. By (8),
(9), (10), (11) and rule Disjunction we obtain
A'  C or L :: z(r)(B_{1} Å B_{2})^{W1 È W2, L È
V2'} (12).
On the other hand, by (2), a derivation of A^{y} P
must contain (P = obj x = C init Q in Q')
[Object] 
[SelfBinding] 
A^{y}+ x : [ r], x.( B  F)
 ( C' or L) :: z( r) B^{W,Ø}(13) 


A^{y} self(x) (C' or L) :: z(r)B^{W,Ø} 



r = B  M X= Gen (r, B, A) ctv(BW) 
A^{y}+ x : " X. [r], x : " X. (B  F)  Q A^{y}+ x : " X. [r]  Q' 


A  obj x = (C' or L) init Q in Q' 


To conclude, observe that (12) and (13) do not unify because
virtual labels in (12) are not empty.
 *
 Microsoft Research, 1 Guildhall Street, Cambridge, U.K.
 #
 Dipartimento di Scienze dell'Informazione, Università
di Bologna, Mura Anteo Zamboni 7, 40127 Bologna, Italy
 %
 INRIA Rocquencourt, BP 105, 78153 Le Chesnay Cedex France.
 1
 In the plain join calculus, this problem is less acute: for
a given definition, each entry point is passed as a separate name,
so lexical scoping on private names provides some privacy; on the other
hand, large tuples of public names must be passed instead
of single objects (see Appendix A.)
 2
 In Ocaml, objects are
kept monomorphic for simplicity, and
polymorphic functions are usually defined outside of objects.
 3
 We could use more
general approximations, e.g., we could discard labels whose types
have no free variable as we compute é Kù from K. However, such
generalizations complicate type inference, which
becomes sensitive to the ordering of type variable instantiations.
This document was translated from L^{A}T_{E}X by
H^{E}V^{E}A.