# A prototype-based approach to object evolution

Alberto Ciaffaglione, Pietro Di Gianantonio, Furio Honsell, Luigi Liquori

► To cite this version:

Alberto Ciaffaglione, Pietro Di Gianantonio, Furio Honsell, Luigi Liquori. A prototype-based approach to object evolution. The Journal of Object Technology, 2020, 20 (4), pp.1-24. hal-01646168v6

HAL Id: hal-01646168

https://inria.hal.science/hal-01646168v6

Submitted on 26 Oct 2021

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.
# A protoype-based approach to object evolution

Alberto Ciaffaglione*, Pietro Di Gianantonio*, Furio Honsell*, and Luigi Liquori†

**ABSTRACT** We investigate, in the context of *functional prototype-based languages*, a calculus of objects which might extend themselves upon receiving a message, a capability referred to by Cardelli as a *self-inflicted* operation. We present a sound type system for this calculus which guarantees that evaluating a well-typed expression will never yield a *message-not-found* runtime error. The resulting calculus is an attempt towards the definition of a language combining the safety advantage of static type checking with the flexibility found in dynamically typed languages.

**KEYWORDS** Prototype-based calculi, Static typing, Object reclassification.

## 1. Introduction

Calculi and languages supporting the *object-oriented programming paradigm* are traditionally divided in two main classes, depending on the presence or absence of *classes* (Abadi & Cardelli 1996). In languages of the first kind, called *class-based*, the notion of class is intended to describe the structure of all *objects* generated from it; classes therefore behave as templates for objects. Languages of the second kind are more heterogeneous and are referred to with a variety of names such as *object-based*, *delegation-based*, etc. In these languages classes *per se* are absent, but their role is emulated through more primitive notions. *Prototype-based languages* are an important class of languages featuring this second style of the object-oriented paradigm. Objects are built from scratch and may be *reused* as canonical representatives, the so-called *prototypes*, to derive novel objects by means of the *inheritance mechanism*.

The possibility of changing at runtime the behavior of objects, by updating, overriding, adding, or even deleting methods, is a major feature that an object-oriented language may provide the programmer with. The trade-off for such a kind of flexibility is given by the lack of static type systems. Indeed, modifying objects at runtime is allowed within dynamically

typed languages such as Smalltalk (via the *become* method), Python (by modifying the `_class_` attribute), and JavaScript.

In this paper we introduce the system $\lambda Obj^\oplus$, which provides yet further flexibility in modifying objects at runtime, still retaining a static typing system. The system $\lambda Obj^\oplus$ builds on the Lambda Calculus of Objects, $\lambda Obj$, which was introduced by Fisher, Honsell, and Mitchell (Fisher et al. 1994) as the first solid foundation for the prototype-based paradigm. $\lambda Obj^\oplus$ is a functional calculus of objects which allows for a full-fledged use of *self-inflicted* operations in methods. The user can modify objects at runtime by calling methods owned by the object itself, both for overriding its own existing methods, as $\lambda Obj$ already features, but also for adding new ones. In $\lambda Obj$, in fact, object extension can be used only as an operation external to the object being extended. Therefore objects cannot self-extend themselves at runtime, but can be extended only by methods owned by other objects. To support the safety of these potentially brittle operations, $\lambda Obj^\oplus$ is equipped with a type assignment system, which permits self-inflicted extension, but is still capable of catching statically the *message-not-found* runtime error.

The present work bears some connection, albeit from a different perspective, to research carried out on Fickle (Drossopoulou et al. 2001, 2002; Damiani et al. 2003), JavaScript (Anderson & Giannini 2005; Thiemann 2005; Zhao 2010, 2012; Chugh et al. 2012) and the related TypeScript (Bierman et al. 2014).

JavaScript is a prototype-based scripting language widely used for Web applications, whose popularity essentially relies on its flexibility: for instance, objects may be modified at runtime, by adding or deleting their members or by replacing them with

<footnote>*Università degli Studi di Udine, Italy</footnote>

<footnote>†INRIA and Université Côte d'Azur, France</footnote>

<footnote>**JOT reference format:**
Alberto Ciaffaglione, Pietro Di Gianantonio, Furio Honsell, and Luigi Liquori. *A protoype-based approach to object evolution*. Journal of Object Technology. Vol. vv, No. nn, yyyy. Licensed under Attribution - NonCommercial - No Derivatives 4.0 International (CC BY-NC-ND 4.0)
http://dx.doi.org/10.5381/jot.yyyy.vv.nn.aa</footnote>
values of different, unrelated types. It is apparent that features like these, make static typing problematic, hence JavaScript was originally only dynamically typed. However, such a typing discipline may not prevent runtime errors, even in presence of runtime type tests for determining properties of objects. As a consequence, in recent years the task of defining more and more powerful type assignment systems, capable to statically type-check larger and larger fragments of JavaScript, has been pursued incessantly.

TypeScript is an extension of JavaScript, introduced to enable easier development of large-scale JavaScript applications. Actually, its compiler checks JavaScript programs and emits JavaScript code. TypeScript enriches JavaScript with a module system, classes, interfaces, and a static type system; however, in order to guarantee the usability of the language, the type system is not statically sound by design.

Fickle, on the other hand, is a class-based language which allows objects to perform the so-called “(dynamic) object reclassification”, that is, changing at runtime their class membership while retaining their identity. It is clear that this kind of behavior provides the user with a high level of flexibility. However, as far as we know, the Fickle type system has never been completely implemented in a concrete programming language.

**Achievements of the present paper** In the context outlined above, we introduced and investigated, in the past decade, the $\lambda Obj^\oplus$ calculus. In our view, prototype-based calculi can offer a finer approach to the above critical issues since they may be defined by means of more primitive mechanisms than class-based calculi and therefore are simpler to analyze and implement. What we achieve in $\lambda Obj^\oplus$, through self-extension, is the possibility of safely extending objects at runtime, as well as updating their methods, provided the overriding version has a type “coherent” with the overridden one. This behavior is less expressive than that of JavaScript, which allows for unrelated overrides, but has the advantage that the catastrophic *message-not-understood* runtime error may be detected statically.

In order to investigate more in depth the expressive power of $\lambda Obj^\oplus$, we have compared it with the features offered by object evolution (Cohen & Gil 2009) and object reclassification in Fickle (Drossopoulou et al. 2002). In fact, we show that the two mechanisms can be emulated in $\lambda Obj^\oplus$ via embedding inheritance and delegation inheritance, respectively.

The present paper extends significantly an earlier paper by the authors, (Di Gianantonio et al. 1998), as follows: we have modified the reduction semantics, substantially simplified the type system, fully documented the proofs, and, by adding novel sections, we have connected our approach with the more recent related developments in the area.

**The Lambda Calculus of Objects, $\lambda Obj$, and its limits**
$\lambda Obj$ is a lambda calculus extended with object primitives, where a new object may be created by modifying or extending an existing *prototype*. The new object thereby inherits properties from the original one in a controlled manner. Objects can be viewed as lists of pairs (*method name*, *method body*) where the method body is (or reduces to) a lambda abstraction whose first formal parameter is always the object itself (this in C++

and Java). The type assignment system of $\lambda Obj$ is set up so as to prevent the catastrophic *message-not-found* runtime error. Types of methods are allowed to be specialized to the type of the inheriting objects. This feature is usually referred to as “mytype method specialization”. The high mutability of method bodies is accommodated in the type system by introducing a form of *higher-order polymorphism*, on top of a calculus inspired by the work of Wand on extensible records (Wand 1987).

The calculus $\lambda Obj$ spurred an intense research in type assignment systems for object calculi. Several calculi inspired by $\lambda Obj$, dealing with various extra features such as incomplete objects, subtyping, encapsulation, imperative features, have appeared soon afterwards (see e.g. (Fisher & Mitchell 1995; Bono & Liquori 1994; Bono et al. 1997; Fisher & Mitchell 1998; Bono & Fisher 1998)).

More specifically, $\lambda Obj$ supports two operations which may change the shape of an object: method *addition* and method *override*. The operational semantics of the calculus allows method bodies in objects to modify their own self, a powerful capability referred to by Cardelli as a *self-inflicted* operation (Cardelli 1995).

Consider for instance the method $set_x$, belonging to a *pt* object with an *x* field:

$$pt \triangleq \langle x=\lambda s.0, set_x=\lambda s.\lambda v.\langle s \leftarrow x=\lambda s'.v \rangle, \dots \rangle$$

When $set_x$ is called to *pt* with argument “3”, written as $pt \leftarrow set_x(3)$, the result is a new object where the *x* field has been set (i.e. overridden) to 3. Notice the self-inflicted operation of object override (i.e. $\leftarrow$) performed by the $set_x$ method.

However, in all the type systems for calculi of objects, both those derived from $\lambda Obj$ and those derived from Abadi and Cardelli's *Object Calculus* (Abadi & Cardelli 1996), the type system prevents the possibility for a method to self-inflict an extension to the host object. We feel that this is an unpleasant limitation if the message-passing paradigm is to be taken in full generality. Moreover, in $\lambda Obj$ this limitation appears arbitrary, given that the operational semantics supports without difficulty self-inflicted extension methods.

There are plenty of situations, both in programming and in real life, where it would be convenient to have objects which modify their interface upon an execution of a message. Consider for instance the following situations.

- The process of *learning* could be easily modeled using an object which can react to the “teacher’s message” by extending its capability of performing a new task, in the future, in response to a new request from the environment (an “old dog” could appear to learn new tricks if in his youth it had been taught a “self-extension” trick).

- The process of “vaccination” against the virus $\mathcal{X}$ can be viewed as the act of extending the capability of the immune system of producing, in the future, a new kind of “$\mathcal{X}$-antibodies” upon receiving the message that an $\mathcal{X}$-infection is in progress. Similar processes arise in epigenetics.

- In standard typed class-based languages the structure of a class can be modified only statically. If we need to add
a new method to an instance of a class we are forced to recompile the class and to make the modification needlessly available to all the class instances, thereby wasting memory. If a class had a self-extension method, only the instances of the class which have dynamically executed this method would allocate new memory, without the need of any re-compilation. As a consequence, many sub-class declarations could be easily explained away if suitable self-extension methods in the parent class were available.

- Downcasting could be smoothly implementable on objects with self-extension methods<fnref n="1" />. For example, for a colored point cpt extending the pt object above, the following expression could be made to type check (see Section 5):

$$ cpt \Leftarrow eq(pt \Leftarrow add_{col}(black) ) $$

where add_col is intended to be a self-extension method of pt (adding a col method) and eq is the name of the standard binary equality method.

- Self-extension is strictly related to object evolution and object reclassification (see Sections 7 and 8), two features which are required in areas such as e.g. banking, GUI development, and games.

**Self-inflicted extension** To enable the $\lambda Obj^\oplus$ calculus to perform self-inflicted extensions, two modifications of the system in (Fisher et al. 1994) are necessary. The first is, in effect, a simplification of the original syntax of the language. The second is much more substantial and it involves the type discipline.

As far as the syntax of the language is concerned, we are forced to unify into a single operator, denoted by $\leftarrow \oplus$, the two original object operators of $\lambda Obj$, i.e. object extension ($\leftarrow$) and object override ($\leftarrow$). This is due to the fact that, when iterating the execution of a self-extension method, only the first time we have a genuine object extension, while from the second time onwards we have just a simple object override.

**Example 1.1** Consider the add_col method, that adds a col field to the “point” object p:

$$ \begin{align*} p &\triangleq \langle x=\lambda s.0, \\ &\quad set_x=\lambda s.\lambda v.\langle s\leftarrow\oplus x=\lambda s'.v\rangle, \\ &\quad add_{col}=\lambda s.\lambda v.\langle s\leftarrow\oplus col=\lambda s'.v\rangle \end{align*} $$

When add_col is sent to p with argument “white”, i.e. $p \Leftarrow add_{col}(white)$, the result is a new object cp where the col field has been added to p and set to white:

$$ cp \triangleq \langle x=..., set_x=..., add_{col}=..., col=\lambda s.white \rangle $$

If add_col is sent twice to p, i.e. $cp \Leftarrow add_{col}(black)$, then, since the col field is already present in cp, it will be overridden with the new “black” value:

$$ cp' \triangleq \langle x=..., set_x=..., add_{col}=..., col=..., col=\lambda s.black \rangle $$

Therefore, only the rightmost version of a method will be the effective one.

As far as types are concerned, we add two new kinds of object-types, namely $\tau \oplus m$, which can be seen as the type-theoretical counterpart of the syntactic object $\langle e_1 \leftarrow \oplus m = e_2 \rangle$, and $\mathit{prot}.R \oplus m_1 \dots \oplus m_k$, a generalization of the original $\mathit{class}.R$ in (Fisher et al. 1994), named pro-type. Intuitively, if the type $\mathit{prot}.R \oplus m_1 \dots \oplus m_k$ is assigned to an object $e$ ($t$ represents the type of self), $e$ can respond to all the methods $m_1, \dots, m_k$. It is required that the list of pairs $R$ contains all the methods $m_1, \dots, m_k$ together with their corresponding types; moreover, $R$ may contain some reserved methods, i.e. methods that can be added to $e$ either by ordinary object-extension or by a method in $R$ which performs a self-inflicted extension (therefore, if $R$ does not contain reserved methods, $\mathit{prot}.R \oplus m_1 \dots \oplus m_k$ would coincide with $\mathit{class}.R$ of (Fisher et al. 1994)).

To convey to the reader the intended meaning of pro-types, let us suppose that an object $e$ is assigned the type $\mathit{prot}.\langle m:t \oplus n, n:int \rangle \oplus m$. In fact, $e \Leftarrow n$ is not typable, but since $e \Leftarrow m$ has the effect of adding the method $n$ to the interface of $e$, thus updating the type of $e$ to $\mathit{prot}.\langle m:t \oplus n, n:int \rangle \oplus m \oplus n$, then ($e \Leftarrow m$) $\Leftarrow n$ is typable.

The list of reserved methods in a pro-type is crucial to enforce the soundness of the type assignment system. Consider e.g. an object containing two methods, $addn_1$, and $addn_2$, each of them self-inflicting the extension of a new method $n$. The type assignment system has to carry enough information so as to enforce that the same type will be assigned to $n$ whatever self-inflicted extension has been executed.

The typing system that we will introduce ensures that we can always dynamically add new fresh methods for pro-types, thus leaving intact the original philosophy of rapid prototyping, peculiar to object calculi.

To model specialization of inherited methods, we use the notion of matching, a.k.a. type extension, originally introduced by Bruce (Bruce 1994) and later applied to the Object Calculus (Abadi & Cardelli 1996) and to $\lambda Obj$ (Bono & Bugliesi 1999). At the price of a little more mathematical overhead, we could have used also the implicit higher-order polymorphism of (Fisher et al. 1994).

**Object subsumption** As it is well-known, see e.g. (Abadi & Cardelli 1996; Fisher & Mitchell 1994), the introduction of a subsumption relation over object-types makes the type system unsound. In particular, width-subtyping clashes with object extension, and depth-subtyping clashes with object override. In fact, on pro-types no subtyping is possible. In order to accommodate subtyping, we add another kind of object-type, i.e. $\mathit{obj}.t.R \oplus m_1 \dots \oplus m_k$, which behaves like $\mathit{prot}.t.R \oplus m_1 \dots \oplus m_k$ except that it can be assigned to objects which can be extended only by making longer the list $\oplus m_1 \dots \oplus m_k$ (by means of reserved methods that appear in $R$). On obj-types a (covariant) width-subtyping is permitted<fnref n="2" />.

**Synopsis.** The present paper is organized as follows. In Section 2 we introduce the calculus $\lambda Obj^\oplus$, its small-step operational semantics, and some intuitive examples to illustrate the

<footnote n="1">¹ Clearly, a semantics that simply “fixes” the object to have the requested type when there is a downcast could be even more bug-prone than throwing.</footnote>

<footnote n="2">² The pro and obj terminology is the same as in Fisher and Mitchell (Fisher & Mitchell 1995, 1998).</footnote>
idea of self-inflicted object extension. In Section 3 we define the type system for $\lambda Obj^{\oplus}$ and discuss in detail the intended meaning of the most interesting rules. In Section 4 we show how our type system is compatible with a width-subtyping relation. Section 5 presents a collection of typing examples. In Section 6 we state our soundness result, namely that every closed and well-typed expression will not produce wrong results. Section 7 is devoted to an example, in order to illustrate the potential of the self-inflicted extension mechanism as a runtime feature, in connection with object evolution and object reclassification. In Section 8 we discuss related work and in Section 9 we address conclusions and future work. The complete set of type assignment rules appears in the Appendix, together with full proofs.

## 2. The lambda calculus of objects

In this section, we present the Lambda Calculus of Objects $\lambda Obj^{\oplus}$. The terms are defined by the following abstract grammar:

$$ \begin{array}{l@{\hspace{2em}}l@{\qquad}l} e ::= & c \mid x \mid \lambda x.e \mid e_1 e_2 & (\lambda\text{-terms}) \\ & \langle \rangle \mid \langle e_1 \leftarrow \oplus m = e_2 \rangle \mid e \leftarrow m & (\text{object-terms}) \\ & Sel(e_1, m, e_2) & (\text{auxiliary terms}) \end{array} $$

where c, x, m are meta-variables ranging over sets of constants, variables, and names of methods, respectively. As usual, terms that differ only in the names of bound variables are identified. Terms are untyped $\lambda$-terms enriched with objects: the intended meaning of the object-terms is the following: $\langle \rangle$ stands for the empty object; $\langle e_1 \leftarrow \oplus m = e_2 \rangle$ stands for extending/overriding the object $e_1$ with a method $m$ whose body is $e_2$; $e \leftarrow m$ stands for the result of sending the message $m$ to the object $e$.

The auxiliary operation $Sel(e_1, m, e_2)$ searches the body of the $m$ method within the object $e_1$. In the recursive search of $m$, $Sel(e_1, m, e_2)$ removes methods from $e_1$; for this reason we need to introduce the expression $e_2$, which denotes a function that, applied to $e_1$, reconstructs the original object with the complete list of its methods. This function is peculiar to the operational semantics and, in practice, could be made not available to the programmer.

To ease the notation we write $\langle m_1=e_1, \dots, m_k=e_k \rangle$ as syntactic sugar for $\langle \dots \langle \rangle \leftarrow \oplus m_1=e_1 \dots \leftarrow \oplus m_k=e_k \rangle$, where $k \ge 1$. Moreover, when no confusion can arise, we write $e$ in place of $\lambda x.e$ if $x \notin FV(e)$; this mainly concerns methods, whose first formal parameter is always their host object: e.g. $\lambda s.1$ and $\lambda s'.(s \leftarrow m)$ are usually written $1$ and $s \leftarrow m$, respectively.

### 2.1. Operational semantics

We define the semantics of $\lambda Obj^{\oplus}$ terms by means of the reduction rules displayed in Figure 1 (small-step semantics $\rightarrow$); the evaluation relation $\rightarrow\vdash$ is then taken to be the symmetric, reflexive, transitive and contextual closure of $\rightarrow$.

In addition to the standard $\beta$-rule for $\lambda$-calculus, the main operation on objects is method invocation, whose reduction is defined by the (Selection) rule. Sending a message $m$ to an object $e$ which contains a method $m$ reduces to $Sel(e, m, \lambda s.s)$,

$$ \begin{array}{l@{\hspace{2em}}l@{\hspace{2em}}l} (\text{Beta}) & (\lambda x.e_1)e_2 & \rightarrow \\ & e_1[e_2/x] & \\ (\text{Selection}) & e \leftarrow m & \rightarrow \\ & Sel(e, m, \lambda s.s) & \\ (\text{Success}) & Sel(\langle e_1 \leftarrow \oplus m = e_2 \rangle, m, e_3) & \rightarrow \\ & e_2(e_3 \langle e_1 \leftarrow \oplus m = e_2 \rangle) & \\ (\text{Next}) & Sel(\langle e_1 \leftarrow \oplus n = e_2 \rangle, m, e_3) & \rightarrow \\ & Sel(e_1, m, \lambda s.e_3 \langle s \leftarrow \oplus n = e_2 \rangle) & \end{array} $$

<caption>Figure 1 Reduction Semantics (Small-Step)</caption>

where the arguments of $Sel$ have the following intuitive meanings:

1<sup>st</sup>-arg. is a sub-object of the receiver (or recipient) of the message;

2<sup>nd</sup>-arg. is the message we want to send to the receiver;

3<sup>rd</sup>-arg. is a function that transforms the first argument in the original receiver.

