Single HTML file   Postcript or PDF   (FSTTCS'00, Slides)

Inheritance in the Join Calculus

Cdric Fournet*   Cosimo Laneve#   Luc Maranget%   Didier Rmy%
April 23, 2004




Abstract: We design an extension of the join calculus with class-based 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.
Table of Contents

1 Introduction

The join calculus is a simple name-passing 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 object-oriented 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 well-known objects-as-records 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 language---the objective join calculus---allows fine-grained 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 compile-time 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 run-time. 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 encapsulation1. 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 trade-off 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 cross-encodings 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.

2.1 Getting started
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 rendez-vous, 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 previously-defined 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 self-inflicted 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 one-place 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.

2.2 Syntax
We use two disjoint countable sets of identifiers for object names x, z, u O and labels l L. Tuples are written xii 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 P1 in P2 by omitting init P1 when P1 is 0.
Figure 1: Syntax for the core objective join calculus
  P ::=     Processes  
    0   null process
    x.M   message sending
    P1 & P2   parallel composition
    obj x = D init P1 in P2   object definition
  D ::=     Definitions  
    M |> P   reaction rule
    D1 or D2   disjunction
  M ::=     Patterns  
    l(u)   message  
    M1 & M2   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 P1 in P2 binds the name x to D. The scope of x is every guarded process in D (here x means ``self'') and the processes P1 and P2. 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 a-conversion).

2.3 Chemical semantics
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
Par
||- P   &   Q ||- PQ

Nil
||- 0 ||-

Obj
||- obj x = D init P in Q x. D ||- PQ

Join
||- x.(M & M') ||- x.Mx.M'

Red
x.[ M |> P] ||- x.Ms x.[ M |> P] ||- Ps

Chemistry
D0 ||- P1 stackrel D0 ||- P2
D, D0 ||- P1, P stackrel D, D0 ||- P2, P

Chemistry-Obj
||- 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 a-conversion 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 Chemistry-Obj. In rule Chemistry, the symbol stackrel stands for either or . In rule Chemistry-Obj, 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 one-place 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 late-binding 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.

3.2 Syntax

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 associative-commutative 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
    P1 & P2   parallel composition
    obj x = C init P1 in P2   object definition
    class c = C in P   class definition
  C ::=     Classes  
    c   class variable  
    L   abstract class  
    J |> P   reaction rule
    C1 or C2   disjunction
    self(xC   self binding
    match C with S end   selective refinement
  S ::=     Refinement clauses  
    (K1 K2 |> P) | S   refinement sequence
      empty refinement
  J ::=     Join patterns  
    l(u)   message  
    J1 & J2   synchronization  
    J1 or J2   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 associative-commutative, & distributes over or, and 0 is the unit for &. Hence, every pattern K can be written as an alternative of patterns ori I Mi. We sometimes use the notation K1 & K2 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 (Ki Ki' |> Pi)) = i I fn(Pi) \ fn(Ki')
  dl(|i I (Ki Ki' |> Pi)) = i I dl(Ki') \ dl(Ki)
In classes C:
  fn( c ) = { c }
  fn( L ) =
  fn( J |> P) = fn( P ) \ fn( J )
  fn( C1 or C2 ) = fn(C1) fn(C2)
  fn( self(zC ) = fn(C) \ { z }
  fn( match C with S end ) = fn(C) fn(S)
  dl( c ) =
  dl( L ) = L
  dl( J |> P ) = dl( J )
  dl( C1 or C2 ) = dl( C1 ) dl( C2)
  dl( self(zC ) = 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 well-formedness conditions:
  1. All conjuncts Mi 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(Mi) bound in each Mi, and write fn(K) for these names.

  2. In a refinement clause K1 K2 |> P, the pattern K1 is either M or 0, the pattern K2 binds at least the names of K1 (fn(K1) fn(K2)), and K1 is empty whenever K2 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 K1 K2 |> P, the selection pattern K1 binds fn(K1) with scope K2 and P; the modification pattern K2 binds fn(K2)\ fn(K1) with scope P. Finally, self(xC 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 a-conversion.

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 ( |- )
Class-Subst
class c = C in P |- P {C/c}

Class-Red
C |-x C'
obj x = C init P in P' |- obj x = C' init P in P'
Rules for classes ( |-x )
Self
self(zC |-x C {x/z}
Or-Pat
J or J' |> P |-x J |> P or J' |> P

Class-Abstract
C or |-x C
Abstract-Cut
L' = L \ dl(C)      L L'
C or L |-x C or L'

Match
C with S   |-   C'      dl(S) dl(C')
match C with S end   |-x   C'
Class-Context
C |-x C'
E[C] |-x E[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

Filter-Apply
K1 & K |> P with K1 K2 |> Q | S   |-   K2 & K |> P & Q or dl(K1) \ dl(K2)

Filter-Next
M |> P with S
     |      
C'      dl(K1) dl(M)
M |> P with K1 K2 |> Q | S  
     |      
  C'

Filter-End
C with   |-   C
Filter-Or
C1 with S   |-   C1'      C2 with S   |-   C2'
(C1 or C2) with S   |-   C1' or C2'

Filter-Abstract
L with S   |-   L

The semantics of classes is defined by reduction to the core calculus. The rules are given in Figure 5. Rules Class-Subst and Class-Red describe class rewritings for processes. Rule Class-Red 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 Or-Pat lifts or constructs from patterns to classes. The next two rules for classes simplify abstract classes, rule Class-Abstract discards empty abstract classes; rule Abstract-Cut 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 Class-Context 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 sub-pattern of M (rules Filter-Next and Filter-Apply). If no clause of S matches M, then the reaction rule is left unchanged (rule Filter-End). Abstract classes L in C are also left unchanged (rule Filter-Abstract).

Note that rule Filter-Apply can be used only if the pattern K2 & K introduced by rule Filter-Apply is well-formed, i.e., (1) K2 and K are not both empty, (2) fn(K2) fn(K) = , and (3) dl(K2) dl(K)= . Condition (1) is enforced by syntactic restriction 2 of Section 3.2. Condition (2) can be enforced by a-conversion. 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 Filter-Apply removes the labels dl(K1) \ dl(K2). To prevent those labels from being undeclared in C', rule Filter-Apply 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 Filter-Apply introduces the labels dl(K2) \ dl(K1). 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 Class-Subst, 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 Class-Red does not apply to P. One of the following holds:
Completion:
C is a disjunction of reaction rules (C = ori = 1n Mi |> Pi).
Failure:
For some evaluation context E, we have:
  1. C = E{c} and c is free (undefined class).
  2. 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 Or-Pat duplicates reaction rules whose patterns contain alternatives. Alternatively, we could have supplemented the object calculus with or-patterns, but we view this as an optimization issue. Perhaps more importantly, the unsharing of reaction rules performed by rule Or-Pat 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 abstraction---method names and signatures are known, method bodies are abstract---does 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, object-oriented 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 well-known 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 i-th 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, n-1)
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 non-full, and to messages on get when non-empty; 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, n-2)
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.

History-dependent 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, n-1)
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 general-purpose 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 pattern-matching, 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 one-place 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 self-referencing 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 approach---the one that we followed---names and slots are in a one-to-one 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 higher-level language. (Indeed, examples of Section 4 conform with this approach.)

In the user-language we replace class and obj declarations by the following ones: The translation of the above declarations are, respectively: 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 Filter-Apply 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.

6 Types and privacy

The static semantics of our calculus extends those of the core join calculus for concurrency and synchronization [12] and of OCaml for the class-layer [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 message-not-understood 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 y1... yn x indicates that object x was created within the definition (or the init process) of objects y1, ..., yn 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 well-formed 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 ori = 1n Mi |> Pi; 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 Chemistry-Obj 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 Public-Comm and Private-Comm 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

Nil
||- y   #  0 ||-

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   #  Py   #  Q

Public-Comm
y x   # D ||- y'   #  x. m(u) y x   # D ||- y x   #  x. m(u)

Private-Comm
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
D0 ||- P1 stackrel D0 ||- P2
D, D0 ||- P1, P stackrel D, D0 ||- P2, P

Chemistry-Obj
||- 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 Private-Comm). We take the presence of non-routable 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
  1. Failed privacy: l F and y' is not a prefix of y.

  2. Undeclared label: l dl(D).

  3. 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.

6.2 Type expressions

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 ::= (tii 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 rendez-vous 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 l1 : t1; ... ln : tn; by l1 : t1; ... ln : tn and we abstract away from the order of labels l1,... ln. For a given set of labels L, we write B | L for the restriction of B to the labels of L. We also write B1 B2 for the union of B1 and B2, with the statement that B1 and B2 coincide on their common labels, and state B1 B2 when there is B1' such that B1 B1' = B2. We write dom(B) for the set of labels listed in B.

Class types have the form " X. z(r)BW,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 calculus2.

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 = ori I Mi, we let cl(K) = i I cl(Mi).

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) =
 
l l'
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 non-generalizable 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 potentially-coupled 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 well-typed K & K'', written cls(BW,K K'). The definition is by cases:
  1. If K' = 0, we use cls(BW,K K') = W.
    (In this case, no new message with arguments is introduced.)

  2. If dl(K) W = and K 0, we use cls(BW,K K') = cl(K').
    (In this case, K is a single message and K'' is empty.)

  3. If dl(K) W , we use cls(BW,K K') = dl( K') W.
    (In this case, all labels in K'' already appear in W.)

  4. Otherwise ( K = 0 and K' 0), we use cls(BW,K K') = dl( K') dom( B).
Note that cls(BW,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 BW 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(BW, 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(BW, 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 well-typed in environment A;
A |- K :: B the pattern or selection pattern K binds variables well-typed in A and joins labels in B.
A |- C :: z(r)BW, V the class C is well-typed 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 :: BW B'W', V
  the refinement clauses S are well-typed 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 gaa 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
Object-Var
x : " X. t A
A |- x : t {a gaa X}
Message
A |- x : [ m : t; r ]
A |- x.m : t

Private-Message
x : " X. (f : t; B) A
A |- x.f : t{a gaa X}
Rules for processes
Null
A |- 0
Send
A |- x.l : (ti i I)      (A |- xi : ti) i I
A |- x.l (xi i I)

Join-Parallel
A |- x.M1    A |- x.M2
A |- x.(M1 & M2)
Parallel
A |- P    A |- Q
A |- P & Q

Class
A |- C :: z(r)BW,V
A + c : " Gen (r, B, A). z(r)BW,V |- P
A |- class c = C in P

Object
    
A |- obj x = C init P in Q

Figure 10: Typing rules for patterns, classes, and refinement clauses 
Rules for patterns
Empty-Pattern
A |- 0 ::
Message-Pattern
(xi : ti A)i I
A |- l(xi i I) :: (l : tii I)

Synchronization
A |- J1 :: B1      A |- J2 :: B2
A |- J1 & J2 :: B1 B2
Alternative
A |- J1 :: B1      A |- J2 :: B2
A |- J1 or J2 :: B1 B2
-2
Rules for classes
Sub
A |- c :: z(r)BW,V
A |- c :: z(r)BW W', V V'
Class-Var
c : " X. z(r)BW,V A
A |- c :: (z(r)BW,V) {a gaa X}

Reaction
A' |- J :: B      A + A' |- P      dom(A') = fn(J)
A |- J |> P :: z(r)Bcl(J),

Self-Binding
A + x : [r],   x : (B | F) |- C :: z(r)BW,V
A |- self(xC :: z(r)BW,V
Abstract
dom(B) = L
A |- L :: z(r)B, L

Disjunction
A |- C1 :: z(r)B1W1, V1      V1' = V1 \ ( dom(B2) \ V2)
A |- C2 :: z(r)B2W2, V2      V2' = V2 \ ( dom(B1) \ V1)
A |- C1 or C2 :: z(r)(B1 B2)W1 W2, V1' V2'

Refinement
A |- C :: z(r)B1W1, V1
A |- S :: B1W1 B2W2, V2      dl(S) dom(B1) =
A |- match C with S end :: z(r)(B1 B2)W1 W2, V1 V2
-2
Rules for refinement clauses
Modifier-Clause
    
A |- K K' |> P :: BW B' W', dl(K) \ dl(K')

Modifier
(A |- Si :: BW BiWi, Vi)i I
A |- | i I Si :: BW (i IB'i)
 
i I
Wi,
 
i I
Vi
 

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)BW,. The shape of this type excludes virtual labels, thus preventing the instantiation of a partially-defined 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 well-formed, 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 Self-Binding folds two bindings for self, accounting for public and private bindings, respectively. Rules Disjunction and Refinement merge virtual-label 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 :: B1W1 B2W2, V2; This premise will ensure that labels in the selection patterns are all defined in B1, hence declared in C. On the contrary, the premise dl(S) dom(B1) = 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 Ki' agree with those Ki 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 well-typed. The auxiliary judgments A |- D :: A' deals with active object definitions. The typing rules appear in Figure 11.

Rule Chemical-Solution uses an additional notation Ay. Let N be a set of object names and A be a typing environment of the form
A =
 
x N
(x : sx)
 
x N
(x: " Yx. Bx)
For any string y of names in N, we define the restricted environment:
A y =
 
x N
(x : sx)
 
x y
(x : " Yx. Bx)
Namely, Ay 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
Chemical-Solution
A = y x   # D    D   Ax
(Ay |- D :: Ax)y x   # D    D
(Ay |- P)y   # P    P
|- D ||- P
Definition
r = B | M
X = Gen (r, B, A) \ ctv(B|W)
A |- self(xD :: z(r)BW,
A |- D :: x : " X. [ r ], x : " X. (B | F)

Rules Chemical-Solution 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 type-checking 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]  
  1. Chemical reductions preserve chemical typings:
    if |-
    D ||- P and D ||- P D' ||- P' or D ||- P D' ||- P', then |- D' ||- P'.

  2. 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 well-typed and D ||- P   ( stackrel |)*   D' ||- P', then D' ||- P' is also well-typed.

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]   Well-typed 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.

6.7 Example of typing

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)  (J1 |> P1 or J2 |> P2). First, consider the typing of pattern J1. By rules Message-Pattern and Synchronization we have:
A1 |- get(r) & Some(a) :: B1     (1)
where the type environment A1 and internal type B1 are A1 = r:q1, a:q2 and B1 = get : (q1) ; Some : (q2), reflecting the presence of labels and their arities.

However, pattern J1 is not typed in isolation but as the pattern of a reaction rule whose guarded process P1 includes r.reply(a). Rule Reaction requires that P1 be typed in an environment that subsumes A1. Moreover, r.reply(a) connects the types for r and a (rule Send). Thus, we get: q1 = [ reply : (q) ; h ] (reflecting that r is an object with at least a reply label) and q2 = q. Then, the type variable q is free in the types of both Some and get which are joined in the same pattern J1. Skipping some details, rule Reaction yields the following typing of J1 |> P1:
A |- J1 |> P1 :: z(r)B1{get, Some},     (2)
where r is the public type for self, A is described below, and B1 is get : ([ reply : (q) ; h ]) ; Some : (q). Similarly, the second reaction rule is typed as:
A |- J2 |> P2 :: z(r)B2     (3)
where B2 = put : (q',[ reply : () ; h' ]) ; Empty : (). Note that the set of coupled labels is empty, since pattern J2 contains only one label of non-zero arity.

Environment A must be the same in both (2) and (3) because these two judgments are premises of a Disjunction rule:
A |- J1 |> P1 or J2 |> P2 :: z(r)B{get,Some},      (4)
The internal type B is B1 B2. Here, this amounts to B1 B2 since patterns J1 and J2 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 Self-Binding implies that environment A contains two bindings for the self name z, namely, z:[r] and z:Br. The internal type of z, Br is the restriction of B to private labels, i.e. we get Br= Some : (q) ; Empty : ().

We can now detail the typing for P2 (which is an hypothesis for (3)). Listing only pertinent parts of the typing environment A + A2, we have:
... a:q', z:(Some:(q), ...) |- P2     (5)
Now, observe that P2 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 object-oriented 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 operator---the let---which 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 programming-language 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 object-oriented 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 non-empty 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], non-generalizable type variables were computed altogether for all clauses of a definition, which may be too conservative. In both [15] and [7], non-generalizable 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 x1 = a1 and x2 = a2 in a as let x = fix (l (x1,x2). (a1, a2)) in a. The latter term separates type-checking the body of the recursion from type-checking 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.

8 Conclusion

We have designed a simple, object-based 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 classes---a 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 Franois Pottier.

References
[1]
G. Agha, P. Wegner, and A. Yonezawa. Research Directions in Concurrent Object-Oriented Programming. MIT Press, 1993.

[2]
P. America. Issues in the design of a parallel object-oriented language. Formal Aspects of Computing, 1(4):366--411, 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 406--421, 1996.

[5]
G. Bracha and W. Cook. Mixin-Based Inheritance. In N. Meyrowitz, editor, European Conference on Object-Oriented Programming: Systems, Languages, and Applications, pages 303--311, Otawa, 1990. ACM press.

[6]
L. Cardelli. Obliq A language with distributed scope. Computing Systems, 8(1):27--59, 1995.

[7]
G. Chen, M. Odersky, C. Zenger, and M. Zenger. A functional view of join. Technical Report ACRC-99-016, University of South Australia, 1999.

[8]
S. Dal-Zilio. Quiet and bouncing objects: Two migration abstractions in a simple distributed blue calculus. In H. Httel and U. Nestmann, editors, Proceedings of the Worshop on Semantics of Objects as Proceedings (SOAP '98), pages 35--42, June 1998.

[9]
C. Fournet. The Join-Calculus: 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 join-calculus. In Proceedings of POPL '96, pages 372--385, Jan. 1996.

[11]
C. Fournet, G. Gonthier, J.-J. Lvy, L. Maranget, and D. Rmy. 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 406--421, 1996.

[12]
C. Fournet, C. Laneve, L. Maranget, and D. Rmy. Implicit typing la ML for the join-calculus. In A. Mazurkiewicz and J. Winkowski, editors, Proceedings of the 8th International Conference on Concurrency Theory, LNCS 1243, pages 196--212, 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). North-Holland, 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 join-patterns. In Nestmann and Pierce [22].

[17]
X. Leroy, D. Doligez, J. Garrigue, D. Rmy, 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 object-oriented concurrent programming languages. In G. Agha, P. Wegner, and A. Yonezawa, editors, Research Directions in Concurrent Object-Oriented Programming, chapter 4, pages 107--150. 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 object-oriented programming. In O. M. Nierstrasz, editor, 7th European Conference on Object Oriented Programming, number 707 in LNCS, pages 220--246. 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:1--40 and 41--77, Sept. 1992.

[22]
U. Nestmann and B. C. Pierce, editors. HLCL '98: High-Level 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 Object-Based Concurrent Computing, LNCS 612, pages 1--20, 1992.

[24]
M. Odersky. Functional nets. In Proc. European Symposium on Programming, number 1782 in LNCS, pages 1--25. 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. Rmy and J. Vouillon. Objective ML: A simple object-oriented extension to ML. In Proceedings of POPL '97, Jan. 1997. Available electronically at ftp://ftp.inria.fr/INRIA/Projects/cristal/ Didier.Remy/objective-ml!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 p-calculus. Information and Computation, 143(1):34--73, 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 100--117. Springer-Verlag, 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 pi-calculus. Information and Computation, 116(2):253--271, 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. Object-oriented concurrent programming in ABCL/1. ACM SIGPLAN Notices, 21(11):258--268, Nov. 1986. Proceedings of OOPSLA '86.
A Cross-encodings 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 cross-encodings 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 single-label forwarder objects and passing those object names instead of channel names. (The encoding given below works for non-recursive definitions in the join calculus; recursive definitions can easily be eliminated beforehand [9].)
[[0]] = 0
[[x (u)]] = x.send (u)
[[P1 & P2]] = [[P1]] & [[P2]]
[[ defD in P]] = obj o = [[D]] in
    obj x1 = send (u1) |> o.m1 (u1) in ...
    obj xn = send (un) |> o.mn (un) in [[P]]
where we assume that D defines the channel names x1, ..., xn. Accordingly, we encode channel reaction rules and patterns as follows:
[[D1 or D2]] = [[D1]] or [[D2]]         [[M1 & M2]]- = [[M1]]- & [[M2]]-
[[M |>P]] = [[M]]-|> [[P]]         [[x (u)]]- = mx(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 {li = xi}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)
[[P1 & P2]] = [[P1]] & [[P2]]
[[ obj x = D \ init P1 in P2]] = ( def[[D]]x in [[P1 & P2]]) {x {l = xl, l dl(D)}}
[[D1 or D2]]x = [[D1]]x or [[D2]]x         [[M1 & M2]]x = [[M1]]x & [[M2]]x
[[M |> P]]x = [[M]]x |> [[P]]         [[l (u)]]x = xl(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.

B Proofs for typing



B.1 Basic properties

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 : [mi : ti i I], x : (l : tll S) |- D and A |- y : t, (A |- y.mi : ti) i I, and (A |- y.l : tl)l S then A |- D{x y}.

Lemma 6  [Substitution of a class name in a term]   Let A + c : " X . z(r)BW,V |- D and A + B |- C :: z(r)BW,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':
  1. an instance of rule Obj, followed by a sequence of Chemistry-Obj;

  2. an instance of one of the rules Par, Nil, Public-Comm, Private-Comm, 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 Chemical-Solution, we obtain (Aj |- D' :: Az)j z   #  D' D (2), Ay |- obj x = D init P in Q and (Aj |- P')j   #  P' P (3), where A = j z   #  D' D   Az. A derivation of Ay |- obj x = D init P in Q must have the form:
[Object]
Ay |- self(xD :: z(r)B W, (4)
X = Gen (r, B, Ay) \ ctv(B|W(5)      Ay + x : " X. [r], x : " X. (B | F) |- P (7)
r = B | M (8)      Ay+ x : " X. [r] |- Q (9)
Ay |- 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 Chemical-Solution, 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(xD :: z(r') B'W',  (15)
r' = B' | M (16)      X' = Gen (r', B', A'y) \ ctv(B'|W') (17)
A'y |- D :: A'x
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 = Ay + x : " X'.   [r'], the following premises can be made equivalent to one another: 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 ||- P1,   P stackrel D ||- P2,   P. There are several subcases, according to the leaf node in the proof tree.

Nil.
The equivalence is D ||- y   #  0, P D ||- P. Indeed the judgment A |- y   # 0 is always true, for any environment A.

Par.
The equivalence is D ||- y   # (P & Q), P D ||- y   #  P, y   #  Q, P. We apply rule Chemical-Solution, then it suffices to prove that the two judgments Ay |- P & Q and Ay |- P, Ay |- Q are equivalent. This follows by rules Parallel and Chemical-Solution.

Join.
This is similar to the above case, and relies on rules Chemical-Solution, Parallel and Join-Parallel.

Public-Comm.
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 Ay |- D :: Ax and Ay' |- x. m(u(1). We must show that Ay x |- x.m (ui i I) where u = ui i I. A complete derivation of (1) must be of the form:
[Send]
[Message]
[Object-Var]
...
Ay' |- x : [ m : (ti i I); r ]
Ay' |- x.m : (ti i I)
     (
Object-Var    
...
Ay' |- ui : ti
) i I
Ay' |- x.m (ui i I)
This derivation, which does not use any internal type assumption of A (any Private-Message rule), is not affected by replacing Ay' with Ay x. Thus, Ay x |- x.m (ui i I) holds.

Private-Comm.
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 Ay |- D :: Ax and Ay x y' |- x. f(u(1). We must show that Ay x |- x.f (ui i I) where u = ui i I. A complete derivation of (1) must be of the form:
[Send]
Private-Message    
x : " X. (f : (ti i I); B) Ay x y'
Ay x y' |- x.f : (ti{a gaa X}i I)
     (
Object-Var    
...
Ay x y' |- ui : ti {a gaa X}
) i I
Ay x y' |- x.f (ui i I)
Note that, the only internal type assumption in the premise is on x, which remains in Ay x. Thus, as in case Public-Comm, we can replace Ay x y' by Ay x in this derivation and conclude that Ay x |- x. f(ui i I).

Red.
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 Ili(xi). A derivation of |- ( D, y x   #  D ||- y x   #  x.(Ms), P) must follow from rule Chemical-Solution with the following premises:
A = (j z   #  D'' D Az) Ax (1)
(Aj |- D'' :: Az) j z   #  D'' D (2)
Ay |- D :: Ax (3)
Ay x |- x.(M s) (4)
(Aj |- P')j   #  P' P (5)
The derivation of (3) must end with rule Definition with the premises
  Ax = x : " X. [ r ], x : " X. (B | F) (6)
  r = B | M (7)
  X = Gen (r, B, Ay) \ ctv(B|W) (8)
  Ay |- self(xD :: z(r)BW, (9)
To demonstrate |- ( D, y x   #  D ||- y x   #  (Ps), P) it suffices to show that Ay |- Ps. Note that Ay x = Ay + Ax follows from (1). The derivation of (4) must end with a rule Join-Parallel. Hence, for each message li (s (xi)) of M s, we have Ay + Ax |- x.li (s(xi)). In turn, this must be derived by rule Send with the premises Ay + Ax |- x.li : ti (10) and Ay + Ax |- s(xi) : ti (11). The judgment (10) is derived by either rule Private-Message or Message, depending on whether l is private or public. In both cases, each tuple ti is an instance of the generic type " X. B(li), with a substitution hi of domain in X ftv(B(li)).

The derivation of (9) must contain a sub-derivation
Reaction
A' |- M :: B0 (12)      Ay+ x : [r], x :(B| F) + A' |- P (13)      dom(A') = fn(M)
Sub    
Ay + x : [r], x :(B| F) |- M |> P :: z(r)B0cl(M),
Ay + x : [r], x :(B| F) |- M |> P :: z(r)B0W, (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 B0 is therefore a subset of B. As regards the premise (12), it is derived by a combination of rules Synchronization, Message-Pattern, and Empty-Pattern. Hence, we have:
A' |- li(xi) :: li : B(li(16)
for every i I. By (15) and the definitions of cl(B) and ctv(B|W), we have ftv(B (li)) ftv(B(lj)) ctv(B|W), hence by (8), ftv(B (li)) ftv(B(lj)) X = , for every distinct i and j in I. Thus, the sets (X ftv(B(li)))i I, i.e. dom(hi)i I form a partition of X. Let h be the sum of substitutions i I hi. Observe that the domain of h is included in X and is thus disjoint from free type variables of Ay (17).

Applying Lemma 3 to (13), we have h (Ay + x : [r], x :(B| F)) + h (A') |- P, that is, Ay + x : [h(r)], x : h (B| F) + h (A') |- P. By Lemma 4, we can let x be used polymorphically, i.e. Ay + Ax + h (A') |- P. Similarly, we have (Ay + Ax |- s(xi) : h(ti')) xi : ti' A' by Lemmas 3 and 4 successively applied to the collection of judgments (11). Thus, by Lemma 5, we derive Ay + Ax |- 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)BV,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)BV,W.
Lemma 8  []   For any selective refinement clauses S such that A |- S :: BW B'W', V', we have dom(B') \ dom(B) dl(S).

Proof:
Selective refinement clauses can always be written as |i I Ki K'i |> P. A proof of A |- S :: BW B'W', V' can only end with rule Modifier in which the derivation of each premise ends with a rule Modifier-Clause. Hence, we have at least the judgments
  Ai |- Ki :: Bi (18)
  Bi B (19)
  Ai |- Ki' :: B'i (20)
  B' = i i B'i (21)
Hence,
  dom(B') \ dom(B) dom(B') \ (i I dom(Bi)) by (19)
    = (i I dom(B'i)) \ (i I dom(Bi)) by (21)
    = i I ( dom(B'i) \ (j I dom(Bj)))
    i I ( dom(B'i) \ dom(Bi))
    = i I (dl(K'i) \ dl(Ki))
    = 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)BW,V
A |- S :: B1W1 B2W2,V2      dl(S) dom(B1) =      B B1      B2 | dom(B1) B1     
then A |- C' :: z(r)(B (B2 \ L))W',V' for some W' W (W2 dom(B (B2 \ L))), V' V (V2 ( dom(B1) \ L)), and L (dl(S) \ dl(C')) ( dom(B1) \ dom(B)).

Proof:
In this proof, we abbreviate dom(B) by B, for sake of conciseness.

Basic cases.
Filter-Apply.
Let us assume that
  K1 & K |> P with K1 K2 |> Q | S     
       | K2 & K |> P & Q or dl(K1) \ dl(K2) (1)
  A |- K1 & K |> P :: z(r)BW, V (2)
  A |- K1 K2 |> Q | S :: B1W1 B2W2,V2 (3)
  ((dl(K2) \ dl(K1)) dl(S)) B1 = (4)
  B B1 (5)
  B2 | B1 B1 (6)
The judgments (2) and (3) are respectively derived by
[Sub]
[Reaction]
[Synchronization]
A' |- K1 :: B1(7)      A' |- K :: B0  (8)
A' |- K1 & K :: B1' B0  (9)
A + A' |- P (10)      A' = fn(K1 & K(11)
A |- K1 & K |> P :: z(r)(B1' B0)cl(K1 & K),
A |- K1 & K |> P :: z(r)(B1' B0)W,V
and,
[Modifier]+[Sub]
A'' |- K1 :: B1(12)
A'' |- K2 :: B2(14)
A + A'' |- Q  (15)
     B1' B1 (13)
A'' = fn(K2(16)
W2' = cls(B1W1, K1 K2)
A |- K1 K2 |> Q :: B1W1 B2'W2',dl(K1) \ dl(K2)
   
A |- K1 K2 |> Q | S :: B1W1 B2W2,V2
where B = B1' B0 (17), cl(K1 & K) W (18), B2' B2 (19), W2' W2 and dl(K1) \ dl(K2) V2 (20).

From (7) and (12), A' and A'' coincide on fn(K1) because they assign the same types to fn(K1). Moreover, due to the scope rules of reaction rules and the selection operator, we can safely assume that A' A'' = fn(K1). Thus, by Lemma 2 applied to (8), and (14) we derive A'+A'' |- K :: B0 (21) and A'+A'' |- K2 :: B2(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 K2 & K. Notice that dl(K2) = (dl(K2) \ dl(K1)) (dl(K2) dl(K1)) and both left and right hand-sides of the have an empty intersection with dl(K). This follows from (4) and from the linearity of K1 & K.

By rule Synchronization with premises (22) and (21), we derive A' + A'' |- K2 & K :: B2' B0 (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(K1) fn(K2). By (16) and (12), we have fn(K1) fn(K2). Hence A' + A'' = fn(K2 & K(27). Therefore, by Reaction with premises (25), (26), and (27) we derive
A |- K2 & K |> P & Q :: z(r)(B2' B0)cl(K2 & K),      (28).
By rule Abstract, we also deduce
A |- dl(K1) \ dl(K2) :: z(r)B1'' ,dl(K1) \ dl(K2)     (29)
where B1'' = B1' \ dl(K2(30). Hence, Disjunction allows to derive:
A |- K2 & K |> P & Q or L' :: z(r)(B2' B0 B1'' )cl(K2 & K), dl(K1) \ dl(K2)      (31)
and by rule Sub:
A |- K2 & K |> P & Q or L' :: z(r)(B2' B0 B1'' )W', V'      (32)
where W' = W cl(K2 & K) and V' = V (dl(K1) \ dl(K2)).

Let L be (dl(S) \ (dl(K2) dl(K) dl(K1))) ((B1 \ B) \ dl(K2)), or equivalently, (dl(S) \ (B'2 B0 B'1)) ((B1 \ B) \ B'2(33). Observe that L is choosen so as to satisfy the condition L (dl(S) \ dl(C')) (B1 \ B). To conclude, we verify that other constraints of the lemma are satisfied for the judgment (32). That is,
  1. B2' B0 B1'' = B (B2 \ L). By (6)(13)(17)(19) it is enough to check the set equality: B'2 B0 B''1 = B (B2 \ L). Since both sides of (33) are restrictions outside of the set B'2, we have L B'2 B (34). Therefore,
    B2' B0 B1''
      = B2' B0 (B1' \ dl(K2)) by definition of B'1
      = B2' B0 (B1' \ B'2)) by (16)
      = B2' B0 B1'
      = B2' B by definition of B
      = B (B2 \ L) by (34)


  2. W' W (W2 (B (B2 \ L)). Because W' = W cl(K2 & K) and cl(K2 & K) W2 by (18), and cl(K2 & K) dl(K2 & K) = B'2 B0 B (B2 \ L) by the equality above.

  3. V' V (V2 (B1 \ L)). By definition, V' = V (dl(K1) \ dl(K2)) and dl(K1) \ dl(K2) V2 by (20). It remains to prove that dl(K1) \ dl(K2) B1 \ L. Since dl(K1) \ dl(K2) B1, it suffices to show that (dl(K1) \ dl(K2)) L = . Obviously, (dl(K1) \ dl(K2)) (dl(S) \ dl(K2 & K & K1)) = , whilst (dl(K1) \ dl(K2)) ((B1 \ B) \ dl(K2))= , since dl(K1) = B'1 B.
Filter-End.
Let us assume
  M |> P with 0 | M |> P (1)
  A |- M |> P :: z(r)BW,V (2)
  A |- 0 :: B1W1 B2W2,V2 (3)
  dl(0) B1 = (4)
  B B1 (5)
Since in (3) B2 must be the empty set, we conclude from (2) by choosing L = B1 \ B, W' = W, and V' = V.

Filter-Abstract.
Let us assume
  L' with S | L'
  A |- L' :: z(r)BW,V (1)
  A |- S :: B1W1 B2W2, V2
  dl(S) B1 = (2)
  B B1 (3)
  B2 | B1 B1 (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') (B1 \ B). We show that (1) satisfies the lemma:
  1. B (B2 \ L) =B. Since by (4) B2 is compatible with B1 and with B by (3), it suffices to show that B2 \ L B. By (5), it follows that L is equal to (dl(S) B1) \ B (6). Hence:
    B2 \ L = ((B2 | B1) (B2 \ B1)) \ L
      (B1 dl(S)) \ L by (4) and Lemma 8
      = (B1 dl(S)) \ ((B1 dl(S)) \ B)
      = (B1 dl(S)) B


  2. W W (W2 (B B2 \ L)). Obvious.

  3. V V (V2 (B1 \ L)). Obvious.
Inductive cases.
Filter-Next.
Let us assume
  M |> P with K1 K2 |> Q | S | C' (1)
  dl(K1) dl(M) (2)
  A |- M |> P :: z(r)BW,V (3)
  A |- K1 K2 |> Q | S :: B1W1 B2W2, V2 (4)
  ((dl(K2) \ dl(K1)) dl(S)) B1 = (5)
  B B1 (6)
  B2 | B1 B1 (7)
The selection clauses S are of the form |i IKi' K''i |> Qi. A derivation of (4) must contain an instance of Modifier, with premises:
  A |- K1 K2 |> Q :: B1W1 B2'W2', V2' (8)
  (A |- Ki' Ki'' |> Qi :: B1W1 Bi''Wi'', Vi'')i I
where
  B2'' = i I B''i  
  B2 = B2' B2'' (9)
  W2'' = i I Wi''  
  W2 = W2' W2'' (10)
  V2'' = i I Vi''  
  V2 = V2' V2'' (11)
 
Hence, by rule Modifier, we derive
A |- S :: B1W1 B2''W2'', V2''     (12)
A derivation of (1) must end with an instance of rule Filter-Next, 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')) (B1 \ B) (15)
  W' W (W''2 (B (B''2 \ L'))) (16)
  V' V (V''2 (B1 \ L')) (17)
Let us prove that A |- C' :: z(r)(B (B2 \ L))W', V' (18), for L = L' B'2 \ (B1 B''2) and check that L, W', V' satisfy the conditions of the lemma. We first prove that L (((dl(K2) \ dl(K1)) dl(S)) \ dl(C')) (B1 \ B(19). By Lemma 8 applied to (8), we have B2'\ B1 dl(K2) \ dl(K1(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 \ (B1 B''2)
  = L' (B'2 \ B1) \ B''2  
  L' (dl(K2) \ dl(K1)) \ B''2 by (20)
  = L' (dl(K2) \ dl(K1)) \ (B B''2) by (5)
  L' (dl(K2) \ dl(K1)) \ dl(C') by (21)
  = (dl(S) \ dl(C')) (B1 \ B) (dl(K2) \ dl(K1)) \ dl(C') by (15)
  = ((dl(K2) \ dl(K1)) dl(S)) \ dl(C') B1 \ B
To conclude, we check the following properties:
  1. B (B2 \ L) =B (B''2 \ L'). Since by (7) B2 and B1 agree, and so do B''2 and B by (6) and (9), it suffices to check the equality of their domains. By
    B (B2 \ L)   = B (B2 \ (L' B'2 \ (B1 B''2)))
    = B (B2 \ (B'2 \ (B1 B''2))) \ L'
    = B ((B'2 B''2) \ (B'2 \ (B1 B''2))) \ L'
    = B ((B'2 \ (B'2 \ (B1 B''2)))
      (B'2 \ (B'2 \ (B1 B''2))) ) \ L'
    = B ((B1 B''2) | B'2 B''2) \ L'
    =
    B
     
    (B1 | B'2) \ L'
    B
     
    (B''2 | B'2) \ L'
    B''2 \ L'
    (B''2 \ L')
    = B (B''2 \ L')


  2. W' W (W2 B (B2 \ L)). This follows from (16), W2'' W2 (by (10)), and B (B2 \ L) =B (B''2 \ L').

  3. V' V (V2 (B1 \ L)). This follows from (17), V2 V2' (by (11)) and L' L (by definition of L').
Filter-Or.
Let us assume that:
  C1 or C2 with S |- C' (1)
  A |- C1 or C2 :: z(r)BW,V (2)
  A |- S :: B1 B2W2,V2 (3)
  dl(S) B1 = (4)
  B B1 (5)
  B2 | B1 B1 (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 |- C1 :: z(r)B'1W'1, V'1 (8)
  A |- C2 :: z(r)B'2W'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) Bi = for i {1,2} (12). The reduction (1) implies that C' is of the form C'1 or C'2 such that Ci 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 Li, W''i, and V''i such that
  A |- C'i :: z(r)(B'i (B2 \ Li))W''i, V''i (14)
  Li (dl(S) \ dl(C'i)) (B1 \ B'i) (15)
  W''i W'i (W2 B'i (B2 \ Li)) (16)
  V''i V'i (V2 (B1 \ Li)) (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 (B2 \ L1) (B2 \ L2)W', V'     (18)
where
  W' = W''1 W''2
  V' = V''1 \ (B'2 (B2 \ L2) \ V''2) V''2 \ (B'1 (B2 \ L1) \ V''1)
Let L be L1 L2. Then
  L = L1 L2
  ((dl(S) \ dl(C1)) (B1 \ B'1)) ((dl(S) \ dl(C2)) (B1 \ B'2)) by (15)
  (dl(S) \ dl(C1)) (dl(S) \ dl(C2)) (B1 \ B'1) (B1 \ B'2) by distributivity
  = (dl(S) \ (dl(C1) dl(C2))) (B1 \ (B'1 B'2))
  = (dl(S) \ dl(C)) (B1 \ B) (19)

To conclude, we prove that (18) satisfies the constraints of the lemma. Indeed, we have:
  1. B (B2 \ L) = B'1 B'2 (B2 \ L1) (B2 \ L2). Since B = B'1 B'2 and B2 \ L = B2 \ L1 B2 \ L2.

  2. W' W (W2 B (B2 \ L)). Since W' = W''1 W''2, it suffices to show that W''i W (W2 B (B2 \ L)), for i {1,2}. This follows by (16), (10) and because B'i (B2 \ Li) B (B2 \ L) (by previous item).

  3. V' V (V2 (B1 \ L)). It suffices to show that both
    V''1 \ (B'2 (B2 \ L2) \ V''2) V (V2 (B1 \ L))
    and
    V''2 \ (B'1 (B2 \ L1) \ V''1) V (V2 (B1 \ 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
  1. if A + x : [r] , x.(B | F) |- C:: z(r)BW,V and C |-x C' then A + x : [r] , x.(B | F) |- C':: z(r)BW,V;

  2. 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 Ax for A + x : [r] , x.(B | F).

Basic cases for class reduction.
Self.
Let self(zC |-x C {z x} and let Ax |- self(zC :: z(r)BW,V. A derivation of this judgment must end with an instance of Self-Binding, followed by a sequence of Sub rules. Hence,
Ax + z : [r] , z.(B | F) |- C :: z(r)B W',V'
with W' W and V' V. Then, by Lemma 5, we have:
Ax |- C {z x} :: z(r)B W',V'
We conclude Ax |- C {z x} :: z(r)BW,V by rule Sub.

Or-Pat.
Let J1 or J2 |> P |-x J1 |> P or J2 |> P and let Ax |- J1 or J2 |> P :: z(r)BW, V (1). The derivation of this judgment must end with the following derivation followed by a sequence of Sub rules:
[Reaction]
[Alternative]
A' |- J1 :: B1      A' |- J2 :: B2     
A' |- J1 or J2 :: B
Ax + A' |- P      dom(A') = fn(J1 or J2(2)
Ax |- J1 or J2 |> P :: z(r)Bcl(J1) cl(J2),
where B is B1 B2 and cl(J1) cl(J2) W. Since fn(J1 or J2) = fn(J1) = fn(J2), we have:
[Disjunction]
A' |- Ji :: Bi      Ax+ A' |- P      dom(A') = fn(Ji)
Ax |- Ji |> P :: z(r)Bicl(Ji),
 i = 1, 2
Ax |- J1 |> P or J2 |> P :: z(r)Bcl(J1) cl(J2),
The we conclude Ax |- J1 |> P or J2 |> P :: z(r)BW, V by rule Sub.

Abstract-Cut.
Let C or L |-x C or L' and Ax |- C or L :: z(r)BW,V and L' = L \ dl(C), with L L'. Therefore L' L (1). The derivation of the judgment Ax |- C or L :: z(r)BW,V must end with the following derivation followed by a sequence of Sub rules:
[Disjunction]
[Abstract]
dom(B2) = L
Ax |- L :: z(r)B2, L
     Ax|- C :: z(r)B1W1,V1
L'' = L \ ( dom(B1) \ V1) (2)
Ax |- C or L :: z(r)(B1 B2)W1, V1 L''
where B = B1 B2, W1 W (3) and V1 L'' V (4).

We first observe that B1 B2 = B1 (B2 | L'). Therefore we can derive:
[Disjunction]
[Abstract]
dom(B2 | L') = L'
Ax |- L' :: z(r)(B2 | L'), L'
     Ax|- C :: z(r)B1W1,V1
L''' = L' \ ( dom(B1) \ V1) (5)
Ax |- C or L' :: z(r)(B1 B2)W1, V1 L'''
By (2), (5) and (1), we derive V1 L''' V1 L''. Hence, by (3), (4) and rule Sub, we obtain Ax |- C or L' :: z(r)(B1 B2)W, V.

Class-Abstract.
Let C or |-x C and Ax |- C or :: z(r)BW,V. The derivation of this judgment must end with rule Disjunction followed by a sequence of Sub rules:
[Disjunction]
Ax |- C :: z(r)BW', V'      Ax|- :: z(r),
Ax |- C or :: z(r)BW',V'
where W' W and V' V. Then, by rule Sub applied to Ax |- C :: z(r)BW',V', we obtain Ax |- C :: z(r)BW,V.

Basic cases for processes.
Class-Var.
Let us assume A |- class c = self(zC 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)BW,V (2)
A + c : " Gen (r, B, A). z(r)BW,V |- P (3)
A |- class c = C in P
By Lemma 6 applied to (2) and (3), we derive A |- P {c C}.

Inductive cases for classes.
Class-Context.
Let Ax |- E {C} :: z(r)BW,V and E {C} |-x E {C'}. By inductive hypothesis, if Ax |- C :: z(r)B'W', V' then Ax |- C' :: z(r)B'W',V', since C |-x C'. The judgment Ax |- E {C'} :: z(r)BV follows by induction on the structure of E {}. The details are omitted.

Match.
Let us assume that A |- match C with S end : z(r)BW, V (1) and match C with S end C(2). We must prove that A |- C' : z(r)BW, 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 B1 B2 (4) and
  A |- C :: z(r)B1W1, V1 (5)
  A |- S :: B1W1 B2W2, V2 (6)
  dl(S) dom(B1) = (7)
  W1 W2 W (8)
  V1 V2 V (9)
The derivation of (2) must contain a rule Match with the premises:
  C with S C' (10)
  dl(S) dl(C') (11)
From (4) it follows that B2 | dom(B1) dom(B2(12). Lemma 9 applied to (10), (5), (6), (7), and (12) implies that
  A |- C' :: z(r)(B1 (B2 \ L))W',V' (13)
  L (dl(S) \ dl(C')) ( dom(B1) \ dom(B1)) (14)
  W' W1 (W2 dom(B1 (B2 \ L))) (15)
  V' V1 (V2 ( dom(B1) \ L)) (16)
The property (11) combined with (14) imply that L is empty. Therefore W' W1 W2 and V' V1 V2. Hence (3) follows by (13), (8), (9) and rule Sub.

Inductive cases for processes.
Class-Red.
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]
[Self-Binding]
A + x : [r], x :(B | F) |- C :: z(r)BW, (3)
A |- self(xC :: z(r)BW,
r = B | M      X= Gen (r, B, A) \ ctv(B|W)
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)BW,, which we can substitute in the previous derivation, thus concluding A |- obj x = C' init P in Q.


B.4 Safety (Theorem 2)

Proof:
Let us assume |- ( D ||- P). By Chemical-Solution and Definition, |- ( D ||- P) holds provided
(Ay|- D :: Ax) y x   #  D D (1)

(Ay|- P) y   #  P P  (2)

A = y x   #  D D Ax  (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 Ay|- D :: Ax. This leaf must be of the form Ay+ A' |- x : t. This implies that x belongs to the domain of Ay because x is free in D. Similarly, every class variable in D should belong to the domain of Ay, 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).
  1. (no privacy failure) Let l be a private label f. We prove that y'x is a prefix of y. A derivation of Ay |- x.l (uii I) must be:
    [Send]
    ((5))
    ...
    Ay |- x.f : (ti i I)
         (Ay |- ui : ti)i I
    Ay |- x.l (uii I)
    where (5) is an instance of Private-Message. The premise of (5) requires that x : " X.(l : (tii I); B') be in Ay. Therefore, by definition of Ay, variable x must appear in y. Furthermore, by well-formedness 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''.

  2. (no undeclared label) We show that l dl(D). Given (4), the judgment Ay' |- D :: Ax, where Ax = x: " X. r, x: " X.(B | F ), follows by rule Definition applied to (1) with the premises below:
    Ay' |- self(xD :: z(r) BW, (6)

    r = B| M (7)

    X = Gen (r, B, Ay') \ ctv(B|W)
    Since Ay|- 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.

  3. (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]
    (
    Message-Pattern    
    (yi : t'i A')i I
    A' |- l (y):: l : (t'ii I)
    )
    l(y) M
     
     
    A' |- M :: B
            
    dom(A') = fn(M)      Ay' + x : [r], x : (B | F)+ A' |- P
    Ay' + x : [r], x : (B | F) |- M |> P :: z(r)Bcl(M),
    Therefore, the type of y in A' is B(l). By rules Chemical-Solution and Definition, A contains a generalization of x : [r], x : (B | F). Thus, the type of x.l in Ay is a generalization of B(l). The proof tree illustrated in item 1 is required to prove Ay |- x.l (uii I). Then, as a consequence of rule (5), the type of u is an instance of the type of x.l in Ay, 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 Class-Red 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,
  1. C E{c}, and c is free. By (1), dom(A) only contains object names. Therefore, by (2), P cannot contain free class names.
  2. 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)BW,V then L V. By rule Abstract, A' |- L :: z(r)B1,L (8). Let A' |- C' :: z(r)B2W2,V2 (9) and V1' = L \( dom(B2) \ V2(10) and V2' = V2 \( dom(B1) \ L(11). Since there does not exists C'' such that C |-x C'', the rule Abstract-Cut cannot be applied. This means that L = L \ dl(C') = L \ dom(B2), which implies V1' = L. By (8), (9), (10), (11) and rule Disjunction we obtain A' |- C or L :: z(r)(B1 B2)W1 W2, L V2' (12).

    On the other hand, by (2), a derivation of Ay|- P must contain (P = obj x = C init Q in Q')
    [Object]
    [Self-Binding]
    Ay+ x : [r],   x.(B | F) |- (C' or L) :: z(r)BW,(13)
    Ay|- self(x)  (C' or L) :: z(r)BW,
    r = B | M      X= Gen (r, B, A) ctv(B|W)
    Ay+ x : " X. [r], x : " X. (B | F) |- Q      Ay+ 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 LATEX by HEVEA.