By looking at the last two rules, one may note that the $Sel$ function scans the receiver of the message until it finds the definition of the called method: when it finds such a method, it applies its body to the receiver of the message. Notice how the $Sel$ function carries over, in its search, all the information necessary to reconstruct the original receiver of the message. The following reduction illustrates the evaluation mechanism:

$$ \begin{array}{l@{\hspace{2em}}l@{\hspace{2em}}l} \langle id = \lambda s.s, \text{one} = 1 \rangle \leftarrow id & \rightarrow & \\ Sel(\langle id = \lambda s.s, \text{one} = 1 \rangle, id, \lambda s'.s') & \rightarrow & \\ Sel(\langle id = \lambda s.s \rangle, id, \lambda s''.(\lambda s'.s')\langle s'' \leftarrow \oplus \text{one} = 1 \rangle) & \rightarrow & \\ (\lambda s.s)((\lambda s''.(\lambda s'.s'))\langle s'' \leftarrow \oplus \text{one} = 1 \rangle)\langle id = \lambda s.s \rangle) & \rightarrow & \\ (\lambda s''.(\lambda s'.s')\langle s'' \leftarrow \oplus \text{one} = 1 \rangle)\langle id = \lambda s.s \rangle & \rightarrow & \\ (\lambda s'.s')\langle\langle id = \lambda s.s \rangle\leftarrow \oplus \text{one} = 1 \rangle & \rightarrow & \\ \langle id = \lambda s.s, \text{one} = 1 \rangle & \rightarrow & \end{array} $$

Namely, in order to call the first method $id$ of an object-term with two methods, $\langle id = \lambda s.s, \text{one} = 1 \rangle$, one needs to consider the subterm containing just the first method $\langle id = \lambda s.s \rangle$ and construct a function, $\lambda s''.\langle s'' \leftarrow \oplus \text{one} = 1 \rangle$, transforming the subterm into the original term.

**Proposition 2.1** *The $\rightarrow$ reduction is Church-Rosser.*

We use the classical technique based on Takahashi's translation for $\lambda$-calculus, (Takahashi 1995). With respect to the $\lambda$-calculus, $\lambda Obj^{\oplus}$ contains, besides the $\lambda$-rule, reduction rules for object terms; however, the latter do not interfere with the former, hence Takahashi's technique can be extended straightforwardly to the $\lambda Obj^{\oplus}$ calculus. First we define a parallel reduction on $\lambda$-terms, where several redexes can be reduced in parallel; then
we show that for any term *e* there is a term *e*\*, i.e. Takahashi's translation, obtained from *M* by reducing the maximum set of redexes in parallel. It follows immediately that the parallel reduction satisfies the triangular property, hence the diamond property, and therefore the calculus is confluent.

## 2.2. Examples

In the next examples we show three objects, none of which can be defined in (Fisher et al. 1994) and (Abadi & Cardelli 1996), performing, respectively: a self-inflicted extension; two (nested) self-inflicted extensions; and a self-inflicted extension “on the fly”.

**Example 2.1** Consider the object self\_ext, defined as follows:

$$self_{ext} \triangleq \langle add_n = \lambda s. \langle s \leftrightarrow n = 1 \rangle \rangle$$

If we send the message add\_n to self\_ext, then we have the following computation:

$$\begin{align*}
self_{ext} \leftarrow add_n & \rightarrow Sel(self_{ext}, add_n, \lambda s'.s') \\
& \rightarrow (\lambda s. (s \leftrightarrow n = 1)) self_{ext} \\
& \rightarrow \langle self_{ext} \leftrightarrow n = 1 \rangle
\end{align*}$$

i.e. the method *n* has been added to self\_ext. If we send the message add\_n twice to self\_ext, i.e. $\langle self_{ext} \leftrightarrow n = 1 \rangle \leftarrow add_n$, the method *n* is merely overridden with the same body; hence, we get an object which is “operationally equivalent” to the previous one.

**Example 2.2** Consider the object inner\_ext, defined as follows:

$$inner_{ext} \triangleq \langle add_{mn} = \lambda s. \langle s \leftrightarrow m = \lambda s'. \langle s' \leftrightarrow n = 1 \rangle \rangle \rangle$$

If we send the message add\_mn to inner\_ext, then we obtain:

$$inner_{ext} \leftarrow add_{mn} \rightarrow \langle inner_{ext} \leftrightarrow m = \lambda s. \langle s \leftrightarrow n = 1 \rangle \rangle$$

i.e. the method *m* has been added to inner\_ext. On the other hand, if we send first the message add\_mn and then *m* to inner\_ext, both the methods *m* and *n* are added:

$$\begin{align*}
(inner_{ext} \leftarrow add_{mn}) \leftarrow m \rightarrow \\
\langle add_{mn} \rangle &= \lambda s. \langle s \leftrightarrow m = \lambda s'. \langle s' \leftrightarrow n = 1 \rangle \rangle, \\
m &= \lambda s. \langle s \leftrightarrow n = 1 \rangle, \\
n &= 1
\end{align*}$$

**Example 2.3** Consider the object fly\_ext, defined as follows:

$$fly_{ext} \triangleq \langle f = \lambda s. \lambda s'. s' \leftarrow n, get_f = \lambda s. (s \leftarrow f) \langle s \leftrightarrow n = 1 \rangle \rangle$$

If we send the message get\_f to fly\_ext, then we get the following

computation:

$$\begin{align*}
fly_{ext} \leftarrow get_f & \rightarrow Sel(fly_{ext}, get_f, \lambda s''.s'') \\
& \rightarrow (\lambda s. (s \leftarrow f) \langle s \leftrightarrow n = 1 \rangle) fly_{ext} \\
& \rightarrow (fly_{ext} \leftarrow f) \langle fly_{ext} \leftrightarrow n = 1 \rangle \\
& \rightarrow Sel(fly_{ext}, f, \lambda s''.s'') \langle fly_{ext} \leftrightarrow n = 1 \rangle \\
& \rightarrow (\lambda s. \lambda s'.s' \leftarrow n) fly_{ext} \langle fly_{ext} \leftrightarrow n = 1 \rangle \\
& \rightarrow \langle fly_{ext} \leftrightarrow n = 1 \rangle \leftarrow n \\
& \rightarrow 1
\end{align*}$$

i.e. the following steps are performed:

1. the method get\_f calls the method *f* with actual parameter the host object itself augmented with the *n* method;

2. the *f* method takes as input the host object augmented with the *n* method, and sends to this object the message *n*, which simply returns the constant 1.

# 3. Type system

In this section, we introduce the syntax of types for $\lambda Obj^\oplus$ and we discuss the most interesting type rules. For the sake of simplicity, we prefer to present first the type system without the rules related with object subsumption (which will be discussed in Section 4). The complete set of rules can be found in Appendices A and B. They are presented in the style of the Edinburgh Logical Framework, (Harper et al. 1993), or equivalently that of PTS, (Barendregt 1992). Examples of terms and their types will be shown in Section 5.

## 3.1. Types

The type expressions are described by the following grammar:

<table><tr><td>σ</td><td>::=</td><td>ι | σ → σ | τ</td><td>(generic-types)</td></tr><tr><td>τ</td><td>::=</td><td>t | prot.R | τ ⊕ m</td><td>(object-types)</td></tr><tr><td>R</td><td>::=</td><td>⟨⟩ | ⟨R, m:σ⟩</td><td>(rows)</td></tr><tr><td>κ</td><td>::=</td><td>*</td><td>(kind of types)</td></tr></table>

In the rest of the article we will use $\sigma$ as meta-variable ranging over generic-types, $\iota$ over constant types, $\tau$ over object-types. Moreover, *t* is a type variable, *R* a metavariable ranging over rows, i.e. unordered sets of pairs (*method label*, *method type*), *m* a method label, and $\kappa$ a metavariable ranging over the unique kind of types *\**.

To ease the notation, we write $\langle \dots \langle \rangle, m_1: \sigma_1 \rangle \dots, m_k: \sigma_k \rangle$ as $\langle m_1: \sigma_1, \dots, m_k: \sigma_k \rangle$ or $\langle \bar{m}_k: \bar{\sigma}_k \rangle$ or else simply $\langle \bar{m}: \bar{\sigma} \rangle$ in the case the subscripts can be omitted. Similarly, we write either $\tau \oplus \bar{m}_k$ or $\tau \oplus \bar{m}$ for $\tau \oplus m_1 \dots \oplus m_k$, and $\tau \oplus \bar{m}$, $n$ for $\tau \oplus m_1 \dots \oplus m_k \oplus n$. If $R \equiv \langle \bar{m}: \bar{\sigma} \rangle$, then we denote $\bar{m}$ by $\bar{R}$, and we write $R_1 \subseteq R_2$ if $R_1 \equiv \langle \bar{m}: \bar{\sigma}_1 \rangle$ and $R_2 \equiv \langle \bar{m}: \bar{\sigma}_2 \rangle$. Finally by $\langle R_1, R_2 \rangle$ we denote concatenation of rows $R_1$ and $R_2$.

As in (Fisher et al. 1994), we may consider object-types as a form of recursively-defined types. Object-types in the form
pro t.R ⊕ $\overline{m}$ are named pro -types, where pro is a binder for the type-variable t representing “self” (we use α -conversion of type-variables bound by pro ) The intended meaning of a pro -type pro t.⟨ $\overline{m}$ : $\overline{\sigma}$⟩ ⊕ $\overline{n}$ is the following:

– the methods in $\overline{m}$ are the ones which are present in the pro -type;

– the methods in $\overline{n}$ , being in fact a subset of those in $\overline{m}$ , are the methods that are available and which can be invoked (it follows that the pro -type pro t.⟨ $\overline{m}$ : $\overline{\sigma}$⟩ ⊕ $\overline{m}$ corresponds exactly to the object-type class t.⟨ $\overline{m}$ : $\overline{\sigma}$⟩ in (Fisher et al. 1994));

– the methods in $\overline{m}$ that do not appear in $\overline{n}$ are methods which cannot be invoked: they are potentially reserved for later object extensions.

We can say that, ultimately, the operator “⊕” is used to activate those methods that were previously just reserved in a pro -type. Essentially, ⊕ is the “type counterpart” of the operator ←⊕ on terms. In the type system, we can extend an object e with a new method m , having type σ , only if it is possible to assign to e an object-type of the form pro t.⟨ R, m : σ⟩ ⊕ $\overline{n}$ , m . This reservation mechanism is crucial to guaranteeing the soundness of the type system. In the rest of the section, we introduce the type judgments and discuss the most significant typing rules.

3.2. Contexts and judgments

The contexts have the following form:

$$
\Gamma ::= \varepsilon \mid \Gamma, x:\sigma \mid \Gamma, t \leftarrow \tau
$$

Our type assignment system uses judgments of the following
shapes:

$$
\Gamma \vdash ok \qquad \Gamma \vdash \sigma : * \qquad \Gamma \vdash e : \sigma \qquad \Gamma \vdash \tau_1 \leftarrow \tau_2
$$

The intended meaning of the first three judgments is standard,
namely they assert that contexts and types are well-formed, and
that the type σ is assigned to a term e in a context Γ. The
intended meaning of Γ ⊢ τ₁ ↘ τ₂ is that τ₁ is the type of a pos-
sible extension of an object having type τ₂, in a given context
Γ. As in (Bruce 1994), and in (Bono & Liquori 1994; Bono et
al. 1996, 1997; Bono & Bugliesi 1999), this judgment formal-
izes the notion of method-specialization (or protocol-extension),
i.e. the capability to “inherit” the type of the methods of the
prototype. The relation ↘ is called the “matching relation”.
Accordingly we refer to this latter kind of judgment as a “match-
ing judgment”.

3.3. Well formed context and types

The type rules for well-formed contexts are quite standard;
however, some remarks are in order. In the (Cont − t) rule:

$$
\frac{\Gamma \vdash \mathrm{pro\thinspace t.R} \oplus \bar{m} : * \quad t \notin \mathrm{Dom}(\Gamma)}{\Gamma, t \leftarrow \sharp \mathrm{pro\thinspace t.R} \oplus \bar{m} \vdash \mathrm{ok}}
$$

we require that the object-types used to bind variables are not
variable types themselves: this condition does not have any

serious restriction, and has been put in the type system in order
to make the proofs of its properties more direct.

The (*Type-Pro*) rule:

$$
\frac{\Gamma, t \leftarrow \sharp \mathrm{prot}.R \vdash \sigma : * \quad m \notin \bar{R}}{\Gamma \vdash \mathrm{prot}.\langle R, m : \sigma \rangle : *}
$$

asserts that the object-type prot .⟨ R, m : σ⟩ is well-formed if the object-type prot .R is well-formed and the type σ is well-formed under the hypothesis that t is an object-type containing the methods in $\overline{R}$. Since σ may contain a subexpression of the form t ⊕ n , with n ∈ $\overline{R}$ , we need to introduce in the context the hypothesis t ↘ prot .R to prove that t ⊕ n is a well-formed type.

The (*Type-Extend*) rule:

$$
\frac{\Gamma \vdash \tau \leftarrow \sharp \mathrm{prot}.R \quad \overline{m} \subseteq \bar{R}}{\Gamma \vdash \tau \oplus \overline{m} : *}
$$

asserts that in order to activate the methods $\overline{m}$ in the object-type
$\tau$, the methods $\overline{m}$ need to be present (reserved) in $\tau$.

3.4. Matching rules

The (*Match-Pro*) rule:

$$
\frac{\Gamma \vdash \mathrm{prot}.R_1 \oplus \bar{m} : * \quad \Gamma \vdash \mathrm{prot}.R_2 \oplus \bar{n} : * \quad R_2 \subseteq R_1 \quad \bar{n} \subseteq \bar{m}}{\Gamma \vdash \mathrm{prot}.R_1 \oplus \bar{m} \leftarrow \sharp \mathrm{prot}.R_2 \oplus \bar{n}}
$$

asserts that an object-type with more reserved and more avail-
able methods specializes an object-type with fewer reserved and
fewer available methods.

The (*Match-Var*) rule:

$$
\frac{\Gamma_1, t \leftarrow \tau_1, \Gamma_2 \vdash \tau_1 \oplus \bar{m} \leftarrow \tau_2}{\Gamma_1, t \leftarrow \tau_1, \Gamma_2 \vdash t \oplus \bar{m} \leftarrow \tau_2}
$$

makes available the matching judgments present in the con-
text. It asserts that, if a context contains the hypothesis that a
type variable *t* specializes a type *τ*₁, and moreover *τ*₁, incre-
mented with a set of methods *m*, itself specializes a type *τ*₂,
then, by transitivity of the matching relation, *t*, incremented by
the methods in *m*, specializes *τ*₂.

The (*Match-t*) rule:

$$
\frac{\Gamma \vdash t \oplus \bar{m} : * \quad \bar{n} \subseteq \bar{m}}{\Gamma \vdash t \oplus \bar{m} \leftarrow t \oplus \bar{n}}
$$

concerns object-types built from the same type variable. It sim-
ply asserts that a type with more available methods specializes
a type with fewer available methods.

3.5. Terms rules

The type rules for λ-terms are self-explanatory and hence they
need no further justification. Concerning those for object terms,
the (Empty) rule assigns to an empty object an empty pro-type,
while the (Pre-Extend) rule:

$$
\frac{\Gamma \vdash e : \mathrm{pro}.R_1 \oplus \bar{m} \quad \Gamma \vdash \mathrm{pro}.\langle R_1, R_2 \rangle \oplus \bar{m} : *}{\Gamma \vdash e : \mathrm{pro}.\langle R_1, R_2 \rangle \oplus \bar{m}}
$$
asserts that an object *e* having type *prot*.R₁ ⊕ *m* can be considered also an object having type *prot*.⟨R₁, R₂⟩ ⊕ *m*, i.e. with more reserved methods. This rule has to be used in conjunction with the (*Extend*) one; it ensures that we can dynamically add fresh methods. Notice that (*Pre-Extend*) *cannot* be applied when *e* is a variable *s* representing self; in fact, as explained in the Remark 3.1 below, the type of *s* can only be a type variable. This fact is crucial for the soundness of the type system.

The (*Extend*) rule:

$$
\frac{
  \begin{array}{l}
    \Gamma \vdash e_1 : \tau \qquad \Gamma \vdash \tau \nparallel prot.\langle R, n : \sigma \rangle \oplus \bar{m} \\
    \Gamma, t \nparallel prot.\langle R, n : \sigma \rangle \oplus \bar{m}, n \vdash e_2 : t \to \sigma
  \end{array}
}{
  \Gamma \vdash \langle e_1 \leftarrow \oplus n = e_2 \rangle : \tau \oplus n
}
$$

can be applied in the following cases:

1. when the object $e_1$ has type $prot.\langle R, n:\sigma \rangle \oplus \bar{m}$ (or, by a previous application of the ($Pre-Extend$) rule, $prot.R \oplus \bar{m}$). In this case the object $e_1$ is extended with the (fresh) method $n$;

2. when $\tau$ is a type variable $t$. In this case $e_1$ can be the variable $s$, and a self-inflicted extension takes place.

The matching constraint on *t* in the environment is the same as the final type for the object ⟨e₁<sub>s</sub>⊕n = e₂⟩; this allows for a recursive call of the method *n* inside the expression *e₂*, defining the method *n* itself.

The (*Override*) rule:

$$
\frac{
  \begin{array}{l}
    \Gamma \vdash e_1 : \tau \qquad \Gamma \vdash \tau \nparallel prot.\langle R, n : \sigma \rangle \oplus \bar{m}, n \\
    \Gamma, t \nparallel prot.\langle R, n : \sigma \rangle \oplus \bar{m}, n \vdash e_2 : t \to \sigma
  \end{array}
}{
  \Gamma \vdash \langle e_1 \leftarrow \oplus n = e_2 \rangle : \tau
}
$$

is quite similar to the (*Extend*) rule, but it is applied when the method *n* is already available in the object *e*₁, hence the body of *n* is overridden with a new one.

**Remark 3.1** By inspecting the (*Extend*) and (*Override*) rules, one can see why the type of the object itself is always a type variable. In fact, the body *e*₂ of the newly added method *n* needs to have type *t*→*σ*. Therefore, if *e*₂ reduces to a value, this value has to be a λ-abstraction in the form λs.e'₂. It follows that, in assigning a type to e'₂, we must use a context containing the hypothesis *s*: *t*. Since no subsumption rule is available, the only type we can deduce for *s* is *t*. □

The (*Send*) rule:

$$
\frac{
  \begin{array}{l}
    \Gamma \vdash e : \tau \quad \Gamma \vdash \tau \nparallel prot.\langle R, n : \sigma \rangle \oplus \bar{m}, n \\
    \qquad \qquad \qquad \Gamma \vdash e \Leftarrow n : \sigma[\tau/t]
  \end{array}
}{
  \Gamma \vdash e
}
$$

is the standard rule that one can expect from a type system combining $\lambda Obj$ and matching. We require that the method we are invoking is available in the recipient of the message.

In the (*Select*) rule:

$$
\frac{
  \begin{array}{l}
    \Gamma \vdash e_1 : \tau \qquad \Gamma \vdash \tau \nparallel prot.\langle R, n : \sigma \rangle \oplus \bar{m}, n \\
    \Gamma, t \nparallel prot.\langle R, n : \sigma \rangle \oplus \bar{m}, n \vdash e_2 : t \to t \oplus n
  \end{array}
}{
  \Gamma \vdash Sel(e_1, n, e_2) : \sigma[\tau \oplus n/t]
}
$$

the first two conditions ensure that the *n* method is available in *e*₁, while the last one that *e*₂ is a function that transforms an object into a more refined one.

4. Object subsumption

While the type assignment system $\lambda Obj^{\oplus}$, presented in Section 3, allows self-inflicted extension, it does not allow object subsumption. This is not surprising: in fact, we could (by subsumption) first hide a method in an object, and then add it again with a type incompatible with the previous one. The papers (Abadi & Cardelli 1996; Fisher & Mitchell 1994; Fisher et al. 1994; Bono & Liquori 1994) propose different type systems for prototype-based languages, where subsumption is permitted only in absence of object extension (and a fortiori self-inflicted extension). In this section, we devise a conservative extension of $\lambda Obj^{\oplus}$, called $\lambda Obj_S^{\oplus}$, to accommodate width-subtyping. The new rules for $\lambda Obj_S^{\oplus}$ appear in Appendix B.

In order to be able to add a subsumption rule to the typing system, we introduce another kind of object-types, i.e. $obj.R \oplus \bar{m}$, called *obj*-types. The main difference between the *pro*-types and the *obj*-types consists in the fact that the (*Pre-Extend*) rule cannot be applied when an object has type $obj.R \oplus \bar{m}$; it follows that the type $obj.R \oplus \bar{m}$ permits extensions of an object only by enriching the list $\bar{m}$, i.e. by making active its reserved methods. This approach to subsumption is inspired by the one in (Fisher & Mitchell 1995; Liquori 1997). Formally, we need to extend the syntax of types with *obj*-types and we need to introduce the new kind of *rigid*, i.e. non-extensible, types:

$$
\tau ::= \dots | obj.t.R \quad (\text{object-types})
$$

$$
\kappa ::= \dots | *_{rgd} \quad (\text{kind of types})
$$

The subset of rigid types contains the *obj*-types and is closed under the arrow constructor. In order to axiomatize this, we introduce the judgment $\Gamma \vdash \tau : *_{rgd}$, whose rules appear in Appendix B. Intuitively, we can use the matching relation as a subtyping relation only when the type in the conclusion is rigid:

$$
\frac{\Gamma \vdash e : \tau_1 \quad \Gamma \vdash \tau_1 \nparallel \tau_2 \quad \Gamma \vdash \tau_2 : *_{rgd}}{\Gamma \vdash e : \tau_2} \quad (\text{Subsume})
$$

Actually, this is the rule performing object subsumption. It permits to use objects with an extended signature in any context expecting objects with a shorter one.

It is important to point out that, so doing, we do not need to introduce another partial order on types, i.e. an ordinary subtyping relation, to deal with subsumption. By introducing the sub-kind of rigid types, we make the matching relation compatible with subsumption, and hence we can make it play the role of the width-subtyping relation. This is in sharp contrast with the uses of matching proposed in the literature (Bruce 1994; Bruce et al. 1997; Bono & Bugliesi 1999). Hence, in our type assignment system, the matching is a relation on types compatible with a limited subsumption rule.

Most of the rules for *obj*-types are a rephrasing of the rules presented so far, replacing the binder *pro* with *obj*. We remark
# 6. Soundness of the Type System

In this section, we prove the crucial property of our type system, i.e. the Subject Reduction theorem. As a corollary, we shall derive the fundamental result of the paper, i.e. Type Soundness, which ensures that a well-typed expression will never raise the critical message-not-understood runtime error.

The proof of the Subject Reduction theorem needs a preliminary series of lemmas and propositions, presenting basic and auxiliary properties, which are proved by inductive arguments. The section being quite technical, we have preferred to give here only the statements, postponing the fully documented proofs to Appendices C and D.

First we address the plain type assignment system without subsumption $\lambda Obj^{\oplus}$, then in Section 6.1 we extend the Subject Reduction property to the whole type system $\lambda Obj_S^{\oplus}$. We are going to establish this via a hierarchy of “corner-stone” results. We start by addressing proof trees (Lemma 6.1) and proof environments (Lemma 6.2), then we focus on object-types, method-types and matching (Lemmas 6.3, 6.5, 6.6, Proposition 6.4), finally we deal with substitution and the main type assignment judgment (Propositions 6.7 and 6.8).

In the presentation of the formal results, we use $\alpha, \beta$ as metareferences for generic types and $\rho, \nu$ for object-types. Moreover, $\mathcal{A}$ is a metavariable ranging on statements of the forms ok, $\alpha : *$, $\nu \not\vdash \rho$, $e : \beta$, and $C$ on statements in the forms $x:\sigma$, $t \not\vdash \tau$.

**Lemma 6.1 (Sub-derivation)**

(i) If $\Delta$ is a derivation of $\Gamma_1, \Gamma_2 \vdash \mathcal{A}$, then there exists a sub-derivation $\Delta' \subseteq \Delta$ of $\Gamma_1 \vdash \text{ok}$.

(ii) If $\Delta$ is a derivation of $\Gamma_1, x:\sigma, \Gamma_2 \vdash \mathcal{A}$, then there exists a sub-derivation $\Delta' \subseteq \Delta$ of $\Gamma_1 \vdash \sigma : *$.

(iii) If $\Delta$ is a derivation of $\Gamma_1, t \not\vdash \tau, \Gamma_2 \vdash \mathcal{A}$, then there exists a sub-derivation $\Delta' \subseteq \Delta$ of $\Gamma_1 \vdash \tau : *$.

**Lemma 6.2 (Weakening)**

(i) If $\Gamma_1, \Gamma_2 \vdash \mathcal{A}$ and $\Gamma_1, \mathcal{C}, \Gamma_2 \vdash \text{ok}$, then $\Gamma_1, \mathcal{C}, \Gamma_2 \vdash \mathcal{A}$.

(ii) If $\Gamma_1 \vdash \mathcal{A}$ and $\Gamma_1, \Gamma_2 \vdash \text{ok}$, then $\Gamma_1, \Gamma_2 \vdash \mathcal{A}$.

**Lemma 6.3 (Well-formed object-types)**

(i) $\Gamma \vdash \text{pro t.R} \oplus \bar{m} : *$ if and only if $\Gamma \vdash \text{pro t.R} : *$ and $\bar{m} \subseteq \bar{R}$.

(ii) $\Gamma \vdash t \oplus \bar{m} : *$ if and only if $\Gamma$ contains $t \not\vdash \text{pro t.R} \oplus \bar{n}$, with $\bar{m} \subseteq \bar{R}$.

**Proposition 6.4 (Matching is well-formed)**

If $\Gamma \vdash \tau_1 \not\vdash \tau_2$, then $\Gamma \vdash \tau_1 : *$ and $\Gamma \vdash \tau_2 : *$.

**Lemma 6.5 (Matching)**

(i) $\Gamma \vdash \text{pro t.R}_1 \oplus \bar{m} \not\vdash \tau_2$ if and only if $\Gamma \vdash \text{pro t.R}_1 \oplus \bar{m} : *$ and $\Gamma \vdash \tau_2 : *$ and $\tau_2 \equiv \text{pro t.R}_2 \oplus \bar{n}$, with $\Gamma_2 \subseteq \Gamma_1$ and $\bar{n} \subseteq \bar{m}$.

(ii) $\Gamma \vdash \tau_1 \not\vdash t \oplus \bar{n}$ if and only if $\Gamma \vdash \tau_1 : *$ and $\tau_1 \equiv t \oplus \bar{m}$, with $\bar{n} \subseteq \bar{m}$.

(iii) $\Gamma \vdash t \oplus \bar{m} \not\vdash \text{pro t.R}_2 \oplus \bar{n}$ if and only if $\Gamma$ contains $t \not\vdash \text{pro t.R}_1 \oplus \bar{p}$, with $\Gamma_1 \subseteq \Gamma_2 \subseteq \bar{m} \cup \bar{p}$.

(iv) (Reflexivity) If $\Gamma \vdash \rho : *$ then $\Gamma \vdash \rho \not\vdash \rho$.

(v) (Transitivity) If $\Gamma \vdash \tau_1 \not\vdash \rho$ and $\Gamma \vdash \rho \not\vdash \tau_2$, then $\Gamma \vdash \tau_1 \not\vdash \tau_2$.

(vi) (Uniqueness) If $\Gamma \vdash \tau_1 \not\vdash \text{pro t.}(R_1, m:\sigma_1)$ and $\Gamma \vdash \tau_1 \not\vdash \text{pro t.}(R_2, m:\sigma_2)$, then $\sigma_1 \equiv \sigma_2$.

(vii) If $\Gamma \vdash \tau_1 \not\vdash \tau_2$ and $\Gamma \vdash \tau_2 \oplus m : *$, then $\Gamma \vdash \tau_1 \oplus m \not\vdash \tau_2 \oplus m$.

(viii) If $\Gamma \vdash \tau_1 \oplus m \not\vdash \text{pro t.R} \oplus \bar{n}$, then $\Gamma \vdash \tau_1 \not\vdash \text{pro t.R} \oplus \bar{n} - m$.

(ix) If $\Gamma \vdash \rho \oplus m : *$, then $\Gamma \vdash \rho \oplus m \not\vdash \rho$.

**Lemma 6.6 (Match weakening and Method types)**

(i) If $\Gamma_1, t \not\vdash \rho, \Gamma_2 \vdash \mathcal{A}$ and $\Gamma_1 \vdash \tau \not\vdash \rho$, with $\tau$ a pro-type, then $\Gamma_1, t \not\vdash \tau, \Gamma_2 \vdash \mathcal{A}$.

(ii) If $\Gamma \vdash \text{pro t.}(R, n:\sigma) \oplus \bar{m} : *$, then $\Gamma, t \not\vdash \text{pro t.}(R, n:\sigma) \oplus \bar{m} \vdash \sigma : *$.

**Proposition 6.7 (Substitution)**

(i) If $\Gamma_1, x:\sigma, \Gamma_2 \vdash \mathcal{A}$ and $\Gamma_1 \vdash e : \sigma$, then $\Gamma_1, \Gamma_2 \vdash \mathcal{A}[e/x]$.

(ii) If $\Gamma_1, t \not\vdash \tau, \Gamma_2, \Gamma_3 \vdash \mathcal{A}$ and $\Gamma_1, t \not\vdash \tau, \Gamma_2 \vdash \rho \not\vdash \tau$, then $\Gamma_1, t \not\vdash \tau, \Gamma_2, \Gamma_3[\rho/t] \vdash \mathcal{A}[\rho/t]$.

(iii) If $\Gamma_1, t \not\vdash \tau, \Gamma_2 \vdash \mathcal{A}$ and $\Gamma_1 \vdash \rho \not\vdash \tau$, then $\Gamma_1, \Gamma_2[\rho/t] \vdash \mathcal{A}[\rho/t]$.

**Proposition 6.8 (Types of expressions are well-formed)**

If $\Gamma \vdash e : \beta$, then $\Gamma \vdash \beta : *$.

We can state now the fundamental Subject Reduction property for our type system.

**Theorem 6.9 (Subject Reduction, $\lambda Obj^{\oplus}$)**

If $\Gamma \vdash e : \beta$ and $e \to e'$, then $\Gamma \vdash e' : \beta$.

Finally we derive the Type Soundness theorem, which guarantees, among other properties, that every closed and well-typed expression will not produce the message-not-found runtime error. This error arises whenever we search for a method $m$ into an expression that does not reduce to an object which has the method $m$ in its interface. First we need a definition.

**Definition 6.10** The set of wrong terms is defined by the following grammar:

$$ \mathit{wrong} ::= \mathit{Sel}(\langle\rangle, m, e) \mid \mathit{Sel}(\langle\lambda x.e\rangle, m, e') \mid \mathit{Sel}(c, m, e) $$

By a direct inspection of the typing rules for terms, one can immediately see that wrong cannot be typed. Hence, the Type Soundness follows as a corollary of the Subject Reduction theorem.

**Corollary 6.11 (Type Soundness)**

If $\varepsilon \vdash e : \beta$, then $e \dashv\dashv C[\mathit{wrong}]$, where $C[\ ]$ is a generic context in $\lambda Obj^{\oplus}$, i.e. a term with an "hole" inside it.
## 6.1. Soundness of the Type System with Subsumption

$$ \lambda Obj_S^{\oplus} $$

The proof of Type Soundness for the type assignment system with subsumption $\lambda Obj_S^{\oplus}$ is quite similar to the corresponding proof for the plain type system. In particular, all the preliminary lemmas and their corresponding proofs remain almost the same; only the proof of the crucial Theorem 6.9 needs to be modified significantly. Therefore, we do not document the whole statements of the preliminary lemmas, but we just remark the points where new arguments are needed.

In particular, Lemmas 6.1 (Sub-derivation), 6.2 (Weakening), 6.4 (Matching is well-formed), 6.7 (Substitution), 6.8 (Types of expressions are well-formed) are valid also for the type assignment with subsumption. Conversely, we need to extend Lemmas 6.3, 6.5, 6.6, as follows.

In Lemma 6.3 (Well-formed object-types), the point (ii) needs to be rephrased as:

(ii) $\Gamma \vdash t \oplus \bar{m} : *$ if and only if $\Gamma$ contains either $t \not\vdash prot.R \oplus \bar{n}$ or $t \not\vdash objt.R \oplus \bar{n}$, with $\bar{m} \subseteq \bar{R}$.

In Lemma 6.5 (Matching), the point (vi) needs to be rephrased as:

(vi) (Uniqueness) if $\Gamma \vdash \tau_1 \not\vdash objt.\langle R_1, m:n_1 \rangle$ and $\Gamma \vdash \tau_1 \not\vdash objt.\langle R_2, m:n_2 \rangle$, then $\sigma_1 \equiv \sigma_2$.

Moreover, in the same lemma the following points need to be added:

(i') $\Gamma \vdash objt.R_1 \oplus \bar{m} \not\vdash \tau_2$ if and only if $\Gamma \vdash prot.R_1 \oplus \bar{m} : *$ and $\Gamma \vdash \tau_2 : *$ and $\tau_2 \equiv objt.R_2 \oplus \bar{n}$, with $R_2 \subseteq R_1$ and $\bar{n} \subseteq \bar{m}$.

(iii') $\Gamma \vdash t \oplus \bar{m} \not\vdash objt.R_2 \oplus \bar{n}$ if and only if $\Gamma$ contains either $t \not\vdash objt.R_1 \oplus \bar{p}$ or $t \not\vdash prot.R_1 \oplus \bar{p}$, with $R_2 \subseteq R_1$ and $\bar{n} \subseteq \bar{m} \cup \bar{p}$.

(viii') If $\Gamma \vdash \tau_1 \oplus m \not\vdash objt.R \oplus \bar{n}$, then $\Gamma \vdash \tau_1 \not\vdash objt.R \oplus \bar{n}-m$.

In Lemma 6.6 (Method types), the point (ii) needs to be rewritten as:

(ii) If $\Gamma \vdash prot.\langle R, n:n \rangle \oplus \bar{m} : *$ or $\Gamma \vdash objt.\langle R, n:n \rangle \oplus \bar{m} : *$ can be derived, then $\Gamma, t \not\vdash objt.\langle R, n:n \rangle \oplus \bar{m} \vdash \sigma : *$.

A new lemma, stating some elementary properties of types with covariant variables and rigid types is necessary.

**Lemma 6.12 (Covariant variables and rigid types)**

(i) If $t$ is covariant in $\sigma$ and $\Gamma \vdash \sigma : *_{rgd}$ and $\Gamma \vdash \tau_1 \not\vdash \tau_2$, then $\Gamma \vdash \sigma[\tau_1/t] \not\vdash \sigma[\tau_2/t]$.

(ii) If $\Gamma \vdash \sigma_1 : *_{rgd}$ and $\Gamma \vdash \sigma_2 : *_{rgd}$, then $\Gamma \vdash \sigma_1[\sigma_2/t] : *_{rgd}$.

Finally, Subject Reduction for the type assignment system with subsumption has the usual formulation, but it needs a more complex proof, which appears in Appendix D.

**Theorem 6.13 (Subject Reduction, $\lambda Obj_S^{\oplus}$)**
If $\Gamma \vdash e : \beta$ and $e \to e'$, then $\Gamma \vdash e' : \beta$.

## 7. Object evolution and object reclassification

In the software world, the urgency to model phenomena like 'a frog may turn into a prince, if kissed' emerged at least since 1993 (Taivalsaari 1993). Within the class-based paradigm, this capability is known as *object reclassification*, which in fact allows for changing *at runtime* the class membership of an object while retaining its identity.

Some languages provide built-in support for reclassification: for instance, Smalltalk offers the *becomes* method, while in Python the `_class_` attribute may be assigned new values. However, these mechanisms are notoriously unsafe, hence strongly-typed languages, like e.g. Java, do not support this functionality.

A particular kind of reclassification, named *object evolution* (Beck 1993; Cohen & Gil 2009), is less general, not allowing for changes as drastic as those permitted by full-fledged reclassification. Namely, in object evolution the dynamic changes to an object's class are *monotonic*, i.e. an object may gain, but never lose, capabilities.

In this section, we investigate how $\lambda Obj^{\oplus}$'s expressivity relates to evolution and reclassification. That is, we connect a functional, prototype-based calculus, as $\lambda Obj^{\oplus}$, with the mechanisms provided by imperative, class-based environments, i.e. evolution and reclassification. But, before addressing such a comparison, we comment briefly on the perspective we take.

**Functional vs imperative semantics.** Since $\lambda Obj^{\oplus}$ is a functional calculus, any object modification, i.e. extension and override, yields a new, completely independent object. An immediate consequence is that our setting, differently from the class-based one, does not support in the present form any notion of *state*, and therefore of *object identity*. This means that, while an object keeps its identity after evolving or being reclassified in imperative settings, in $\lambda Obj^{\oplus}$ we need to build different objects to simulate its behavior.

This fact can be seen as a limitation of our comparison, but it is precisely the point of our effort. Namely, we will explore the possibility of modeling evolution and reclassification, which are mechanisms proper of the class-based scenario, via the prototype-based $\lambda Obj^{\oplus}$. In fact, our ultimate goal is to point out the expressive power of our calculus.

We believe that our investigation has two firm motivations. First, since evolution and reclassification are very useful to capture real-world phenomena, it is natural to try to make them available in the alternative, prototype-based setting. Second, the methodology of using calculi based on objects to model those based on classes has a long tradition, which relies on the fact that 'class-based notions can be emulated in the object-based model by more primitive notions, and these more primitive notions can be combined in more flexible ways than in a strict class discipline' (Abadi & Cardelli 1996)<fnref n="3" />.

**Embedding vs delegation.** Capitalizing on the concept of code reuse, in object-orientation, *inheritance* is the main tool for sharing common behavior across objects.

<footnote n="3">³ For instance, to model a class in $\lambda Obj^{\oplus}$ one could define a prototype object, and then invoke its methods to generate objects as these were instances of that class (see Example 5.1).</footnote>
In the prototype-based paradigm, inheritance is usually realized by building new objects that include some members of the existing objects: actually, these members may be either *embedded* into the host object or *delegated* to the donors themselves. In the former case, the host contains its own copies of the members of the donor; in the latter one, the members of the donor are shared with the host.

In fact, both categories of inheritance are available in $\lambda Obj^\oplus$. On the one hand, object extension and self-extension carry out (implicit) embedding, because all the methods of the donor are inherited by the host at the time of its creation, when the methods are obtained and embedded. On the other hand, if a new object is built from scratch, it is possible to select *individual* methods from donors and ask the latter to execute such methods, thus carrying out inheritance by (explicit) delegation.

In this section, we will employ the two kinds of inheritance, i.e. embedding and delegation, to model the evolution and reclassification mechanisms, respectively.

## 7.1. Object evolution

As explained above, evolution is a limited form of reclassification, where the dynamic changes to an object's class are *monotonic*, i.e. the object may gain, but never lose, capabilities (Cohen & Gil 2009). In other words, once an object evolves, it cannot retrace its steps and be reclassified into its previous class. Such a restricted scenario integrates well with static typing, as it is guaranteed that any message understood by an object prior to an evolution operation is understood after the operation as well.

In this section we consider I-evolution, an approach to evolution based on *standard inheritance*, where an object can evolve into any subclass of its own class (Cohen & Gil 2009). An I-evolution operation replaces, at runtime, the type of an object with the type of a selected subclass. Since a subclass may only extend its parent class, I-evolution may be encoded naturally in $\lambda Obj^\oplus$ through self-extension. To provide an example, we model here a person, named Mary, who might become either a student or a worker:

$$ 
\begin{align*}
\mathit{mary} &\triangleq \langle \mathit{name} = \text{"Mary"}, \\
\mathit{student} &= \lambda s.\lambda m.\langle s \oplus \mathit{number} = m \rangle, \\
\mathit{worker} &= \lambda s.\lambda n.\langle s \oplus \mathit{salary} = n \rangle \rangle
\end{align*}
$$

It turns out that this prototype object can be typed as follows:

```
mary : prot.⟨ name : String,
    student : N → t ⊕ number,
    worker : N → t ⊕ salary,
    number : N,
    salary : N⟩ ⊕ name, student, worker
```

An immediate consequence is that the two following calls can be typed too:

$$ \mathit{mary} \leftarrow \mathit{student}(26) \quad (\mathit{mary} \leftarrow \mathit{student}(26)) \leftarrow \mathit{worker}(40K) $$

In fact, by applying the type soundness property 6.11, such a typability ensures that the two method invocations will not raise message-not-found runtime errors. These can be used to realize evolution, as we are going to show.

When the *student* method is sent to *mary*, then it reduces, i.e. evolves, to *mary*<sub>S</sub> (that is, *mary* ⇝ *student* (26) → *mary*<sub>S</sub>), a new object which inherits, by implicit embedding, all the methods of the former, and augments them with the extra *number* method:

$$ 
\begin{align*}
\mathit{mary}_S &\triangleq \langle \mathit{name} = \text{"Mary"}, \\
\mathit{student} &= \lambda s.\lambda m.\langle s \oplus \mathit{number} = m \rangle, \\
\mathit{worker} &= \lambda s.\lambda n.\langle s \oplus \mathit{salary} = n \rangle, \\
\mathit{number} &= 26 \rangle
\end{align*}
$$

Afterwards, Mary may become a student-and-worker, again by implicit embedding, via the second call *mary*<sub>S</sub> ⇝ *worker* (40K), which reduces to:

$$ 
\begin{align*}
\mathit{mary}_{SW} &\triangleq \langle \mathit{name}, \dots, \mathit{number} = \text{as in } \mathit{mary}_S, \\
\mathit{salary} &= 40K \rangle
\end{align*}
$$

Obviously, a behaviorally equivalent object *mary*<sub>WS</sub> could be obtained by swapping the order of the calls to the *student* and *worker* methods.

In (Cohen & Gil 2009), besides I-evolution, two extra approaches to evolution are developed, based on *mixin* and *shakein* inheritance. We are confident that we can suitably simulate in our calculus many aspects of these features, but more work needs to be done to reduce the formal overhead.

## 7.2. Object reclassification

As stated at the beginning of Section 7, the potential of reclassification is highly valued in the software world, because the capability of changing at runtime the class membership of an object, while retaining its identity, increases dramatically the expressive power of the object-oriented paradigm. One major contribution to the development of reclassification features has produced the Java-like Fickle language, in its incremental versions (Drossopoulou et al. 2001, 2002; Damiani et al. 2003). These papers, combine reclassification with a strong type system and achieve the formal result that well-typed objects will never access non-existing class components.

In this section, we explore how $\lambda Obj^\oplus$ may be used to emulate the mechanisms implemented in Fickle. We proceed, suggestively, by working out a case study: first we write an example in Fickle which illustrates the essential ingredients of the reclassification, then we devise and discuss the possibilities of its encoding in $\lambda Obj^\oplus$.

### 7.2.1. Reclassification in Fickle

Fickle is an imperative, class-based, strongly-typed language, where classes are types and subclasses are subtypes. It is statically typed, via a type and effect system which is proved to be sound w.r.t. the operational semantics. To develop the example in this section, we refer to the second version of the language (known as Fickle<sub>II</sub> (Drossopoulou et al. 2002)).
```java
abstract root class Person extends Object {
    string name;
    abstract void emp(int n) {Person};
}

state class Student extends Person {
    int id;
    Student(string s, int m) {} {} {name:=s; id:=m};
    void emp(int n) {Person} {this=>Worker; sal:=n};
}

state class Worker extends Person {
    int sal;
    Worker(string s, int n) {} {} {name:=s; sal:=n};
    void emp(int n) {} {} {sal:=sal+n};
    void reg(int m) {Person} {this=>Student; id:=m};
}
```

<caption>Figure 3 Person-Student-Worker example</caption>

In the Fickle scenario, an abstract class C has two non-overlapping concrete subclasses A and B, where the three classes must be of two different kinds: C is a root class, whereas A and B are state ones. In fact, one finds in root classes, such as C, the declaration of the (private) attributes (a.k.a. fields) and the (public) methods which are common to its state subclasses. On the other hand, state classes, such as A and B, are intended to serve as targets of reclassifications, hence their declaration contains the extra attributes and methods that exclusively belong to each of them.

The reclassification mechanism allows an object in a state class, say A, to become an object of the state class B (or, vice versa, moving from B to A) through the execution of a reclassification expression. The semantics of this operation, which may appear in the body of methods, is that the attributes of the object belonging to the source class are removed, those common to the two classes (which are in C) are retained, and the ones belonging to the target class are added to the object itself, without changing its identity. The same happens to the methods component, with the difference that the abstract methods declared in C (therefore common to A and B) may have different bodies in the two subclasses: when this is the case, reclassifying an object means replacing the bodies of the involved methods, too.

In the example of Figure 3, written in Fickle syntax (hence we use a “code” font), we first introduce the class Person, with an attribute to name a person and an abstract method to employ him/her. Then we add two subclasses, to model students and workers, with the following intended meaning<fnref n="4" />. The Student class extends Person via a registration number (id attribute) and by instantiating the emp method. The Worker class extends Person via a remuneration information (sal attribute), a different emp method, and the extra reg method to register as a student.

The root class Person defines the attributes and methods common to its state subclasses Student and Worker (notice that, being its employment method abstract, the root class itself must be abstract, therefore not supplying any constructor).

The classes Student and Worker, being subclasses of a root one (i.e. Person), must be state classes, which means that they may be used as targets of reclassifications. Annotations, like `{ }` and `{Person}`, placed before the bodies of the methods, are named effects and are intended to list the root classes of the objects that may be reclassified by invoking those methods: in particular, the empty effect `{ }` cannot cause any reclassification and the non-empty effect `{Person}` allows to reclassify objects of its subclasses. Let us now consider the following program fragment:

1. Person p,q;

2. p := new Student("Alice",45);

3. q := new Worker("Bob",27K);

After these lines, the variables p and q are bound to a Student and a Worker objects, respectively. To illustrate the key points of the reclassification mechanism, we make Bob become a Student, and Alice first become a Worker and then get a second job:

4. q.reg(57);

5. p.emp(30K);

6. p.emp(14K);

Line 4, by sending the reg message to the object q, causes the execution of the reclassification expression `this => Student:` before its execution, the receiver q is an object of the Worker class, therefore it contains the sal attribute; after it, q is reclassified into the Student class, hence sal is removed, name is not affected, and the id attribute is added and instantiated with the actual parameter.

Coming to the second object p, belonging to Student and representing Alice, line 5 carries out exactly the opposite operation w.r.t. line 4, by reclassifying p into the Worker class via the expression `this => Worker`, with the result that id is no longer available, name preserves its value, and sal is added and instantiated.

The following line 6, therefore, selects the emp method from Worker, not from Student as before, because the object p has been reclassified in the meantime. This latter invocation of emp has the effect of augmenting Alice’s income by the actual parameter value, thus allowing us to model a sort of multi-worker.

### 7.2.2. Embedding inheritance, i.e. self-extension

In this section, we show how to utilize the potential expressive power of the untyped version of the calculus $\lambda Obj^\oplus$ to model reclassification by means of self-extension.

It is apparent that to mimic Fickle’s reclassification mechanism we need a *reversible* extension functionality, to be used first to extend an object with new methods and later to remove from the resulting object some of its methods. Hence, an immediate solution would rely on a massive use of the self-extension

<footnote n="4">⁴ We remark that in the present working example students and workers are *mutually exclusive*, differently from Section 7.1.</footnote>
primitive, as follows:

$$
\begin{align*}
\mathit{alice} &\triangleq \langle \mathit{name} = \text{"Alice"}, \\
\mathit{reg} &= \lambda s.\lambda m. \langle \langle s \leftarrow \oplus \mathit{id} = m \rangle \\
&\qquad \leftarrow \oplus \mathit{emp} = \lambda n.s. \leftarrow \mathit{emp}(n) \rangle, \\
\mathit{emp} &= \lambda s.\lambda m. \langle \langle \langle s \leftarrow \oplus \mathit{sal} = m \rangle \\
&\qquad \leftarrow \oplus \mathit{emp} = \lambda s'.\lambda p. \\
&\qquad \langle s' \leftarrow \oplus \mathit{sal} = (s' \leftarrow \mathit{sal}) + p \rangle \rangle \\
&\qquad \leftarrow \oplus \mathit{reg} = \lambda n.s. \leftarrow \mathit{reg}(n) \rangle \rangle
\end{align*}
$$

Namely, in order to model the example of Figure 3 in $\lambda Obj^⊕$, we define the *alice* prototype object for representing Alice as person, which can be extended to represent either a student or a worker via the *reg* (i.e. registration) or *emp* (i.e. employment) methods. These are intended to play the role of the *Student* and *Worker* constructors of Section 7.2.1, respectively. Upon receiving the *reg* method, *alice* produces a student, via the addition of *id* and the override of the *emp* method. For example, *alice* $\leftarrow reg(45)$ reduces to the following object:

$$
\begin{align*}
\mathit{alice}_S &\triangleq \langle \mathit{name}, \mathit{reg}, \mathit{emp} \rangle = \begin{array}{@{}l@{}}
\text{as in } \mathit{alice}, \\
\mathit{id} = 45, \\
\mathit{emp} = \lambda m.\mathit{alice} \leftarrow \mathit{emp}(m)
\end{array} \\
&\triangleq \langle \mathit{name}, \mathit{reg}, \mathit{emp} \rangle = \begin{array}{@{}l@{}}
\text{as in } \mathit{alice}, \\
\mathit{id} = 45, \\
\mathit{emp} = \lambda m.\mathit{alice} \leftarrow \mathit{emp}(m)
\end{array}
\end{align*}
$$

In this way, the prototype *alice* is stored in the body of the
novel *emp* method, in view of a possible reclassification<fnref n="5" />. This
is the mechanism which will permit *alice*<sub>S</sub> to retrace its steps
and be reclassified in the future. Upon receiving the mes-
sage *emp*, *alice*<sub>S</sub> is reclassified into a worker via the call to
*alice*'s version of *emp*, i.e. its third method body; actually,
*alice*<sub>S</sub> &lt;- emp(30K) reduces to:

$$
\begin{align*}
\mathit{alice}_W &\triangleq \langle \mathit{name}, \mathit{reg}, \mathit{emp} \rangle = \begin{array}{@{}l@{}}
\text{as in } \mathit{alice}, \\
\mathit{sal} = 30K, \\
\mathit{emp} = \lambda s.\lambda n. \\
\phantom{\mathit{emp} = } \langle s \leftarrow \oplus \mathit{sal} = (s \leftarrow \mathit{sal}) + n \rangle, \\
\mathit{reg} = \lambda m.\mathit{alice} \leftarrow \mathit{reg}(m)
\end{array} \\
&\triangleq \langle \mathit{name}, \dots, \mathit{emp}, \mathit{reg} \rangle = \begin{array}{@{}l@{}}
\text{as in } \mathit{alice}_W, \\
\mathit{sal} = (\mathit{alice}_W \leftarrow \mathit{sal}) + 14K
\end{array}
\end{align*}
$$

The effect of the *emp* message therefore produces an object
which is observationally equal to what one would obtain by
“removing” the methods characterizing a student, “restoring” the
original *alice*, and extending it with the methods characterizing
a worker. Notice that the novel version of *emp* implements a
multi-worker object.

In order to complete the encoding of Section’s 7.2.1 example
in $\lambda Obj^⊕$, $\mathit{alice}_W$’s income may be increased by means of a call
to such a novel version of $\mathit{emp}$, which has overridden $\mathit{alice}$’s
third method; that is, $\mathit{alice}_W \Leftarrow \mathit{emp}(14K)$ reduces to:

$$
\begin{align*}
\mathit{alice}_{W_2} &\triangleq \langle \mathit{name}, \dots, \mathit{emp}, \mathit{reg} \rangle &&= \text{as in } \mathit{alice}_W, \\
\mathit{sal} &&= (\mathit{alice}_W \leftarrow \mathit{sal}) + 14K
\end{align*}
$$

**The typability issue.** The above encoding illustrates how re-classification can be faithfully implemented in $\lambda Obj^⊕$ via embedding inheritance. However, the above “liberal” use of the self-extension operation cannot be typed. Achieving static safety raises rather subtle issues as we will presently show.

Let us focus on the prototype *alice* object. The point is that the self-variable, named *s* representing the receiver object, cannot be used in the body of a method added by self-extension to remove methods, in the attempt to restore the receiver before its extension. This is the case, in the example above, of *emp*'s body, added by the second method *reg* and, symmetrically, *reg*'s body, added by *emp*.

We clarify the issue using a simpler object:

$$
\mathit{andback} \triangleq \langle \mathit{extend} = \lambda s. \langle s \leftarrow \oplus \mathit{delete} = \lambda s'. s \rangle \rangle
$$

The difficulty to type *andback* concerns the type returned by
the *delete* method:

$$
\mathit{andback} : \mathit{prot}.\langle \mathit{extend} : t \oplus \mathit{delete}, \mathit{delete} : ? \rangle \oplus \mathit{extend}
$$

We first observe that the type variable *t* would not be a
suitable candidate for ?, because, within the scope of the above
*pro* binder, *t* is the type of the receiver, i.e. the object *already*
extended, which therefore contains the *delete* method itself.

A reasonable proposal would be to type andback with the type
returned by delete:

$$
\mathit{andback} : \tau \triangleq \mathit{prot}.\langle \mathit{extend} : t \oplus \mathit{delete}, \mathit{delete} : \tau \rangle \oplus \mathit{extend}
$$

But then the candidate $\tau$ should satisfy a recursion equation,
and $\lambda Obj^⊕$'s recursion mechanism is not powerful enough to
express such a type.

The rest of Section 7.2 is devoted to design alternative, ty-
pable implementations of reclassification.

**7.2.3. The runtime solution** A first possibility to circumvent the typability problem arising above is plain: the first time we extend an object with new methods, afterwards we keep just overriding the resulting object, without removing methods from it. That is, the first use of the self-extension leads to object extension, whereas all the following ones to object override. It is apparent that this solution realizes reclassification, again, by embedding.

Actually, we may model Figure 3’s example via the following
object:

$$
\begin{align*}
\mathit{alice}' &\triangleq \langle \mathit{name} = \text{"Alice"}, \\
\mathit{reg} &= \lambda s.\lambda m. \langle \langle s \leftarrow \oplus \mathit{id} = m \rangle \leftarrow \mathit{sal} = 0 \rangle, \\
\mathit{emp} &= \lambda s.\lambda m. \langle \langle \langle s \leftarrow \oplus \mathit{id} = 0 \rangle \leftarrow \mathit{sal} = m \rangle \\
&\qquad \leftarrow \oplus \mathit{emp} = \lambda s'.\lambda n. \\
&\qquad \langle \langle s' \leftarrow \oplus \mathit{id} = 0 \rangle \leftarrow \mathit{sal} = (s' \leftarrow \mathit{sal}) + n \rangle \rangle
\end{align*}
$$

Differently from what we did in Section 7.2.2, in this alternative encoding of Alice the variables representing the host object (*s* and *s'*) are never used in a method body to represent the receiver without the method being defined. This crucial fact holds also

<footnote n="5">⁵ No matter if a cascade of *reg* is invoked and *emp* methods are stacked, because eventually the outermost version of *emp* is executed. An alternative solution would be that *reg* in *alice* overrides itself as *reg* = λs'.λp.⟨s' ← ⊕ id = p⟩: in such an equivalent case only *id* methods would be stacked.</footnote>
for the rightmost sal, where s' refers to an object where that method is already available. Hence *alice'* may be given the following type:

$$
\begin{align*}
\mathit{alice}' & : \mathit{prot}.\langle \mathit{name} \ : \ \mathit{String}, \\
\mathit{reg} & : \ \mathbb{N} \to t \oplus id \oplus sal, \\
\mathit{emp} & : \ \mathbb{N} \to t \oplus id \oplus sal, \tag{1} \\
\mathit{id} & : \ \mathbb{N}, \\
\mathit{sal} & : \ \mathbb{N} \rangle \oplus \mathit{name}, \mathit{reg}, \mathit{emp}
\end{align*}
$$

Calls to *reg* and *emp* methods, therefore, will not raise runtime
errors, and hence we are allowed to invoke such methods to
carry out Alice's reclassification. The price to pay for the
present solution is that the objects playing the roles of students
and workers will contain more methods than needed (all the
methods involved), because no method can be removed. In
detail, when *alice'* registers as student, *id* and *sal* are added
permanently to the interface, i.e. *alice'* $\Leftarrow$ *reg* (45) reduces to:

$$
\begin{align*}
\mathit{alice}_S' &\triangleq \langle \mathit{name}, \mathit{reg}, \mathit{emp} &= \text{as in } \mathit{alice}', \\
\mathit{id} &\triangleq 45, \\
\mathit{sal} &\triangleq 0 \rangle
\end{align*}
$$

From this point onwards, the type system will not detect errors
related to incorrect method calls. Actually, *alice'* is intended to
represent a student, but in practice we will have to distinguish
between students and workers via the runtime answers to the
*id* and *sal* (representing students' and workers' attributes, re-
spectively) method invocations: non-zero values (such as 45,
returned by *id*) are informative of genuine attributes, while zero
values (returned by *sal*) tell us that the corresponding attribute
is not significant. This solution is reminiscent of an approach
to reclassification via wide classes, requiring runtime tests to
diagnose the presence of fields (Serrano 1999).

We proceed by reclassifying $alice'_S$ into worker;
$alice'_S \Leftarrow emp(30K)$ reduces to$^6$:

$$
\begin{align*}
\mathit{alice}'_W &\triangleq \langle \mathit{name}, \mathit{reg} &= \text{as in } \mathit{alice}', \\
\mathit{id} &= 0, \\
\mathit{sal} &= 30K, \\
\mathit{emp} &= \lambda s. \lambda m. \langle \langle s \leftrightarrow id = 0 \rangle \\
&\qquad \leftrightarrow sal = (s \Leftarrow sal) + m \rangle
\end{align*}
$$

The consequence of this call to (the original) *emp* is that *id* and *sal* swap their roles, thus making effective the reclassification, and a new version of *emp* is embedded in the interface. Notice that such a novel *emp* (increasing the salary *sal*) works correctly not only with the usual multi-worker operation, e.g.

$alice'_{W} \Leftarrow emp(14K)$ reduces to:

$$
\begin{align*}
\mathit{alice}'_{W_2} &\triangleq \langle \mathit{name}, \mathit{reg}, \mathit{emp} &= \text{as in } \mathit{alice}'_W, \\
\mathit{id} &= 0, \\
\mathit{sal} &= (\mathit{alice}'_W \Leftarrow \mathit{sal}) + 14K
\end{align*}
$$

but also in the case of a further reclassification of *alice'* into
a student, as in effect setting *de novo* a salary is equivalent to
adding it to the zero value stored by *reg*.

We conclude this subsection with two remarks concerning
the relation of the two versions of *emp* w.r.t. type (1). First,
the fact that the overridden *emp* (i.e. the one belonging to
*alice'* ) extends the receiver via *id* and *sal* but overrides itself is
clearly expressed by its type $\mathbb{N} \to t \oplus id \oplus sal$. Second, the
redundant *id* version contained in the overriding *emp* (appearing
in *alice'* ) is necessary to derive such a type.

**7.2.4. Delegation inheritance, i.e. new objects from scratch**

In Section 7.2.2 we have modeled reclassification by massively using the self-extension mechanism, i.e. via embedding inheritance, but we have also diagnosed a typability problem which we have analyzed in detail. Such an issue, however, is far from being a limitation of the expresive power of $\lambda Obj^\oplus$. Actually, in Section 7.2.3 we have given a first alternative encoding to overcome it. In this section we devise a different solution, which relies on *delegation inheritance*.

We recall the difficulty in removing methods from an object
preserving typability, a feature which would allow for the object
to retrace its reclassification steps. This goal can be naturally
achieved however by constructing a new object from scratch. To
illustrate such an approach, let us consider the following object:

$$
\mathit{andback}' \triangleq \langle \mathit{extend} = \lambda s. \langle \mathit{extend} = \lambda s'. s', \mathit{delete} = \lambda s'. s \rangle \rangle
$$

which is behaviorally equivalent to the problematic *andback*
introduced in Section 7.2.2. In the present case, the *delete*
method is allowed by the type system to return its prototype
object, represented by the variable *s*, because such a method
belongs to a completely *new object*, not to an object which has
extended its prototype (as it was in Section 7.2.2):

$$
\begin{align*}
\mathit{andback}' : \mathit{prot}.\langle \mathit{extend} : \\
\phantom{\mathit{andback}' : \mathit{prot}.\langle} \mathit{pro} \, \mathit{t}'.\langle \mathit{extend} : \mathit{t}', \mathit{delete} : \mathit{t} \rangle \oplus \mathit{extend}, \mathit{delete} \\
\phantom{\mathit{andback}' : \mathit{prot}.\langle} \rangle \oplus \mathit{extend}
\end{align*}
$$

The reader may observe how this typing reflects the given ex-
planation: a new object is generated via the *extend* method
and represented by *t'*; within such an object, the *delete* method
refers back to the prototype object, represented by *t*.

We apply the idea to our working example, via a third repre-

<footnote n="6">⁶ Notice that, to ease readability, we will omit from now onward the overridden methods if the latter become garbage eventually; namely, in this case, the inner versions of *emp*, *id*, *sal*.</footnote>
sentation of Alice:

$$
\begin{align*}
\mathit{alice}'' &\triangleq \langle \mathit{name} = \text{"Alice"}, \\
\mathit{reg} &= \lambda s.\lambda m. \langle \mathit{name} = s \leftarrow \mathit{name}, \\
&\phantom{=} \mathit{id} = m, \\
&\phantom{=} \mathit{emp} = \lambda n. s \leftarrow \mathit{emp}(n) \rangle, \\
\mathit{emp} &= \lambda s.\lambda m. \langle \mathit{name} = s \leftarrow \mathit{name}, \\
&\phantom{=} \mathit{sal} = m, \\
&\phantom{=} \mathit{emp} = \lambda s'.\lambda n. \\
&\phantom{=} \langle s' \leftarrow \mathit{sal} = (s' \leftarrow \mathit{sal}) + n \rangle, \\
&\phantom{=} \mathit{reg} = \lambda p. s \leftarrow \mathit{reg}(p) \rangle
\end{align*}
$$

The novelty of the present solution amounts to the fact that the *reg* and *emp* methods (which, as earlier, play the role of Fickle's constructors *Student* and *Worker*) do not extend the existing *alice''* prototype object, but in fact take advantage of the inheritance mechanism to create new objects. In particular, the core of this encoding is that these new objects are built by relying on *explicit delegation* inheritance.

We illustrate the point by inspecting the *reg* method, that produces a new object equipped with three methods: the second one simply stores the *id* attribute; the crucial methods are *name* and *emp*, actually delegated to the *alice''* object, which is represented by the *s* variable and from which the methods are obtained *at invocation* time. The definition of *alice''*'s third method *emp* is symmetric w.r.t *reg*, apart from the presence, in the new object, of the extra *emp* method, which allows us to model the "multi-worker", again by means of self-extension.

As anticipated at the beginning of the section, *alice''* 's *reg* and *emp* are typable, conversely to their versions in *alice* (see Section 7.2.2), because their methods are not added by self-extension, but belong instead to a different object, created from scratch. In the end, the *alice''* object can be derived the following type:

$$
\begin{align*}
\mathit{alice}'' & : \quad \mathit{prot}.\langle \mathit{name} : \mathit{String}, \\
& \phantom{:} \mathit{reg} : \mathbb{N} \to \sigma, \\
& \phantom{:} \mathit{emp} : \mathbb{N} \to \tau \oplus \mathit{name}, \mathit{reg}, \mathit{emp} \\
\sigma & \triangleq \quad \mathit{prot}'.\langle \mathit{name} : \mathit{String}, \\
& \phantom{:} \mathit{id} : \mathbb{N}, \\
& \phantom{:} \mathit{emp} : \mathbb{N} \to \tau \oplus \mathit{name}, \mathit{id}, \mathit{emp} \\
\tau & \triangleq \quad \mathit{prot}'''.\langle \mathit{name} : \mathit{String}, \\
& \phantom{:} \mathit{sal} : \mathbb{N}, \\
& \phantom{:} \mathit{emp} : \mathbb{N} \to t'', \\
& \phantom{:} \mathit{reg} : \mathbb{N} \to \sigma \oplus \mathit{name}, \mathit{sal}, \mathit{emp}, \mathit{reg}
\end{align*}
$$

By proceeding with our example, Alice's registration,
`alice'' ⇐ reg(45)`, reduces to:

$$
\begin{align*}
\mathit{alice}''_S &\triangleq \langle \mathit{name} = \mathit{alice}'' \Leftarrow \mathit{name}, \\
&\phantom{=} \mathit{id} = 45, \\
&\phantom{=} \mathit{emp} = \lambda n. \mathit{alice}'' \Leftarrow \mathit{emp}(n)
\end{align*}
$$

which is typed by $\sigma$. The third method of this object, *emp*,
which explicitly designates the *emp* method in *alice''*, is crucial
for reclassification, because it permits both *alice''*<sub>S</sub> to retrace its
steps and be reclassified into the "previous" *alice''* and then,
in turn, *alice''* to be reclassified into worker. Therefore, the
message call *alice''*<sub>S</sub> ⇐ *emp* (30K) reduces to:

$$
\begin{align*}
\mathit{alice}''_W &\triangleq \langle \mathit{name} = \mathit{alice}'' \Leftarrow \mathit{name}, \\
&\phantom{=} \mathit{sal} = 30K, \\
&\phantom{=} \mathit{emp} = \lambda s.\lambda m. \langle s \leftarrow \mathit{sal} = (s \Leftarrow \mathit{sal}) + m \rangle, \\
&\phantom{=} \mathit{reg} = \lambda p.\mathit{alice}'' \Leftarrow \mathit{reg}(p) \rangle
\end{align*}
$$

which, in turn, is typed by $\tau$. Finally we add a second job
to Alice, through $alice''_W \Leftarrow emp(14K)$, which reduces to the
following object, typed as well by $\tau$:

$$
\begin{align*}
\mathit{alice}''_{W_2} &\triangleq \langle \mathit{name}, \mathit{emp}, \mathit{reg} = \text{as in } \mathit{alice}''_W, \\
&\phantom{=} \mathit{sal} = (\mathit{alice}''_W \Leftarrow \mathit{sal}) + 14K \rangle
\end{align*}
$$

8. Related work

In the past decades a considerable effort has been put in provid-
ing static type systems for object-oriented calculi and languages
that change at runtime the behavior of objects. In this section,
we discuss first various approaches in the literature by consid-
ering, separately, the two main categories of prototype-based
and class-based languages. Then, we take an alternate view and
discuss the relationship between object extension and object
subsumption.

**8.1. Prototype-based languages**

Vouillon, in 2001 (Vouillon 2001), introduces a prototype-based
calculus with an “object-view” mechanism, which allows an
object, in particular contexts, to change its interface towards the
environment, by hiding some of its methods.

In the mid 00's, the literature started focusing on the script-
ing language JavaScript. JavaScript, which is prototype-based,
has become popular due to its embedding in web pages and
its flexibility. It is interpreted as web pages are loaded and it
supports the runtime modification of objects: addition of new
members to objects, updating, i.e. replacement, of the existing
ones, and even deletion. Clearly, these dynamic features make
static typing difficult, hence JavaScript is dynamically typed.
Actually, errors such as access to non-existing members of ob-
jects cannot be detected until runtime, or they are not detected at
all, which results in errors reported by web browsers. This is the
reason why researchers have begun to pursue the development
of static type disciplines for JavaScript, so as to combine the
flexibility of this programming paradigm with the safety offered
by static type systems.

One of the first approaches is by Anderson and Giannini, who
introduce a formalism for JavaScript, named JS₀, as well as its
operational semantics and type system in (Anderson & Giannini
2005). JS₀ supports JavaScript’s standard features, including
dynamic addition and replacements of members. The type
system, which is proved sound w.r.t. the operational semantics,
permits to detect statically errors such as access to non-existing members of objects. Afterwards, the same authors together with Drossopoulou, in (Anderson et al. 2005), design a type inference algorithm to automatically translate $JS_0$ into an explicitly typed version $JS_0^T$, for which the resulting, annotated programs are proved to be well-typed. One limitation, declared by the authors, is that their formalism does not include the dynamic removal of members from objects.

Thiemann has built in (Thiemann 2005) a type-based analyzer for JavaScript, with the goal of improving the capability of the users to develop and maintain programs. A significant subset of JavaScript is considered, together with its small-step semantics and type system. A type soundness result is proved for this system. The perspective chosen by the author is to model automatic conversion of the values of the language, from one type to another, which happens at runtime and leads to surprising results.

More recently, Zhao (Zhao 2012) has introduced a type inference algorithm to support object extension and update, as well as type polymorphism. The author considers a small fragment of JavaScript and suggests two type disciplines for preventing undefined method calls. JavaScript provides object extension. In order to deal with this feature, Zhao acknowledges and elaborates our ideas in (Di Gianantonio et al. 1998), and shares with the $\lambda Obj^\oplus$ calculus: i) the distinction between pro-types and obj-types, ii) the distinction between “available” and “reserved” methods, and iii) the mechanisms to mark the migration of a method from reserved to available. There are differences between $\lambda Obj^\oplus$ and Zhao’s system, besides the syntax. Most notably in (Zhao 2012) types are defined by means of a set of subtyping constraints and moreover a limited form of strong update, i.e. overriding a method with a different type, is allowed.

Chugh and co-authors (Chugh et al. 2012) propose a statically typed dialect of JavaScript, named Dependent JavaScript, which models quite a rich subset of the former. The features addressed are imperative updates (i.e. updates that change the set of methods of an object, by adding and also subtracting methods), dynamic delegation inheritance, and arrays, which in JavaScript can be homogeneous, when all the elements have the same type, but also heterogeneous, like tuples. Since the syntax makes no distinction between these two kinds of arrays, a correct typing system is challenging. In order to deal with subtyping and inheritance, the authors further elaborate our ideas in (Di Gianantonio et al. 1998) splitting the list of methods into reserved and available parts, as we do in $\lambda Obj^\oplus$.

## 8.2. Class-based languages

The typical setting where the class-based paradigm is investigated is a Java-like environment. In the previous Section 7 we have considered object reclassification, and we have experimented with modeling in $\lambda Obj^\oplus$ the mechanisms implemented in Fickle (Drossopoulou et al. 2002). We complete the survey of related work, by presenting other contributions that fall in the same class-based category.

Monpratarnchai and Tamai (Monpratarnchai & Tamai 2008) introduce an extension of Java, EpsilonJ, featuring role modeling (that is, a set of roles to represent collaboration carried out in

that context, e.g. between an employer and its employees) and object adaptation (that is, a dynamic change of role, to participate in a context by assuming one of its roles). Dynamically acquired methods obtained by assuming roles have to be invoked by means of downcasting, which is a type unsafe operation. Later, Kamina and Tamai (Kamina & Tamai 2010) introduce another extension of Java, NextEJ, to combine the object-based adaptation mechanisms of EpsilonJ and the object-role binding provided by context-oriented languages. The authors model in NextEJ the context activation scope, adopted from the latter languages, and prove that such a mechanism is type sound by using a small calculus which formalizes the core features of NextEJ.

Cohen and Gil's work (Cohen & Gil 2009) on introducing object evolution into statically typed languages, is closely related to reclassification, because evolution is a restriction of reclassification where objects may only gain, but never lose, their capabilities. An evolution operation (which may be of three non-mutually exclusive variants, based respectively on inheritance, mixes, and shakeins) takes at runtime an instance of one class and replaces it with an instance of a selected subclass. We recall that we have deserved Section 7.1 to model the first instance of evolution in $\lambda Obj^\oplus$. Cohen and Gil experiment with an implementation of evolution in Java, based on the idea of using a forward pointer to a new memory address, to support the objects which have evolved starting from the original non-evolved object.

Ressia and co-authors (Ressia et al. 2014) introduce a new form of inheritance called talents. A talent is an object belonging to a standard class, named Talent, which can be acquired (via a suitable acquire primitive) by any object, which is then adapted. The crucial operational characteristics of talents are that they are scoped dynamically and that their composition order is irrelevant. Actually, when two talents with different implementations of the same method are composed a conflict arises, which has to be resolved either through aliasing (the name of the method in a talent is changed) or via exclusion (the method is removed from a talent before composition).

## 8.3. Object extension vs. subsumption

Several calculi proposed in the literature combine object extension with object subsumption. Apart from the individual technicalities of those proposals, they all share the principle of avoiding (type incompatible) object extensions in presence of a (limited) form of object subsumption.

Riecke and Stone in (Riecke & Stone 2002) present a calculus where it is possible to first subsume (forget) an object component, and then re-add it again with a type which may be incompatible with the forgotten one. In order to guarantee the soundness of the type system, method dictionaries are used inside objects with the goal of linking correctly method names and method bodies.

Ghelli in (Ghelli 2002) pursues the same freedom (of forgetting a method and adding it again with a different incompatible type) by introducing a context-dependent behavior of objects called *object role*. Ghelli introduces a role calculus, which is a minimal extension of Abadi-Cardelli's $\zeta$-calculus, where an
object is allowed to change dynamically identity while keeping static type checking. Vouillon’s “view” mechanism (Vouillon 2001), see Section 8.1, can also be interpreted as a a kind of role.

Approaches to subsumption similar to the one presented in this work can be found in (Fisher & Mitchell 1995; Liquori 1997; Bono et al. 1997; Rémy 1998). In (Liquori 1997), an extension of Abadi-Cardelli’s Object Calculus is presented; roughly speaking, we can say that pro-types and obj-types in the present article correspond to “diamond-types” and “saturated-types” in that work. Similar ideas can be found in (Rémy 1998), although the type system presented there permits also a form of self-inflicted extension. However, in that type system, a method m performing a self-inflicted extension needs to return a rigid object whose type is fixed in the declaration of the body of m. As a consequence, the following expressions would not be typable in that system:

$$ \langle\langle p \leftrightarrow new_m = \dots \rangle\rangle \Leftarrow add_{col} \Leftarrow new_m \\ \langle\langle p \Leftarrow add_{col} \langle\leftrightarrow new_m = \dots \rangle \rangle $$

Another type system for the $\lambda Obj$ calculus is presented in (Bono et al. 1997); such a type system uses a refined notion of subtyping that allows to type also binary methods.

## 9. Conclusion and future work

In this paper, we have introduced $\lambda Obj^{\oplus}$, a functional prototype-based calculus whose objects may modify their interface upon receiving a message, by adding new methods or overriding the existing ones, a feature realized via a self-extension mechanism. Moreover, we have equipped $\lambda Obj^{\oplus}$ with a type assignment system and proved a type soundness result, to guarantee that well-typed expressions will not produce message-not-found runtime errors. Finally, we have addressed the emulation problem in $\lambda Obj^{\oplus}$ of type-safe object evolution and object reclassification, which are the benchmarks of the class-based paradigm. We model evolution via embedding inheritance (that is, by using self-extension); on the other hand, we model reclassification by combining delegation inheritance and, again, embedding inheritance but only for overriding.

We devise two departures from the content of the present manuscript as future work. First, we could refine the recursion mechanism of $\lambda Obj^{\oplus}$’s type system, to allow for the removal of methods, previously added by self-extension, from objects (see Section 7.2.2). Second, we could address the possibility of overriding methods with bodies that have unrelated types, a feature which is normally carried out in JavaScript.

## Acknowledgments

The authors would like to express their gratitude for very helpful suggestions, concerning both technical and presentation issues, to Martin Abadi, Mariangiola Dezani-Ciancaglini, and Rekha Redamalla, as well as to the anonymous referees of the Journal of Object Technology, of an earlier version of this paper.

## References

Abadi, M., & Cardelli, L. (1996). A theory of objects. Springer. Retrieved from https://doi.org/10.1007/978-1-4419-8598-9

Anderson, C., & Giannini, P. (2005). Type checking for javascript. Electron. Notes Theor. Comput. Sci., 138(2), 37–58. Retrieved from https://doi.org/10.1016/j.entcs.2005.09.010

Anderson, C., Giannini, P., & Drossopoulou, S. (2005). Towards type inference for javascript. In A. P. Black (Ed.), ECOOP 2005 - object-oriented programming, 19th european conference, glasgow, uk, july 25-29, 2005, proceedings (Vol. 3586, pp. 428–452). Springer. Retrieved from https://doi.org/10.1007/11531142_19

Barendregt, H. P. (1992). Lambda calculi with types.

Beck, K. (1993). Instance specific behavior: how and why. The Smalltalk Report, 2(6), 13–21.

Bierman, G. M., Abadi, M., & Torgersen, M. (2014). Understanding typescript. In R. E. Jones (Ed.), ECOOP 2014 - object-oriented programming - 28th european conference, uppsala, sweden, july 28 - august 1, 2014. proceedings (Vol. 8586, pp. 257–281). Springer. Retrieved from https://doi.org/10.1007/978-3-662-44202-9_11

Bono, V., & Bugliesi, M. (1999). Matching for the lambda calculus of objects. Theor. Comput. Sci., 212(1-2), 101–140. Retrieved from https://doi.org/10.1016/S0304-3975(98)00137-6

Bono, V., Bugliesi, M., Dezani-Ciancaglini, M., & Liquori, L. (1997). Subtyping constraints for incomplete objects (extended abstract). In M. Bidoit & M. Dauchet (Eds.), Tap-soft’97: Theory and practice of software development, 7th international joint conference caap/fase, lille, france, april 14-18, 1997, proceedings (Vol. 1214, pp. 465–477). Springer. Retrieved from https://doi.org/10.1007/BFb0030619

Bono, V., Bugliesi, M., & Liquori, L. (1996). A lambda calculus of incomplete objects. In W. Penczek & A. Szalas (Eds.), Mathematical foundations of computer science 1996, 21st international symposium, mfcs’96, cracow, poland, september 2-6, 1996, proceedings (Vol. 1113, pp. 218–229). Springer. Retrieved from https://doi.org/10.1007/3-540-61550-4_150

Bono, V., & Fisher, K. (1998). An imperative, first-order calculus with object extension. In E. Jul (Ed.), Eloop’98 - object-oriented programming, 12th european conference, brussels, belgium, july 20-24, 1998, proceedings (Vol. 1445, pp. 462–497). Springer. Retrieved from https://doi.org/10.1007/BFb0054104

Bono, V., & Liquori, L. (1994). A subtyping for the fisher-honsell-mitchell lambda calculus of objects. In L. Pacholski & J. Tiuryn (Eds.), Computer science logic, 8th international workshop, CSL ’94, kazimierz, poland, september 25-30, 1994, selected papers (Vol. 933, pp. 16–30). Springer. Retrieved from https://doi.org/10.1007/BFb0022244

Bruce, K. B. (1994). A paradigmatic object-oriented programming language: Design, static typing and semantics. J. Funct. Program., 4(2), 127–206. Retrieved from https://doi.org/10.1017/S0956796800001039

Bruce, K. B., Cardelli, L., Castagna, G., Eifrig, J., Smith, S. F.,
Trifonov, V., ... Pierce, B. C. (1995). On binary methods. *Theory Pract. Object Syst.*, 1(3), 221-242.

Bruce, K. B., Petersen, L., & Fiech, A. (1997). Subtyping is not a good "match" for object-oriented languages. In M. Aksit & S. Matsuoka (Eds.), *Ecoop'97 - object-oriented programming, 11th european conference, jyväskylä, finland, june 9-13, 1997, proceedings* (Vol. 1241, pp. 104–127). Springer. Retrieved from https://doi.org/10.1007/BFb0053376

Cardelli, L. (1995). A language with distributed scope. *Comput. Syst.*, 8(1), 27–59. Retrieved from http://www.usenix.org/publications/compsystems/1995/win Cardelli.pdf

Castagna, G. (1995). Covariance and contravariance: Conflict without a cause. *ACM Trans. Program. Lang. Syst.*, 17(3), 431–447. Retrieved from https://doi.org/10.1145/2030952.203096

Castagna, G. (1996). *Object-oriented programming: A unified foundation*. Boston: Birkhäuser.

Chugh, R., Herman, D., & Jhala, R. (2012). Dependent types for javascript. In G. T. Leavens & M. B. Dwyer (Eds.), *Proceedings of the 27th annual ACM SIGPLAN conference on object-oriented programming, systems, languages, and applications, OOPSLA 2012, part of SPLASH 2012, tucson, az, usa, october 21-25, 2012* (pp. 587–606). ACM. Retrieved from https://doi.org/10.1145/2384616.2384659

Cohen, T., & Gil, J. (2009). Three approaches to object evolution. In B. Stephenson & C. W. Probst (Eds.), *Proceedings of the 7th international conference on principles and practice of programming in java, PPPJ 2009, calgary, alberta, canada, august 27-28, 2009* (pp. 57–66). ACM. Retrieved from https://doi.org/10.1145/1596655.1596665

Damiani, F., Drossopoulou, S., & Giannini, P. (2003). Refined effects for unanticipated object re-classification: Fickle³. In C. Blundo & C. Laneve (Eds.), *Theoretical computer science, 8th italian conference, ICTCS 2003, bertinoro, italy, october 13-15, 2003, proceedings* (Vol. 2841, pp. 97–110). Springer. Retrieved from https://doi.org/10.1007/978-3-540-45208-9_9

Di Gianantonio, P., Honsell, F., & Liquori, L. (1998). A lambda calculus of objects with self-inflicted extension. In B. N. Freeman-Benson & C. Chambers (Eds.), *Proceedings of the 1998 ACM SIGPLAN conference on object-oriented programming systems, languages & applications (OOPSLA '98), vancouver, british columbia, canada, october 18-22, 1998* (pp. 166–178). ACM. Retrieved from https://doi.org/10.1145/286936.286955

Drossopoulou, S., Damiani, F., Dezani-Ciancaglini, M., & Giannini, P. (2001). Fickle : Dynamic object re-classification. In J. L. Knudsen (Ed.), *ECOOP 2001 - object-oriented programming, 15th european conference, budapest, hungary, june 18-22, 2001, proceedings* (Vol. 2072, pp. 130–149). Springer. Retrieved from https://doi.org/10.1007/3-540-45337-7_8

Drossopoulou, S., Damiani, F., Dezani-Ciancaglini, M., & Giannini, P. (2002). More dynamic object reclassification: Fickle. ACM Trans. Program. Lang. Syst., 24(2), 153–191. Retrieved from https://doi.org/10.1145/514952.514955

Fisher, K., Honsell, F., & Mitchell, J. C. (1994). A lambda calculus of objects and method specialization. *Nord. J. Comput.*,

1(1), 3–37.

Fisher, K., & Mitchell, J. C. (1994). Notes on typed object-oriented programming. In M. Hagiya & J. C. Mitchell (Eds.), *Theoretical aspects of computer software, international conference TACS '94, sendai, japan, april 19-22, 1994, proceedings* (Vol. 789, pp. 844–885). Springer. Retrieved from https://doi.org/10.1007/3-540-57887-0_128

Fisher, K., & Mitchell, J. C. (1995). A delegation-based object calculus with subtyping. In H. Reichel (Ed.), *Fundamentals of computation theory, 10th international symposium, FCT '95, dresden, germany, august 22-25, 1995, proceedings* (Vol. 965, pp. 42–61). Springer. Retrieved from https://doi.org/10.1007/3-540-60249-6_40

Fisher, K., & Mitchell, J. C. (1998). On the relationship between classes, objects, and data abstraction. *Theory Pract. Object Syst.*, 4(1), 3–25.

Ghelli, G. (2002). Foundations for extensible objects with roles. *Inf. Comput.*, 175(1), 50–75. Retrieved from https://doi.org/10.1006/inco.2001.2943

Harper, R., Honsell, F., & Plotkin, G. D. (1993). A framework for defining logics. *J. ACM*, 40(1), 143–184. Retrieved from https://doi.org/10.1145/138027.138060

Kamina, T., & Tamai, T. (2010). A smooth combination of role-based language and context activation. In *Proceedings of the ninth workshop on foundation of aspect-oriented languages (foal 2010)*, (pp. 15–24).

Liquori, L. (1997). An extended theory of primitive objects: First order system. In M. Aksit & S. Matsuoka (Eds.), *Ecoop'97 - object-oriented programming, 11th european conference, jyväskylä, finland, june 9-13, 1997, proceedings* (Vol. 1241, pp. 146–169). Springer. Retrieved from https://doi.org/10.1007/BFb0053378

Monpratarnchai, S., & Tamai, T. (2008). The implementation and execution framework of a role model based language, epsilonj. In *Ninth ACIS international conference on software engineering, artificial intelligence, networking and parallel/distributed computing, SNPD 2008, in conjunction with second international workshop on advanced internet technology and applications, august 6-8, 2008, phuket, thailand* (pp. 269–276). IEEE Computer Society. Retrieved from https://doi.org/10.1109/SNPD.2008.103

Rémy, D. (1998). From classes to objects via subtyping. In C. Hankin (Ed.), *Programming languages and systems - esop'98, 7th european symposium on programming, held as part of the european joint conferences on the theory and practice of software, etaps'98, lisbon, portugal, march 28 - april 4, 1998, proceedings* (Vol. 1381, pp. 200–220). Springer. Retrieved from https://doi.org/10.1007/BFb0053572

Ressia, J., Gîrba, T., Nierstrasz, O., Perin, F., & Renggli, L. (2014). Talents: an environment for dynamically composing units of reuse. *Softw. Pract. Exp.*, 44(4), 413–432. Retrieved from https://doi.org/10.1002/spe.2160

Riecke, J. G., & Stone, C. A. (2002). Privacy via subsumption. *Inf. Comput.*, 172(1), 2–28. Retrieved from https://doi.org/10.1006/inco.2000.2925

Serrano, M. (1999). Wide classes. In R. Guerraoui (Ed.), *Ecoop'99 - object-oriented programming, 13th european*
conference, lisbon, portugal, june 14-18, 1999, proceedings (Vol. 1628, pp. 391–415). Springer. Retrieved from https://doi.org/10.1007/3-540-48743-3_18

Taivalsaari, A. (1993). Object-oriented programming with modes. *Journal of Object-Oriented Programming*, 6(3), 25–32.

Takahashi, M. (1995, April). Parallel reductions in lambda calculus. *Inf. Comput.*, 118(1), 120–127. Retrieved from http://dx.doi.org/10.1006/inco.1995.1057

Thiemann, P. (2005). Towards a type system for analyzing javascript programs. In S. Sagiv (Ed.), *Programming languages and systems, 14th european symposium on programming, esop 2005*, held as part of the joint european conferences on theory and practice of software, ETAPS 2005, edinburgh, uk, april 4-8, 2005, *proceedings* (Vol. 3444, pp. 408–422). Springer. Retrieved from https://doi.org/10.1007/978-3-540-31987-0_28

Vouillon, J. (2001). Combining subsumption and binary methods: an object calculus with views. In C. Hankin & D. Schmidt (Eds.), *Conference record of POPL 2001: The 28th ACM SIGPLAN-SIGACT symposium on principles of programming languages*, London, uk, january 17-19, 2001 (pp. 290–303). ACM. Retrieved from https://doi.org/10.1145/360204.360233

Wand, M. (1987). Complete type inference for simple objects. In *Proceedings of the symposium on logic in computer science (LICS '87)*, Ithaca, new York, usa, june 22-25, 1987 (pp. 37–44). IEEE Computer Society. Retrieved from http://www.ccs.neu.edu/home/wand/papers/wand-lics-87.pdf

Zhao, T. (2010). Type inference for scripting languages with implicit extension. In *Acm sigplan international workshop on foundations of object-oriented languages*.

Zhao, T. (2012, October). Polymorphic type inference for scripting languages with object extensions. *SIGPLAN Not.*, 47(2), 37–50. Retrieved from http://doi.acm.org/10.1145/2168696.2047855

## A. Typing rules for $\lambda\mathcal{O}bj^\oplus$

### Well-formed Contexts

$$ \frac{}{\varepsilon \vdash ok} (\text{Cont}-\varepsilon) \quad \frac{\Gamma \vdash \sigma : * \quad x \notin \text{Dom}(\Gamma)}{\Gamma, x:\sigma \vdash ok} (\text{Cont}-x) $$

$$ \frac{\Gamma \vdash \mathit{prot}.R \oplus \bar{m} : * \quad t \notin \mathit{Dom}(\Gamma)}{\Gamma, t \negthinspace \negthinspace \negthinspace \negthinspace \mathit{prot}.R \oplus \bar{m} \vdash ok} (\mathit{Cont}-t) $$

### Well-formed Types

$$ \frac{\Gamma \vdash ok}{\Gamma \vdash t : *} (\text{Type-Const}) \qquad \frac{\Gamma \vdash ok}{\Gamma \vdash \mathit{prot}.\langle \rangle : *} (\text{Type-Pro}_\langle\rangle) $$

$$ \frac{\Gamma, t \negthinspace \negthinspace \negthinspace \negthinspace \mathit{prot}.R \vdash \sigma : * \quad m \notin \bar{R}}{\Gamma \vdash \mathit{prot}.\langle R, m:\sigma \rangle : *} (\text{Type-Pro}) $$

$$ \frac{\Gamma \vdash \tau \negthinspace \negthinspace \negthinspace \negthinspace \mathit{prot}.R \quad \bar{m} \subseteq \bar{R}}{\Gamma \vdash \tau \oplus \bar{m} : *} (\text{Type-Extend}) $$

$$ \frac{\Gamma \vdash \sigma_1 : * \quad \Gamma \vdash \sigma_2 : *}{\Gamma \vdash \sigma_1 \to \sigma_2 : *} (\text{Type-Arrow}) $$

### Matching Rules

$$ \frac{\Gamma \vdash t \oplus \bar{m} : * \quad \bar{n} \subseteq \bar{m}}{\Gamma \vdash t \oplus \bar{m} \negthinspace \negthinspace \negthinspace \negthinspace t \oplus \bar{n}} (\text{Match}-t) $$

$$ \frac{\Gamma_1, t \negthinspace \negthinspace \negthinspace \negthinspace \tau_1, \Gamma_2 \vdash \tau_1 \oplus \bar{m} \negthinspace \negthinspace \negthinspace \negthinspace \tau_2}{\Gamma_1, t \negthinspace \negthinspace \negthinspace \negthinspace \tau_1, \Gamma_2 \vdash t \oplus \bar{m} \negthinspace \negthinspace \negthinspace \negthinspace \tau_2} (\text{Match}-\text{Var}) $$

$$ \Gamma \vdash \mathit{prot}.R_1 \oplus \bar{m} : * \quad R_2 \subseteq R_1 $$

$$ \Gamma \vdash \mathit{prot}.R_2 \oplus \bar{n} : * \quad \bar{n} \subseteq \bar{m} $$

$$ \frac{\Gamma \vdash \mathit{prot}.R_1 \oplus \bar{m} \negthinspace \negthinspace \negthinspace \negthinspace \mathit{prot}.R_2 \oplus \bar{n}}{\Gamma \vdash \mathit{prot}.R_1 \oplus \bar{m} \negthinspace \negthinspace \negthinspace \negthinspace \mathit{prot}.R_2 \oplus \bar{n}} (\text{Match-Pro}) $$

### Type Rules for $\lambda$-terms

$$ \frac{\Gamma \vdash ok}{\Gamma \vdash c : t} (\text{Const}) \qquad \frac{\Gamma_1, x:\sigma, \Gamma_2 \vdash ok}{\Gamma_1, x:\sigma, \Gamma_2 \vdash x : \sigma} (\text{Var}) $$

$$ \frac{\Gamma, x:\sigma_1 \vdash e : \sigma_2}{\Gamma \vdash \lambda x.e : \sigma_1 \to \sigma_2} (\text{Abs}) $$

$$ \frac{\Gamma \vdash e_1 : \sigma_1 \to \sigma_2 \quad \Gamma \vdash e_2 : \sigma_1}{\Gamma \vdash e_1 e_2 : \sigma_2} (\text{Appl}) $$

### Type Rules for Object Terms

$$ \frac{\Gamma \vdash ok}{\Gamma \vdash \langle \rangle : \mathit{prot}.\langle \rangle} (\text{Empty}) $$

$$ \frac{\Gamma \vdash e : \tau \quad \Gamma \vdash \tau \negthinspace \negthinspace \negthinspace \negthinspace \mathit{prot}.\langle R, n:\sigma \rangle \oplus \bar{m}, n}{\Gamma \vdash e \leftarrow n : \sigma[\tau/t]} (\text{Send}) $$

$$ \Gamma \vdash e : \mathit{prot}.R_1 \oplus \bar{m} $$

$$ \frac{\Gamma \vdash \mathit{prot}.\langle R_1, R_2 \rangle \oplus \bar{m} : *} {\Gamma \vdash e : \mathit{prot}.\langle R_1, R_2 \rangle \oplus \bar{m}} (\text{Pre-Extend}) $$

$$ \Gamma \vdash e_1 : \tau \quad \Gamma \vdash \tau \negthinspace \negthinspace \negthinspace \negthinspace \mathit{prot}.\langle R, n:\sigma \rangle \oplus \bar{m} $$

$$ \frac{\Gamma, t \negthinspace \negthinspace \negthinspace \negthinspace \mathit{prot}.\langle R, n:\sigma \rangle \oplus \bar{m}, n \vdash e_2 : t \to \sigma}{\Gamma \vdash \langle e_1 \leftrightarrow n = e_2 \rangle : \tau \oplus n} (\text{Extend}) $$

$$ \Gamma \vdash e_1 : \tau \quad \Gamma \vdash \tau \negthinspace \negthinspace \negthinspace \negthinspace \mathit{prot}.\langle R, n:\sigma \rangle \oplus \bar{m}, n $$

$$ \frac{\Gamma, t \negthinspace \negthinspace \negthinspace \negthinspace \mathit{prot}.\langle R, n:\sigma \rangle \oplus \bar{m}, n \vdash e_2 : t \to \sigma}{\Gamma \vdash \langle e_1 \leftrightarrow n = e_2 \rangle : \tau} (\text{Override}) $$

$$ \Gamma \vdash e_1 : \tau \quad \Gamma \vdash \tau \negthinspace \negthinspace \negthinspace \negthinspace \mathit{prot}.\langle R, n:\sigma \rangle \oplus \bar{m}, n $$

$$ \frac{\Gamma, t \negthinspace \negthinspace \negthinspace \negthinspace \mathit{prot}.\langle R, n:\sigma \rangle \oplus \bar{m}, n \vdash e_2 : t \to t \oplus n}{\Gamma \vdash \mathit{Sel}(e_1, n, e_2) : \sigma[\tau \oplus n/t]} (\text{Select}) $$

## B. Extra rules for Subsumption: $\lambda\mathcal{O}bj_S^\oplus$

### Extra Well-formed Contexts

$$ \frac{\Gamma \vdash \mathit{obj}.R \oplus \bar{m} : * \quad t \notin \mathit{Dom}(\Gamma)}{\Gamma, t \negthinspace \negthinspace \negthinspace \negthinspace \mathit{obj}.R \oplus \bar{m} \vdash ok} (\mathit{Cont}-\mathit{Obj}) $$

### Extra Well-formed Types

$$ \frac{\Gamma \vdash \mathit{prot}.R \oplus \bar{m} : *}{\Gamma \vdash \mathit{obj}.R \oplus \bar{m} : *} (\text{Type-Obj}) $$

$$ \frac{\Gamma \vdash \tau \negthinspace \negthinspace \negthinspace \negthinspace \mathit{obj}.R \quad \bar{m} \subseteq \bar{R}}{\Gamma \vdash \tau \oplus \bar{m} : *} (\text{Type-Extend}-\mathit{Obj}) $$
## Rules for Rigid Types

$$ \frac{\Gamma \vdash ok}{\Gamma \vdash t : *_{rgd}} \quad (\text{Type-Const-Rgd}) $$

$$ \frac{\Gamma \vdash \sigma_1 : * \quad \Gamma \vdash \sigma_2 : *_{rgd}}{\Gamma \vdash \sigma_1 \to \sigma_2 : *_{rgd}} \quad (\text{Type-Arrow-Rgd}) $$

$$ \Gamma_1, t \nvdash \text{objt.R} \oplus \bar{m}, \Gamma_2 \vdash t \oplus \bar{n} : * \\ t \text{ covariant in } R $$

$$ \frac{\Gamma_1, t \nvdash \text{objt.R} \oplus \bar{m}, \Gamma_2 \vdash t \oplus \bar{n} : *_{rgd}}{\Gamma_1, t \nvdash \text{objt.R} \oplus \bar{m}, \Gamma_2 \vdash t \oplus \bar{n} : *_{rgd}} \quad (\text{Type-Var-Obj}) $$

$$ \Gamma \vdash \text{objt.} \langle \bar{m}_k : \bar{\sigma}_k \rangle \oplus \bar{n} : * $$

$$ \forall i \leq k. \Gamma \vdash \sigma_i : *_{rgd} \wedge t \text{ covariant in } \sigma_i $$

$$ \frac{\Gamma \vdash \text{objt.} \langle \bar{m}_k : \bar{\sigma}_k \rangle \oplus \bar{n} : *_{rgd}}{\Gamma \vdash \text{objt.R} \oplus \bar{m}_k \nvdash \text{objt.R}_2 \oplus \bar{n}} \quad (\text{Type-Obj-Rdg}) $$

## Extra Matching Rules

$$ \frac{\Gamma \vdash \sigma'_1 \nvdash \sigma_1 \quad \Gamma \vdash \sigma_2 \nvdash \sigma'_2 \quad \Gamma \vdash \sigma_1 : *_{rgd}}{\Gamma \vdash \sigma_1 \to \sigma_2 \nvdash \sigma'_1 \to \sigma'_2} \quad (\text{Match-Arrow}) $$

$$ \Gamma \vdash \text{prot.R}_1 \oplus \bar{m} : * \quad R_2 \subseteq R_1 $$

$$ \Gamma \vdash \text{prot.R}_2 \oplus \bar{n} : * \quad \bar{n} \subseteq \bar{m} $$

$$ \frac{\Gamma \vdash \text{prot.R}_1 \oplus \bar{m} \nvdash \text{objt.R}_2 \oplus \bar{n}}{\Gamma \vdash \text{prot.R}_1 \oplus \bar{m} \nvdash \text{objt.R}_2 \oplus \bar{n}} \quad (\text{Promote}) $$

$$ \Gamma \vdash \text{prot.R}_1 \oplus \bar{m} : * \quad R_2 \subseteq R_1 $$

$$ \Gamma \vdash \text{prot.R}_2 \oplus \bar{n} : * \quad \bar{n} \subseteq \bar{m} $$

$$ \frac{\Gamma \vdash \text{objt.R}_1 \oplus \bar{m} \nvdash \text{objt.R}_2 \oplus \bar{n}}{\Gamma \vdash \text{objt.R}_1 \oplus \bar{m} \nvdash \text{objt.R}_2 \oplus \bar{n}} \quad (\text{Match-Obj}) $$

## Extra Type Rules for Terms

$$ \Gamma \vdash e_1 : \tau \quad \Gamma \vdash \tau \nvdash \text{objt.} \langle R, n : \sigma \rangle \oplus \bar{m} $$

$$ \Gamma, t \nvdash \text{objt.} \langle R, n : \sigma \rangle \oplus \bar{m}, n \vdash e_2 : t \to \sigma $$

$$ \frac{\Gamma \vdash \langle e_1 \leftrightarrow n = e_2 \rangle : \tau \oplus n}{\Gamma \vdash \langle e_1 \leftrightarrow n = e_2 \rangle : \tau} \quad (\text{Extend-Obj}) $$

$$ \Gamma \vdash e_1 : \tau \quad \Gamma \vdash \tau \nvdash \text{objt.} \langle R, n : \sigma \rangle \oplus \bar{m}, n $$

$$ \Gamma, t \nvdash \text{objt.} \langle R, n : \sigma \rangle \oplus \bar{m}, n \vdash e_2 : t \to \sigma $$

$$ \frac{\Gamma \vdash \langle e_1 \leftrightarrow n = e_2 \rangle : \tau}{\Gamma \vdash \langle e_1 \leftrightarrow n = e_2 \rangle : \tau} \quad (\text{Override-Obj}) $$

$$ \frac{\Gamma \vdash e : \tau \quad \Gamma \vdash \tau \nvdash \text{objt.} \langle R, n : \sigma \rangle \oplus \bar{m}, n}{\Gamma \vdash e \leftarrow n : \sigma[\tau/t]} \quad (\text{Send-Obj}) $$

$$ \Gamma \vdash e_1 : \tau \quad \Gamma \vdash \tau \nvdash \text{objt.} \langle R, n : \sigma \rangle \oplus \bar{m}, n $$

$$ \Gamma, t \nvdash \text{objt.} \langle R, n : \sigma \rangle \oplus \bar{m}, n \vdash e_2 : t \to t \oplus n $$

$$ \frac{\Gamma \vdash \text{Sel}(e_1, n, e_2) : \sigma[\tau \oplus n/t]}{\Gamma \vdash \text{Sel}(e_1, n, e_2) : \sigma[\tau \oplus n/t]} \quad (\text{Select-Obj}) $$

$$ \frac{\Gamma \vdash e : \sigma_1 \quad \Gamma \vdash \sigma_1 \nvdash \sigma_2 \quad \Gamma \vdash \sigma_2 : *_{rgd}}{\Gamma \vdash e : \sigma_2} \quad (\text{Subsume}) $$

# C. Soundness of the Type System $\lambda\mathcal{O}bj^{\oplus}$

## Lemma C.1 (Sub-derivation)

(i) If $\Delta$ is a derivation of $\Gamma_1, \Gamma_2 \vdash \mathcal{A}$, then there exists a sub-derivation $\Delta' \subseteq \Delta$ of $\Gamma_1 \vdash \text{ok}$.

(ii) If $\Delta$ is a derivation of $\Gamma_1, x:\sigma, \Gamma_2 \vdash \mathcal{A}$, then there exists a sub-derivation $\Delta' \subseteq \Delta$ of $\Gamma_1 \vdash \sigma : *$.

(iii) If $\Delta$ is a derivation of $\Gamma_1, t \nvdash \tau, \Gamma_2 \vdash \mathcal{A}$, then there exists a sub-derivation $\Delta' \subseteq \Delta$ of $\Gamma_1 \vdash \tau : *$.

The three points are proved, separately, by structural induction on the derivation $\Delta$.

(i) The only cases where the induction hypothesis cannot be applied are the cases where the last rule in $\Delta$ is a context rule (that is, the only kind of rule that can increase the context) and $\Gamma_2$ is empty. In these cases the thesis coincides with the hypothesis. In all the other cases the thesis follows immediately by an application of the induction hypothesis.

(ii) As in point (i), either we conclude immediately by induction hypothesis or it is the case that $\Gamma_2$ is empty and the last rule in $\Delta$ is a context rule. In this latter case the last rule in $\Delta$ is necessarily a $(\text{Cont}-x)$ rule deriving $\Gamma_1, x:\sigma \vdash \text{ok}$, and the first premise of this rule coincides with the thesis.

(iii) The proof works similarly to point (ii). □

## Lemma C.2 (Weakening)

(i) If $\Gamma_1, \Gamma_2 \vdash \mathcal{A}$ and $\Gamma_1, \mathcal{C}, \Gamma_2 \vdash \text{ok}$, then $\Gamma_1, \mathcal{C}, \Gamma_2 \vdash \mathcal{A}$.

(ii) If $\Gamma_1 \vdash \mathcal{A}$ and $\Gamma_1, \Gamma_2 \vdash \text{ok}$, then $\Gamma_1, \Gamma_2 \vdash \mathcal{A}$.

(i) By structural induction on the derivation $\Delta$ of $\Gamma_1, \Gamma_2 \vdash \mathcal{A}$. If the last rule in $\Delta$ has the context in the conclusion identical to the context in the premise(s), then it is possible to apply the induction hypothesis, thus deriving almost immediately the goal. In the other cases, if the last rule in $\Delta$ is a $(\text{Cont}-x)$ or $(\text{Cont}-t)$ rule, then the proof is trivial, since the second hypothesis coincides with the thesis. The remaining cases concern the $(\text{Type-Pro})$, $(\text{Abs})$, $(\text{Extend})$ and $(\text{Override})$ rules, which require a more careful treatment. We give the details here only of the proof for $(\text{Type-Pro})$, since the other rules are handled in a similar way.

In the $(\text{Type-Pro})$ case, the hypothesis $\Gamma_1, \Gamma_2 \vdash \text{prot}.\langle R, m : \sigma \rangle : *$ follows from:

$$ \Gamma_1, \Gamma_2, t \nvdash \text{prot.R} \vdash \sigma : * \quad (2) $$

Let us briefly remark that if the statement $\mathcal{C}$ of the second hypothesis is equal to $t \nvdash \tau$, for some type $\tau$, then it is convenient to $\alpha$-convert the type $\text{prot}.\langle R, m : \sigma \rangle$ to avoid clash of variables. In any case, by Lemma C.1.(iii) (Sub-derivation), there exists a sub-derivation of $\Delta$ deriving $\Gamma_1, \Gamma_2 \vdash \text{prot.R} : *$, from which, by induction hypothesis, $\Gamma_1, \mathcal{C}, \Gamma_2 \vdash \text{prot.R} : *$ and in turn, via the $(\text{Cont}-t)$ rule, $\Gamma_1, \mathcal{C}, \Gamma_2, t \nvdash \text{prot.R} \vdash \text{ok}$. By using (2) and the induction hypothesis, we deduce $\Gamma_1, \mathcal{C}, \Gamma_2, t \nvdash \text{prot.R} \vdash \sigma : *$. Finally we have the thesis via the $(\text{Type-Pro})$ rule.

(ii) By induction on the length of $\Gamma_2$; the proof uses the previous point (i) and Lemma C.1.(i) (Sub-derivation). □

## Lemma C.3 (Well-formed object-types)

(i) $\Gamma \vdash \text{prot.R} \oplus \bar{m} : *$ if and only if $\Gamma \vdash \text{prot.R} : *$ and $\bar{m} \subseteq \bar{R}$.

(ii) $\Gamma \vdash t \oplus \bar{m} : *$ if and only if $\Gamma$ contains $t \nvdash \text{prot.R} \oplus \bar{n}$, with $\bar{m} \subseteq \bar{R}$.
Point (i) is immediately proved by inspection on the rules for well-formed types and matching. Point (ii) is proved by inspection on the rules for well-formed contexts, well-formed types and matching. □

In the following proofs often we will not refer explicitly to the previous lemmas, considering their application immediate.

**Proposition C.4 (Matching is well-formed)**

If $\Gamma \vdash \tau_1 \dashv \tau_2$, then $\Gamma \vdash \tau_1 : *$ and $\Gamma \vdash \tau_2 : *$.

By structural induction on the derivation $\Delta$ of $\Gamma \vdash \tau_1 \dashv \tau_2$. The premises of the (Match-Pro) rule coincide with the thesis. If the last rule in $\Delta$ is (Match-t), we conclude by using its premises and Lemma C.3.(ii) (Well-formed object-types). If the last rule in $\Delta$ is (Match-Var), then the judgment $\Gamma_1, t \dashv \rho, \Gamma_2 \vdash t \oplus \bar{m} \dashv \tau_2$ is derived from $\Gamma_1, t \dashv \rho, \Gamma_2 \vdash \rho \oplus \bar{m} \dashv \tau_2$. By induction hypothesis $\tau_2$ is well-formed and $\Gamma_1, t \dashv \rho, \Gamma_2 \vdash \rho \oplus \bar{m} : *$. By inspecting the (Cont-t) rule, $\rho$ must be in the form $\text{prot}.R \oplus \bar{n}$, and by Lemma C.3.(i) it holds $\bar{m} \subseteq \bar{R}$. We can now conclude $\Gamma_1, t \dashv \rho, \Gamma_2 \vdash t \oplus \bar{m} : *$ via Lemma C.3.(ii). □

**Lemma C.5 (Matching)**

(i) $\Gamma \vdash \text{prot}.R_1 \oplus \bar{m} \dashv \tau_2$ if and only if $\Gamma \vdash \text{prot}.R_1 \oplus \bar{m} : *$ and $\Gamma \vdash \tau_2 : *$ and $\tau_2 \equiv \text{prot}.R_2 \oplus \bar{n}$, with $R_2 \subseteq R_1$ and $\bar{n} \subseteq \bar{m}$.

(ii) $\Gamma \vdash \tau_1 \dashv t \oplus \bar{n}$ if and only if $\Gamma \vdash \tau_1 : *$ and $\tau_1 \equiv t \oplus \bar{m}$, with $\bar{n} \subseteq \bar{m}$.

(iii) $\Gamma \vdash t \oplus \bar{m} \dashv \text{prot}.R_2 \oplus \bar{n}$ if and only if $\Gamma$ contains $t \dashv \text{prot}.R_1 \oplus \bar{p}$, with $R_2 \subseteq R_1$ and $\bar{n} \subseteq \bar{m} \cup \bar{p}$.

(iv) (Reflexivity) If $\Gamma \vdash \rho : *$ then $\Gamma \vdash \rho \dashv \rho$.

(v) (Transitivity) If $\Gamma \vdash \tau_1 \dashv \rho$ and $\Gamma \vdash \rho \dashv \tau_2$, then $\Gamma \vdash \tau_1 \dashv \tau_2$.

(vi) (Uniqueness) If $\Gamma \vdash \tau_1 \dashv \text{prot}.\langle R_1, m:\sigma_1 \rangle$ and $\Gamma \vdash \tau_1 \dashv \text{prot}.\langle R_2, m:\sigma_2 \rangle$, then $\sigma_1 \equiv \sigma_2$.

(vii) If $\Gamma \vdash \tau_1 \dashv \tau_2$ and $\Gamma \vdash \tau_2 \oplus m : *$, then $\Gamma \vdash \tau_1 \oplus m \dashv \tau_2 \oplus \bar{m}$.

(viii) If $\Gamma \vdash \tau_1 \oplus m \dashv \text{prot}.R \oplus \bar{n}$, then $\Gamma \vdash \tau_1 \dashv \text{prot}.R \oplus \bar{n} - \bar{m}$.

(ix) If $\Gamma \vdash \rho \oplus m : *$, then $\Gamma \vdash \rho \oplus m \dashv \rho$.

(i) (ii) (iii) The thesis is immediate by inspection on the matching rules.

(iv) By cases on the form of the object-type $\rho$. The thesis can be derived immediately using either the (Match-Pro) rule or the (Match-t) one.

(v) By cases on the forms of $\tau_1, \tau_2, \rho$, using the points (i), (ii), (iii) above. If $\tau_1 \equiv \text{prot}.R \oplus \bar{m}$, we conclude by a triple application of point (i). If $\tau_2 \equiv t \oplus \bar{n}$, we conclude by three applications of point (ii). If $\tau_1 \equiv t \oplus \bar{m}$ and $\tau_2 \equiv \text{prot}.R \oplus \bar{n}$, we conclude by reasoning on the form of $\rho$, using all the points (i), (ii), (iii).

(vi) By cases on the form of $\rho$, using either point (i) or point (iii).

(vii) By cases on the form of $\tau_1$. If $\tau_1 \equiv \text{prot}.R \oplus \bar{m}$, we have the thesis by point (i) and Lemma C.3.(i) (Well-formed

object-types). If $\tau_1 \equiv t \oplus \bar{m}$, we reason by cases on the form of $\tau_2$: if $\tau_2 \equiv \text{prot}.R \oplus \bar{n}$, then we have the thesis by point (iii) and the validity of the thesis for pro-types; if $\tau_2 \equiv t \oplus \bar{n}$, then we have the thesis by point (ii).

(viii) By cases on the form of $\tau_1$, using either point (i) or point (iii).

(ix) By cases on the form of $\rho$, using either point (i) or point (ii) and Lemma C.3.(ii) (Well-formed object-types). □

**Lemma C.6 (Match weakening and Method types)**

(i) If $\Gamma_1, t \dashv \rho, \Gamma_2 \vdash A$ and $\Gamma_1 \vdash \tau \dashv \rho$, with $\tau$ a pro-type, then $\Gamma_1, t \dashv \tau, \Gamma_2 \vdash A$.

(ii) If $\Gamma \vdash \text{prot}.\langle R, n:\sigma \rangle \oplus \bar{m} : *$, then $\Gamma, t \dashv \text{prot}.\langle R, n:\sigma \rangle \oplus \bar{m} \vdash \sigma : *$.

(i) By structural induction on the derivation $\Delta$ of $\Gamma_1, t \dashv \rho, \Gamma_2 \vdash A$.

The only case where the induction hypothesis cannot be applied is when $\Gamma_2$ is empty and the last rule in $\Delta$ is a rule increasing the length of the context, i.e. the (Cont-t) rule. In fact, $\Gamma, t \dashv \rho \vdash \text{ok}$ is derived from $t \notin \text{Dom}(\Gamma)$; on the other hand, from the second hypothesis and Proposition C.4 (Matching is well-formed) we have also that $\Gamma_1 \vdash \tau : *$, hence we may derive the thesis using the same (Cont-t) rule.

For all the other cases but one the application of the induction hypothesis and the derivation of the thesis is immediate, since the last rule in $\Delta$ does not use the hypothesis $t \dashv \rho$ in the context. The only rule that can use this hypothesis is (Match-Var): in such a case $\Gamma_1, t \dashv \rho, \Gamma_2 \vdash t \oplus \bar{m} \dashv \nu$ is derived from the premise $\Gamma_1, t \dashv \rho, \Gamma_2 \vdash \rho \oplus \bar{m} \dashv \nu$. By induction hypothesis, we have $\Gamma_1, t \dashv \tau, \Gamma_2 \vdash \rho \oplus \bar{m} \dashv \nu$. Moreover, from $\Gamma_1 \vdash \tau \dashv \rho$ and the Weakening Lemma C.2, we derive $\Gamma_1, t \dashv \tau, \Gamma_2 \vdash \tau \dashv \rho$, from which, by Lemma C.5.(vii) (Matching), $\Gamma_1, t \dashv \tau, \Gamma_2 \vdash \tau \oplus \bar{m} \dashv \rho \oplus \bar{m}$. Finally, by transitivity of matching (Lemma C.5.(v)), we have $\Gamma_1, t \dashv \tau, \Gamma_2 \vdash \tau \oplus \bar{m} \dashv \nu$, and by an application of the (Match-Var) rule we obtain the thesis.

(ii) First observe that there exists $R_1 \subseteq R$ such that $\Gamma, t \dashv \text{prot}.R_1 \vdash \sigma : *$.

In fact, by Lemma C.3.(i) (Well-formed object-types), we have $\Gamma \vdash \text{prot}.\langle R, n:\sigma \rangle : *$, that can only be derived by an application of the (Type-Pro) rule; therefore, we have either our goal or $\Gamma, t \dashv \text{prot}.\langle R_2, n:\sigma \rangle \vdash \alpha : *$ for a suitable $R_2$ such that $R \equiv \langle R_2, p:\alpha \rangle$. From Lemma C.1.(iii) (Sub-derivation) follows that $\Gamma \vdash \text{prot}.\langle R_2, n:\sigma \rangle : *$, hence we may conclude the existence of $R_1$.

Now, from $\Gamma, t \dashv \text{prot}.R_1 \vdash \sigma : *$, by using Lemma C.1.(iii), the (Match-Pro) rule and point (i), we have the thesis. □

**Proposition C.7 (Substitution)**

(i) If $\Gamma_1, x:\sigma, \Gamma_2 \vdash A$ and $\Gamma_1 \vdash e : \sigma$, then $\Gamma_1, \Gamma_2 \vdash A[e/x]$.

(ii) If $\Gamma_1, t \dashv \tau, \Gamma_2, \Gamma_3 \vdash A$ and $\Gamma_1, t \dashv \tau, \Gamma_2 \vdash \rho \dashv \tau$, then $\Gamma_1, t \dashv \tau, \Gamma_2, \Gamma_3[\rho/t] \vdash A[\rho/t]$.

(iii) If $\Gamma_1, t \dashv \tau, \Gamma_2 \vdash A$ and $\Gamma_1 \vdash \rho \dashv \tau$, then $\Gamma_1, \Gamma_2[\rho/t] \vdash A[\rho/t]$.
(i) By induction on the derivation $\Delta$ of $\Gamma_1, x:\sigma, \Gamma_2 \vdash A$. The only situation where the induction hypothesis cannot be immediately applied is when the last rule in $\Delta$ is $(\mathit{Cont}-x)$. In such a case $\Gamma_1, x:\sigma \vdash ok$ is derived from $\Gamma_1 \vdash \sigma : *$, from which, by Lemma C.1.(i) (Sub-derivation), we have the thesis.

All the remaining rules can be easily dealt with by applying the induction hypothesis, apart from the case where the last rule in $\Delta$ is $(\mathit{Var})$ and the variable $x$ coincides with the one dealt with by the rule. In this case the conclusion $\Gamma_1, x:\sigma, \Gamma_2 \vdash x : \sigma$ derives from the premise $\Gamma_1, x:\sigma, \Gamma_2 \vdash ok$ and so $\Gamma_1, \Gamma_2 \vdash ok$ by induction. By the second hypothesis $\Gamma_1 \vdash e : \sigma$ and Lemma C.2 (Weakening), we deduce $\Gamma_1, \Gamma_2 \vdash e : \sigma$.

(ii) By induction on the derivation $\Delta$ of $\Gamma_1, t \not\vdash \tau, \Gamma_2, \Gamma_3 \vdash A$. As in the previous point, the only case where the induction hypothesis cannot be applied is when the last rule in $\Delta$ is a context rule; in this case the hypothesis coincides with the thesis.

As far as the remaining rules, the only non-trivial case is when the last rule in $\Delta$ is $(\mathit{Match}-\mathit{Var})$ (the only rule that can use the judgment $t \not\vdash \tau$ of the context) and the type variable $t$ coincides with the rule. In this case the conclusion $\Gamma_1, t \not\vdash \tau, \Gamma_2, \Gamma_3 \vdash t \oplus \bar{m} \not\vdash \tau_2$ derives from the premise $\Gamma_1, t \not\vdash \tau, \Gamma_2, \Gamma_3 \vdash \tau \oplus \bar{m} \not\vdash \tau_2$; then, by induction hypothesis, $\Gamma_1, t \not\vdash \tau, \Gamma_2, \Gamma_3[\rho/t] \vdash (\tau \oplus \bar{m} \not\vdash \tau_2)[\rho/t]$. By the side condition on $(\mathit{Cont}-t)$, $t$ cannot be free in $\tau$ and, by Lemma C.5 (i) (Matching), neither in $\tau_2$; hence, the above judgment can be written as $\Gamma_1, t \not\vdash \tau, \Gamma_2, \Gamma_3[\rho/t] \vdash \tau \oplus \bar{m} \not\vdash \tau_2$. On the other hand, from the second hypothesis $\Gamma_1, t \not\vdash \tau, \Gamma_2 \vdash \rho \not\vdash \tau$ we can derive $\Gamma_1, t \not\vdash \tau, \Gamma_2, \Gamma_3[\rho/t] \vdash \rho \oplus \bar{m} \not\vdash \tau \oplus \bar{m}$ by Lemma C.2.(ii) (Weakening) and Lemma C.5.(vii), and from the transitivity of matching (Lemma C.5.(v)) we can conclude $\Gamma_1, t \not\vdash \tau, \Gamma_2, \Gamma_3[\rho/t] \vdash \rho \oplus \bar{m} \not\vdash \tau_2$.

(iii) By the previous point we can derive $\Gamma_1, t \not\vdash \tau, \Gamma_2[\rho/t] \vdash A[\rho/t]$. Now, via an immediate induction, one can prove that if $\Gamma_1, t \not\vdash \tau, \Gamma_2 \vdash A$ and $t$ is not free in $\Gamma_2$ nor in $A$, then $\Gamma_1, \Gamma_2 \vdash A$. The thesis follows immediately from such a property. $\square$

**Proposition C.8 (Types of expressions are well-formed)**

If $\Gamma \vdash e : \beta$, then $\Gamma \vdash \beta : *$.

By structural induction on the derivation $\Delta$ of $\Gamma \vdash e : \beta$. In this proof we need to consider explicitly all the possible cases for the last rule in $\Delta$; each case is quite simple but needs specific arguments.

(Rules for $\lambda$-terms) If the last rule in $\Delta$ is $(\mathit{Const})$, we derive the thesis via $(\mathit{Type}-\mathit{Const})$. To address the $(\mathit{Var})$ rule we use Lemma C.1.(ii) (Sub-derivation) and Lemma C.2.(i) (Weakening). For the $(\mathit{Abs})$ rule one applies the induction hypothesis, Lemma C.1.(ii), Proposition C.7.(i) (Substitution), and the $(\mathit{Type}-\mathit{Arrow})$ rule. About $(\mathit{Appl})$, the induction hypothesis allows us to derive $\Gamma \vdash \alpha \to \beta : *$; this judgment can only be derived through the $(\mathit{Type}-\mathit{Arrow})$ rule, whose second premise is precisely the thesis.

(Rules for object terms) The thesis is trivial for the $(\mathit{Empty})$, $(\mathit{Pre}-\mathit{Extend})$ and $(\mathit{Override})$ rules. In the $(\mathit{Extend})$ case, $\Gamma \vdash (e_1 \leftrightarrow n = e_2) : \tau \oplus n$ is derived from $\Gamma \vdash$

$\tau \not\vdash \mathit{prot} \langle R, n:\sigma \rangle \oplus \bar{m}$; by Proposition C.4 (Matching is well-formed) and Lemma C.3.(i) (Well-formed object-types), we have $\Gamma \vdash \mathit{prot} \langle R, n:\sigma \rangle \oplus \bar{m}, n : *$; by Lemma C.5.(vii) (Matching), $\Gamma \vdash \tau \oplus n \not\vdash \mathit{prot} \langle R, n:\sigma \rangle \oplus \bar{m}, n$, and so we conclude by Proposition C.4.

The two remaining cases are more complex.

(Send) We have that $\Gamma \vdash e \Leftarrow n : \sigma[\tau/t]$ is derived from $\Gamma \vdash \tau \not\vdash \mathit{prot} \langle R, n:\sigma \rangle \oplus \bar{m}, n$, from which, by Proposition C.4, we derive $\Gamma \vdash \mathit{prot} \langle R, n:\sigma \rangle \oplus \bar{m}, n : *$ and, in turn, $\Gamma, t \not\vdash \mathit{prot} \langle R, n:\sigma \rangle \oplus \bar{m}, n \vdash \sigma : *$ by Lemma C.6.(ii) (Method types); finally, by Proposition C.7.(iii) (Substitution), we can conclude that $\Gamma \vdash \sigma[\tau/t] : *$.

(Select) We have that $\Gamma \vdash \mathit{Sel}(e_1, n, e_2) : \sigma[(\tau \oplus \bar{n})/t]$ is derived from both $\Gamma, t \not\vdash \mathit{prot} \langle R, n:\sigma \rangle \oplus \bar{m}, n \vdash e_2 : t \to (t \oplus \bar{n})$ and $\Gamma \vdash \tau \not\vdash \mathit{prot} \langle R, n:\sigma \rangle \oplus \bar{m}, n$. By induction hypothesis, $\Gamma, t \not\vdash \mathit{prot} \langle R, n:\sigma \rangle \oplus \bar{m}, n \vdash t \to (t \oplus \bar{n}) : *$ and, by Proposition C.7.(iii), $\Gamma \vdash \tau \to (\tau \oplus \bar{n}) : *$; then, since this latter judgment can only be obtained via the $(\mathit{Type}-\mathit{Arrow})$ rule, we deduce $\Gamma \vdash \tau \oplus \bar{n} : *$. Further, we have $\Gamma \vdash \tau \oplus \bar{n} \not\vdash \mathit{prot} \langle R, n:\sigma \rangle \oplus \bar{m}, n$ by case analysis and Lemma C.5.(i)-(iii), from which the thesis follows by Lemma C.6.(ii) and Proposition C.7.(iii). $\square$

**Theorem C.9 (Subject Reduction, $\lambda\mathcal{O}bj^\oplus$)**

If $\Gamma \vdash e : \beta$ and $e \to e'$, then $\Gamma \vdash e' : \beta$.

We prove that the type is preserved by each of the four reduction rules (Beta), (Selection), (Success), and (Next). Preservation under contextual closure is then proved by an application of Proposition C.7 (Substitution).

(Beta) The derivation $\Delta$ of $\Gamma \vdash (\lambda x.e_1)e_2 : \beta$ needs to terminate with a rule $(\mathit{Appl})$, deriving $\Gamma \vdash (\lambda x.e_1)e_2 : \alpha$, possibly followed by some applications of $(\mathit{Pre}-\mathit{Extend})$. Let the premises of $(\mathit{Appl})$ be $\Gamma \vdash (\lambda x.e_1) : \sigma \to \alpha$ and $\Gamma \vdash e_2 : \sigma$ for a suitable $\sigma$; in turn, the first judgment has to be derived from $\Gamma, x:\sigma \vdash e_1 : \alpha$ via the $(\mathit{Abs})$ rule. By Proposition C.7.(i) (Substitution), we conclude $\Gamma \vdash (e_1 : \alpha)[e_2/x] \equiv e_1[e_2/x] : \alpha$; then, possibly repeatedly applying rule $(\mathit{Pre}-\mathit{Extend})$ in $\Delta$, we have the thesis.

(Selection) The derivation $\Delta$ of $\Gamma \vdash e \Leftarrow n : \beta$ has to terminate with a $(\mathit{Send})$ rule, deriving $\Gamma \vdash e \Leftarrow n : \sigma[\tau/t]$, possibly followed by applications of $(\mathit{Pre}-\mathit{Extend})$. The premises of $(\mathit{Send})$ are $\Gamma \vdash e : \tau$ and $\Gamma \vdash \tau \not\vdash \mathit{prot} \langle R, n:\sigma \rangle \oplus \bar{m}, n$. From this latter judgment, by Lemma C.4 (Matching is well-formed) and the rules $(\mathit{Cont}-t)$, $(\mathit{Match}-\mathit{Pro})$, $(\mathit{Match}-\mathit{Var})$, $(\mathit{Type}-\mathit{Extend})$, $(\mathit{Cont}-x)$, $(\mathit{Var})$, and $(\mathit{Abs})$, one can derive $\Gamma, t \not\vdash \mathit{prot} \langle R, n:\sigma \rangle \oplus \bar{m}, n \vdash \lambda s.s : t \to t$. From the above premises, by applying the $(\mathit{Select})$ rule, we have $\Gamma \vdash \mathit{Sel}(e, n, \lambda s.s) : \sigma[\tau/t]$ and, by possibly repeatedly applying $(\mathit{Pre}-\mathit{Extend})$ in $\Delta$, we have the thesis.

(Success) The derivation $\Delta$ of $\Gamma \vdash \mathit{Sel}(e_1 \leftrightarrow n = e_2, n, e_3) : \beta$ must terminate with a $(\mathit{Select})$ rule, deriving $\Gamma \vdash \mathit{Sel}(e_1 \leftrightarrow n = e_2, n, e_3) : \sigma[(\tau \oplus \bar{n})/t]$, possibly followed by applications of $(\mathit{Pre}-\mathit{Extend})$. The premises of $(\mathit{Select})$ are:

$$ \Gamma \vdash (e_1 \leftrightarrow n = e_2) : \tau \qquad (3) $$
$$ \Gamma \vdash \tau \dashv prot. \langle R, n: \sigma \rangle \oplus \bar{m}, n \quad (4) $$

$$ \Gamma, t \dashv prot. \langle R, n: \sigma \rangle \oplus \bar{m}, n \vdash e_3 : t \to t \oplus \bar{n} \quad (5) $$

From (4) and (5), through the Substitution Proposition, we have $\Gamma \vdash e_3 : \tau \to \tau \oplus \bar{n}$; from this latter judgment and (3), by the (Appl) rule, we derive:

$$ \Gamma \vdash e_3 \langle e_1 \leftrightarrow n = e_2 \rangle : \tau \oplus \bar{n} \quad (6) $$

The judgment (3) can only be obtained using either the (Extend) rule or the (Override) one, possibly followed by some applications of (Pre-Extend). Here we consider only the case where (Extend) is applied, since (Override) can be managed similarly, with the difference that in some points the proof is simpler. Hence, let us assume that (Extend) derives $\Gamma \vdash \langle e_1 \leftrightarrow n = e_2 \rangle : \rho \oplus n$ from the premise $\Gamma \vdash e_1 : \rho$ and:

$$ \Gamma \vdash \rho \dashv prot. \langle R_1, n: \sigma_1 \rangle \oplus \bar{p} \quad (7) $$

$$ \Gamma, t \dashv prot. \langle R_1, n: \sigma_1 \rangle \oplus \bar{p}, n \vdash e_2 : t \to \sigma_1 \quad (8) $$

By inspection of the (Pre-Extend) rule, we can readily derive $\Gamma \vdash \tau \dashv \rho \oplus n$. From (7), by Lemma C.5.(vii), we have $\Gamma \vdash \rho \oplus n \dashv prot. \langle R_1, n: \sigma_1 \rangle \oplus \bar{p}, n$, and, by transitivity of matching, $\Gamma \vdash \tau \dashv prot. \langle R_1, n: \sigma_1 \rangle \oplus \bar{p}, n$. From this latter judgment and (4), by Lemma C.5.(vi) (Matching uniqueness), it follows that $\sigma \equiv \sigma_1$.

On the other hand, by Lemma C.5.(ix), we have $\Gamma \vdash \tau \oplus \bar{n} \dashv \tau$ and, by transitivity of matching, $\Gamma \vdash \tau \oplus \bar{n} \dashv prot. \langle R_1, n: \sigma \rangle \oplus \bar{p}, n$. From this latter judgment and (8), by the Substitution Proposition, we have $\Gamma \vdash e_2 : \tau \oplus \bar{n} \to \sigma[(\tau \oplus \bar{n})/t]$, and, in turn, from this and (6), $\Gamma \vdash e_2(e_3 \langle e_1 \leftrightarrow n = e_2 \rangle) : \sigma[(\tau \oplus \bar{n})/t]$ via the (Appl) rule. Finally, by repeating possible applications of (Pre-Extend) in $\Delta$, we obtain the thesis.

(Next) As argued for (Success), the derivation of $\Gamma \vdash Sel(\langle e_1 \leftrightarrow n = e_2 \rangle, m, e_3) : \beta$ must end with a (Select) rule, deriving $\Gamma \vdash Sel(\langle e_1 \leftrightarrow n = e_2 \rangle, m, e_3) : \sigma[(\tau \oplus \bar{m})/t]$, possibly followed by applications of (Pre-Extend). The premises of (Select) are:

$$ \Gamma \vdash \langle e_1 \leftrightarrow n = e_2 \rangle : \tau \quad (9) $$

$$ \Gamma \vdash \tau \dashv prot. \langle R, m: \sigma \rangle \oplus \bar{n}, m \quad (10) $$

$$ \Gamma, t \dashv prot. \langle R, m: \sigma \rangle \oplus \bar{n}, m \vdash e_3 : t \to (t \oplus \bar{m}) \quad (11) $$

The judgment (9) can only be derived using either the (Extend) rule or the (Override) one, possibly followed by some applications of (Pre-Extend). As carried out in the proof for the (Success) rule, we address here only the case where (Extend) is applied, being the (Override) case similar but simpler.

Since (Pre-Extend) has been applied and (9) holds, $\tau$ must be in the form $prot. \langle R_1, m: \sigma, n: \sigma_1 \rangle \oplus \bar{n}, m, n$. Hence, let (9) be derived through (Pre-Extend) from:

$$ \Gamma \vdash \langle e_1 \leftrightarrow n = e_2 \rangle : prot. \langle R_2, m: \sigma, n: \sigma_1 \rangle \oplus \bar{n}, m, n $$

(where $R_2 \subseteq R_1$), which, in turn, is derived via the (Extend) rule from the premises:

$$ \Gamma \vdash e_1 : prot. \langle R_2, m: \sigma, n: \sigma_1 \rangle \oplus \bar{n}, m \quad (12) $$

$$ \Gamma \vdash prot. \langle R_2, m: \sigma, n: \sigma_1 \rangle \oplus \bar{n}, m \dashv prot. \langle R_3, n: \sigma_1 \rangle \oplus \bar{p} \quad (13) $$

$$ \Gamma \vdash t \dashv prot. \langle R_3, n: \sigma_1 \rangle \oplus \bar{p}, n \vdash e_2 : t \to \sigma_1 \quad (14) $$

Then, let $\rho$ represent the type $prot. \langle R_1, m: \sigma, n: \sigma_1 \rangle \oplus \bar{n}, m$, i.e. $\tau \equiv \rho \oplus n$. From the judgment (12), by the (Pre-Extend) rule, we can derive:

$$ \Gamma \vdash e_1 : \rho \quad (15) $$

By the (Match-Pro) rule, we have $\Gamma \vdash \rho \oplus n \dashv prot. \langle R_2, m: \sigma, n: \sigma_1 \rangle \oplus \bar{n}, m$ and, from this latter judgment, (13) and (14), by transitivity of matching and the Weakening Lemma, we derive $\Gamma, t \dashv \rho \oplus n \vdash e_2 : t \to \sigma_1$. From it, by means of the (Extend) rule:

$$ \Gamma, t \dashv \rho, s: t \vdash \langle s \leftrightarrow n = e_2 \rangle : t \oplus n \quad (16) $$

Now, through (10), the (Match-Var) rule, and the transitivity of matching, one can derive $\Gamma, t \dashv \rho \vdash t \oplus n \dashv prot. \langle R, m: \sigma \rangle \oplus \bar{n}, m$. From this latter judgment and (11), by Substitution, we obtain $\Gamma, t \dashv \rho \vdash e_3 : t \oplus n \to t \oplus n \oplus \bar{m}$, and, from this judgment and (16), by the (Appl) and (Abs) rules, we have:

$$ \Gamma, t \dashv \rho \vdash \lambda s. e_3 \langle s \leftrightarrow n = e_2 \rangle : t \to t \oplus n \oplus \bar{m} $$

This judgment, together with (15), allows us to apply the (Select) rule, thus deriving:

$$ \Gamma \vdash Sel(e_1, m, \lambda s. e_3 \langle s \leftrightarrow n = e_2 \rangle) : \sigma[(\rho \oplus n \oplus \bar{m})/t] $$

Finally, we get the thesis via the usual repeated applications of (Pre-Extend). $\square$

# D. Soundness of the Type System with Subsumption $\lambda Ob_S^{\oplus}$

**Theorem D.1 (Subject Reduction, $\lambda Ob_S^{\oplus}$)**

If $\Gamma \vdash e : \beta$ and $e \to e'$, then $\Gamma \vdash e' : \beta$.

As in Theorem C.9 (type system without subsumption), we prove that the type is preserved by each of the reduction rules (Beta), (Selection), (Success), and (Next). Also in this case closure under contextual reduction is dealt using the analogue of Lemma C.7 (Substitution) for $\lambda Ob_S^{\oplus}$. In the present case we have to manage the extra difficulty of possible applications of the (Subsume) rule.

(Beta) The derivation of $\Gamma \vdash (\lambda x. e_1) e_2 : \beta$ needs to terminate with a rule (Appl), deriving $\Gamma \vdash (\lambda x. e_1) e_2 : \alpha$, possibly followed by some applications of (Pre-Extend) and (Subsume). The premises of (Appl) must be $\Gamma \vdash (\lambda x. e_1) : \sigma \to \alpha$ and $\Gamma \vdash e_2 : \sigma$, where the first judgment has to be derived via (Abs), followed by possible applications of (Subsume). Let $\Gamma \vdash (\lambda x. e_1) : \sigma_1 \to \alpha_1$ be the conclusion of the (Abs) rule, and:

$$ \Gamma, x: \sigma_1 \vdash e_1 : \alpha_1 \quad (17) $$

its premise. Since the (Subsume) rule has been applied, we have $\Gamma \vdash \sigma_1 \to \alpha_1 \dashv \sigma \to \alpha$ and $\Gamma \vdash \sigma \to \alpha : *_{rgd}$, therefore $\Gamma \vdash \sigma \dashv \sigma_1$ and $\Gamma \vdash \sigma_1 : *_{rgd}$ and $\Gamma \vdash \alpha_1 \dashv \alpha$, where $\Gamma \vdash$
α : *<sub>rgd</sub>. Using these judgments and (17) it is not difficult to prove, by structural induction, that Γ, x:σ ⊢ e₁ : α₁. By Substitution Proposition, we have then Γ ⊢ e₁[e₂/x] : α₁, and, by the (Subsume) rule, Γ ⊢ e₁[e₂/x] : α, from which we get the thesis.

(Selection) This case works as for the system without subsumption.

(Success) As in Theorem C.9, we can start by asserting that the derivation Δ of Γ ⊢ Sel(⟨e₁<sub>⊕</sub> n = e₂⟩, n, e₃) : β must end with a (Select) rule, deriving Γ ⊢ Sel(⟨e₁<sub>⊕</sub> n = e₂⟩, n, e₃) : σ[(τ ⊕ <n>/t)]. This is possibly followed by applications of the (Pre-Extend) rule and, in the present case, also the (Subsume) rule. The premises of (Select) are the following:

$$ \Gamma \vdash \langle e_1 \leftarrow \leftarrow n = e_2 \rangle : \tau \quad (18) $$

$$ \Gamma \vdash \tau \dashv \sharp \mathrm{objt}. \langle R, n: \sigma \rangle \oplus \bar{m}, n \quad (19) $$

$$ \Gamma, t \dashv \sharp \mathrm{objt}. \langle R, n: \sigma \rangle \oplus \bar{m}, n \vdash e_3 : t \to t \oplus \bar{n} \quad (20) $$

If judgment (18) were not obtained by an application of the (Subsume) rule, we could repeat the steps made in order to prove Theorem C.9. Hence we address here the case where (18) is derived by a single application of (Subsume) (it is sufficient to consider a single application, because consecutive applications can be compressed into a single one). Hence, let the premises of (Subsume) be:

$$ \Gamma \vdash \langle e_1 \leftarrow \leftarrow n = e_2 \rangle : \rho \quad (21) $$

$$ \Gamma \vdash \rho \dashv \sharp \tau \quad (22) $$

$$ \Gamma \vdash \tau : *_{rgd} \quad (23) $$

From the judgments (19), (22) and (20), by transitivity of matching and Substitution, we have Γ ⊢ e₂ : ρ → ρ ⊕ <n>. From this and (21), by the (Appl) rule, we derive:

$$ \Gamma \vdash e_3 \langle e_1 \leftarrow \leftarrow n = e_2 \rangle : \rho \oplus \bar{n} \quad (24) $$

Again, by repeating the steps carried out for Theorem C.9 (case analysis on the derivation of (21)), we can prove that Γ ⊢ e₂(e₃⟨e₁<sub>⊕</sub> n = e₂⟩) : σ[(ρ ⊕ <n>/t)].

Now, from (19) and (23) follows that t is covariant in σ and Γ ⊢ σ : *<sub>rgd</sub>, and from Lemma 6.12 that Γ ⊢ σ[(ρ ⊕ <n>/t)]dashvσ[(τ ⊕ <n>/t)] and Γ ⊢ σ[(τ ⊕ <n>/t)] : *<sub>rgd</sub>. Finally, by an application of the (Subsume) rule, we have Γ ⊢ e₂(e₃⟨e₁<sub>⊕</sub> m = e₂⟩) : σ[(τ ⊕ <n>/t)], and from this we have the thesis via possibly repeated applications of (Pre-Extend) in Δ.

(Next) As in the version without subsumption, we start from the derivation Δ of Γ ⊢ Sel(⟨e₁<sub>⊕</sub> n = e₂⟩, m, e₃) : β, which has to terminate with a (Select) rule, deriving Γ ⊢ Sel(⟨e₁<sub>⊕</sub> n = e₂⟩, m, e) : σ[(τ ⊕ <m>/t)], possibly followed by applications of the (Pre-Extend) and (Subsume) rules. Let the premises of (Select) be:

$$ \Gamma \vdash \langle e_1 \leftarrow \leftarrow n = e_2 \rangle : \tau \quad (25) $$

$$ \Gamma \vdash \tau \dashv \sharp \mathrm{objt}. \langle R, m: \sigma \rangle \oplus \bar{m}, m \quad (26) $$

$$ \Gamma, t \dashv \sharp \mathrm{objt}. \langle R, m: \sigma \rangle \oplus \bar{n}, m \vdash e_3 : t \to (t \oplus \bar{m}) \quad (27) $$

If the judgment (25) were not obtained by an application of the (Subsume) rule, we could repeat the steps used to prove Theorem C.9. Hence, we discuss here the case where (25) is derived by a single application of (Subsume), from the premises:

$$ \Gamma \vdash \langle e_1 \leftarrow \leftarrow n = e_2 \rangle : \rho \quad (28) $$

$$ \Gamma \vdash \rho \dashv \sharp \tau \quad (29) $$

$$ \Gamma \vdash \tau : *_{rgd} \quad (30) $$

From these hypotheses, by repeating the same steps used in the proof without subsumption (case analysis on the derivation of the judgment (28)), we deduce:

$$ \Gamma \vdash Sel(e_1, m, \lambda s. e_3 \langle s \leftarrow \leftarrow n = e_2 \rangle) : \sigma[(\rho \oplus n \oplus \bar{m})/t] $$

Finally, the proof can be accomplished as in the (Success) case, by applying Lemma 6.12 and by means of the (Subsume) and (Pre-Extend) rules. □

## About the authors

Alberto Ciaffaglione is an independent researcher whose main interest is the area of proof assistants and their applications to software dependability. PhD in Computer Science at the Università degli Studi di Udine (Italy) and the Institut National Polytechnique de Lorraine (France), then Research Fellow at the University of Sussex (UK), he currently collaborates with the Università degli Studi di Udine. You can contact him at alberto.ciaffaglione@uniud.it, alberto.ciaffaglione@libero.it or visit http://users.dimi.uniud.it/~alberto.ciaffaglione.

Pietro Di Gianantonio is professor at the Università degli Studi di Udine (Italy). His interests include computable analysis, type assignment systems, semantics of programming languages. You can contact him at pietro.digianantonio@uniud.it or visit http://users.dimi.uniud.it/~pietro.digianantonio.

Furio Honsell is full professor in Computer Science at the Università degli Studi di Udine (Italy). His interests are in foundations of informatics, λ-calculus, Logical Frameworks, semantics of programming languages, and software dependability. Currently he is serving as elected member of the Regional Council of the Friuli Venezia Giulia Region (Italy). You can contact him at furio.honsell@uniud.it.

Luigi Liquori MS 1990 Udine University, Ph.D. 1996 University of Turin, H.d.R. 2007 Institut National Polytechnique de Lorraine, served as Lecturer at the Ecole Nationale des Mines de Nancy from 1999. Since 2001, he is a senior researcher at French Institute for Research in Computer Science and Automation. Luigi Liquori research's fields range from logics and foundations of interactive proof assistants, to semantics of object oriented programming languages, until foundations of overlay networks, ETSI oneM2M IoT resource discovery protocols, and recently IoT-based Digital Contact Tracing against Covid-19 pandemics. You can contact him at Luigi.Liquori@inria.fr.