Nicolas Haderer
email: nicolas.haderer@inria.fr

Vincent Primault
email: vincent.primault@liris.cnrs.fr

Patrice Raveneau
email: patrice.raveneau@inria.fr

Christophe Ribeiro
email: christophe.ribeiro@inria.fr

Romain Rouvoy
email: romain.rouvoy@univ-lille1.fr

Sonia Ben Mokhtar
email: sonia.ben-mokhtar@liris.cnrs.fr

Towards a Practical Deployment of Privacy-preserving Crowd-sensing Tasks

Keywords: C.2.4 [Distributed Systems]: Distributed Applications; K.4.1 [Computers and society]: Public policy issuesprivacy Algorithms, Security crowd-sensing, privacy, mobile crowdsourcing, middleware

Recent generations of mobile phones, embedding a wide variety of sensors, have fostered the development of open sensing applications, such as network quality or weather forecast applications. In this paper, we present a novel privacy-preserving crowdsourcing platform relying on two components: APISENSE and PRIVAPI. APISENSE is a distributed middleware platform that leverages the dynamic deployment of crowdsourcing tasks across a population of mobile phones. PRIVAPI is a middleware handling privacypreserving publication of mobility data.

INTRODUCTION

The increasing popularity of mobile devices has raised the opportunity to easily connect to a crowd of mobile users and to engage them in the completion of a variety of cyberphysical tasks. In particular, mobile crowdsourcing (or crowdsensing) refers to the capability of lifting a large and diffuse group of users to delegate the task of retrieving trustable data from the field. The pervasive nature of mobile crowdsourcing allows easy gathering of mobility data, which consists in all timestamped locations where a user has been during the experiment. This obviously raises some serious concerns about privacy, not taken in account by existing solutions like the Funf Open Sensing Framework1 . As it has been demonstrated by several papers like [START_REF] Krumm | Inference Attacks on Location Tracks[END_REF] it is possible to use mobility data about individuals to infer a lot of knowledge like where they work, where they live and ultimately who they are. Mobility data can also be used to learn sensitive information like religious or political preferences.

APISENSE is a mobile crowdsourcing platform that makes easier the deployment of crowd-sensing experiment by taking care of the critical challenges in this area [START_REF] Haderer | Dynamic Deployment of Sensing Experiments in the Wild Using Smartphones[END_REF]. The novelty is therefore to provide a Software-as-a-Service platform where crowd-sensing experiments are described as scripts, which will be offloaded onto mobile devices in order to collect data on the field.

PRIVAPI is a privacy-preserving middleware that can be easily integrated on-top of APISENSE. Its goal is to preprocess gathered mobility data before it is released. Thanks to its knowledge on the whole dataset it can use an optimal anonymization strategy on mobility data while still offering a satisfactory level of utility. At the moment one novel strategy satisfying these two criteria is implemented in PRI-VAPI.

In the remainder of the paper, we provide an overview of the APISENSE platform in Section 2) and the PRIVAPI middleware in Section 3), before concluding in Section 4).

THE APISENSE PLATFORM

APISENSE builds on a distributed architecture. In its center sits the Hive service, that is responsible for managing the community of mobile users and publishing crowd-sensing tasks. These crowd-sensing tasks are uploaded on the Hive from Honeycomb endpoints, which are deployed and used by people interested in collecting specific datasets. The Honeycomb is therefore used to describe the crowd-sensing tasks as scripts (based on an extension of JavaScript) that are seamlessly offloaded onto mobile devices by the Hive. Once triggered by the mobile device, these scripts will automatically produce a dataset, which will be sent back to the Honeycomb to be processed and stored depending on experiments.

One of the benefits of building a common platform like APISENSE lies in the federation of communities of mobile users who are willing to contribute to mobile crowdsourcing experiments in order to ease their recruitment and therefore focus on the nature of the datasets to be collected. The APISENSE platform also implements the concept of virtual sensors as a mean to abstract the individual devices and therefore offer a set of additional services that self-organize a group of mobile devices to orchestrate the retrieval of datasets according to different strategies (e.g., round robin, energy-aware). The APISENSE platform supports the implementation of different incentive strategies, including user feedback, user ranking, user rewarding and win-win services. The selection of incentive strategies carefully depends on the nature of the crowdsourcing experiments.

Concerning privacy, a first layer is deployed on the mobile device and implements several algorithms to filter out and blur sensitive information (e.g., address book, location) depending on user preferences. The user keeps the control of her mobile phone to select the sensors to be shared, as well as when and where these sensors can be used by the platform.

THE PRIVAPI MIDDLEWARE

PRIVAPI is a generic middleware that can be integrated with any crowd-sensing platform. It focuses on protecting mobility data, which comes with specific threats against location privacy. We have previously studied in [START_REF] Primault | Differentially Private Location Privacy in Practice[END_REF] the impact of points of interest, which are places where a user spends significant amounts of time like his home, his office, a cinema, etc. These places are highly sensitive because they convey rich semantic information. Moreover, they allow to almost uniquely identify individuals by studying their mobility patterns. We have shown that even a recent state-of-the art protection mechanism still allows to re-identify at least 60 % of the points of interest from a real-life dataset.

PRIVAPI leverages the global knowledge of the whole system to apply an optimal anonymization strategy and produce a privacy-preserving mobility dataset. Because published data will be used by researchers or industrials, it must guarantee both privacy and utility. A minimum level of privacy must be enforced, as parametrized by the users and/or the platform owner. In the same time, our middleware wants to be utility-driven. We believe there is not one unique anonymization strategy that always performs well but many from which we can choose the one that fits the best to the usage that will be done with the anonymized dataset.

Because of the threats related to points of interest, we have implemented an original anonymization strategy that focuses on hiding these places. To achieve that we use an algorithm that smoothes speed along a trajectory (typically one day of data) to guarantee that speed is constant. This still allows to analyze the trajectory of a user but prevents to find out places where he stopped during his day. First experiments show that under such a protection utility of our anonymized dataset remains high for useful data mining tasks such as finding out crowded places or predicting traffic.

CONCLUSION

We introduced a privacy-preserving crowd-sensing platform composed of two complementary components. APISENSE 2as an open platform that can be used to quickly deploy a wide diversity of crowdsourcing tasks. PRIVAPI is a middleware protecting mobility data by producing privacypreserving yet useful anonymized datasets.

Figure 1 :

 1 Figure 1: Architecture of the data collection platform.

http://www.funf.org

APISENSE online: http://www.apisense.com

ACKNOWLEDGMENTS

This work was supported by the LABEX IMU (ANR-10-LABX-0088) of Université de Lyon, within the program "Investissements d'Avenir" (ANR-11-IDEX-0007) operated by the French National Research Agency (ANR).


Cinzia Di Giusto

Jorge A Perez

Jorge A Perez An

Jorge A Pérez

An Event-Based Approach to Runtime Adaptation in Communication-Centric Systems

Introduction

Context. Modern software systems are built as assemblies of heterogeneous artifacts which must interact following predefined protocols. Correctness in these communication-centric systems largely depends on ensuring that dialogues are consistent. Sessionbased concurrency is a type-based approach to ensure conformance of dialogues to prescribed protocols: dialogues are organized into units called sessions; interaction patterns are abstracted as session types [START_REF] Honda | Language primitives and type discipline for structured communication-based programming[END_REF], against which specifications may be checked.

As communication-centric systems operate on open infrastructures, runtime adaptation appears as a crucial feature to ensure continued system operation. Here we understand runtime adaptation as the dynamic modification of (the behavior of) the system in response to an exceptional event, such as, e.g., a varying requirement or a local failure. These events are not necessarily catastrophic but are hard to predict. As such, protocol conformance and dynamic reconfiguration are intertwined concerns: although the specification of runtime adaptation is not strictly tied to that of structured protocols, steps of dynamic reconfiguration have a direct influence in a system's interactive behavior.

We are interested in integrating forms of runtime adaptation into models of sessionbased concurrency. As a first answer to this challenge, in previous work [START_REF] Giusto | Disciplined structured communications with disciplined runtime adaptation[END_REF] we extended a typed process framework for binary sessions with basic constructs from the model of adaptable processes [2]. In this work, with the aim of extending the applicability and expressiveness of the approach in [START_REF] Giusto | Disciplined structured communications with disciplined runtime adaptation[END_REF], we propose adaptation mechanisms which depend on the state of the session protocols active in a given location. As a distinctive feature, we advocate an event-based approach: by combining constructs for dynamic type inspection and non-blocking event detection (as put forward by Kouzapas et al. [START_REF] Kouzapas | On asynchronous eventful session semantics[END_REF][START_REF] Kouzapas | A Study of Bisimulation Theory for Session Types[END_REF]), adaptation requests, both internal or external to the location, can be naturally assimilated to events.

A Motivating Example.

Here we consider a standard syntax for binary session types [START_REF] Honda | Language primitives and type discipline for structured communication-based programming[END_REF]: where T stands for both basic types (e.g., booleans, integers) and session types α. Also, n 1 , . . . , n m denote labels. To illustrate session types, consider a buyer B and a seller S which interact as follows. First, B sends to S the name of an item and S replies back with its price. Then, depending on the amount, B either adds the item to its shopping cart or closes the transaction. In the latter case the protocol ends. In the former case B must further choose a paying method. From B's perspective, this protocol may be described by the session type α = !item. ?amnt. α pay , where item and amnt are base types and α pay = ⊕{addItem : ⊕{ccard : α cc , payp : α pp } , cancel : ε}.

Thus, session type α says that protocol α pay may only be enabled after sending a value of type item and receiving a value of type amnt. Also, addItem, ccard, cc, and payp denote labels in the internal choice. Types α cc and α pp denote the behavior of each payment method. Following the protocol abstracted by α, code for B may be specified as a π-calculus process. Processes P and R below give two specifications for B: P = x(book).x(a).if a < 50 then x ⊳ addItem; x ⊳ ccard; P c else x ⊳ cancel; 0 R = x(game).x(b).if b < 80 then x ⊳ addItem; x ⊳ payp; R p else x ⊳ cancel; 0 Thus, although both P and R implement α, their behavior is rather different, for they purchase different items using different payment methods (which are abstracted by processes P c and R p ). Let us now analyze the situation for the seller S. To ensure protocol compatibility and absence of communication errors, the session type for S, denoted β, should be dual to α. This is written α ⊥ C β. Intuitively, duality decrees that every action from B must be matched by a complementary action from S, e.g., every output of a string in α is matched by an input of a string in β. In our example, we let β = ?item. !amnt. β pay , where β pay and a process implementation for S are as follows:

β pay = &{addItem : &{ccard : β cc , payp : β pp } , cancel : ε} Q = y(i).y(price(i)).y ⊲ {addItem : y ⊲ {ccard :

Q c [] ppal : Q p } [] cancel : 0}
where price stands for an auxiliary function. Also, β cc and β pp are the duals of α cc and α pp ; they are realized by processes Q c y and Q p y . The interaction of P and Q is defined using session initialization constructs: process u(x:α).P denotes the request of a session of type α; dually, u(x:α).P denotes the acceptance of a session of type α. In both cases, u denotes a (shared) name used for synchronization. In our example, we may have Sys = u(x:α).P | u(y:β).Q -→ (νκ

)(P [ κ + /x] | Q[ κ - /y]) = S ′
Thus, upon synchronization on u, a new session κ is established. Intuitively, in process S ′ session κ is "split" into two session channels (or endpoints) κ + and κ -: we write + and to denote their opposing polarities, which make their complementarity manifest. The use of restriction (νκ) covers both channels, thus ensuring an interference-free medium for executing the session protocols described by α and β.

In this work, we are interested in ways of expressing and reasoning about the dynamic modification of session-typed processes such as P and Q above. Such modifications may be desirable to react to exceptional runtime conditions (say, an error) or to implement new requirements. For instance, the type below defines a new payment method for S:

β gift = &{addItem : &{giftc : β gc , ccard : β cc , payp : β pp } , cancel : ε}
Intuitively, β gift extends β pay with a new alternative on label giftc. As such, it is safe to use a process implementing β gift wherever a process implementing β pay is required. The safe substitution principle that connects β gift and β pay is formalized by a subtyping relation on session types [START_REF] Gay | Subtyping for session types in the pi calculus[END_REF], denoted ≤ C . In our example, we have β pay ≤ C β gift .

In previous work [START_REF] Giusto | Disciplined structured communications with disciplined runtime adaptation[END_REF] we studied how to update processes when sessions have not yet been established; this suffices to analyze runtime adaptation for processes such as Sys above. In this paper, we go further and address the runtime adaptation of processes such as S ′ above, which contain already established session protocols. As we would like to guarantee that adaptation preserves overall system correctness, a key challenge is ensuring that adaptation does not jeopardize such protocols. Continuing our example, let S ′′ be the process resulting from S ′ above, after the first step stipulated by α and β (i.e., an exchange of a value of type item). Intuitively, at that point, the buyer part of S ′ will have session type ?amnt. α pay , whereas the seller part of S ′ will have session type !amnt. β pay . Suppose we wish to modify at runtime the part of S ′′ realizing the buyer behavior. To preserve protocol correctness, a candidate new implementation must conform, up to ≤ C , to the type ?amnt. α pay ; a process realizing any other type will fail to safely interact with the part of S ′′ implementing the seller. In [START_REF] Giusto | Disciplined structured communications with disciplined runtime adaptation[END_REF] we defined the notion of consistency to formalize the correspondence between declared session protocols and the processes installed by steps of runtime adaptation. As we will see, consistency is still appropriate for reasoning about runtime adaptation of processes with active sessions.

Our Approach. Having motivated the context of our contributions, we move on to describe some technical details. We rely on a process language which extends session πcalculi with locations, located processes, and update processes [2]. We use locations as explicit delimiters for process behavior: these are transparent, possibly nested computation sites. Given a location loc and a process P , the located process loc[P ] denotes the fact that P resides in loc (or, alternatively, that P has scope loc). This way, e.g., process W = sys buyer u(x:α).P | seller u(y:β).Q represents an explicitly distributed variant of Sys above: the partners now reside in locations buyer and seller; location sys encloses the whole system. An update process, denoted loc{U }, intuitively says that the behavior currently enclosed by loc should be replaced according to the adaptation routine U . Since a location may enclose one or more session channels, update processes allow for flexible specifications of adaptation routines. This way, e.g., one may specify an update on buyer that does not involve seller (and vice versa); also, a system-level adaptation could be defined by adding a process sys{U s } in parallel to W , given an U s that accounts for both buyer and seller behaviors.

The integration of runtime adaptation into sessions is delicate, and involves defining not only what should be the state of the system after adaptation but also when an adaptation step should be triggered. To rule out careless adaptation steps which jeopardize established protocols, communication and adaptation actions should be harmonized. As hinted at above, in previous work [START_REF] Giusto | Disciplined structured communications with disciplined runtime adaptation[END_REF] we proposed admitting adaptation actions only when locations do not enclose running sessions. This is a simple solution that privileges communication over adaptation, in the sense that adaptation is enabled only when sessions are not yet active. Still, in realistic applications it may be desirable to give communication and adaptation a similar status. To this end, in this paper we admit the adaptation of locations with running sessions. We propose update processes loc{U } in which U is able to dynamically check the current state of the session protocols running in loc. In their simplest form, our update processes concern only one session channel and are of the shape loc case x of {(x:β i ) :

U i } i∈I
where I is a finite index set, x denotes a channel variable, each β i and U i denotes a session type and an alternative (process) U i , respectively. (We assume x occurs free in U i .)

The informal semantics for this construct is better understood by considering its interaction with a located process loc Q in which Q implements a session of type α along channel κ p . The two processes may interact as follows. If there is a j ∈ I such that types α and β j "match" (up to ≤ C ), then there is a reduction to process loc U j [ κ p /x] . Otherwise, if no β j validates a match, then there is a reduction to process loc Q , keeping the behavior of loc unchanged and consuming the update.

In general, update processes may define adaptation for locations enclosing more than one session channel. In the distributed buyer-seller example, the process below defines a runtime update which depends on the current state of the two channels at location sys:

U xy = sys case x, y of (x:α ; y:β) : buyer[R] | seller[Q]
(x:α pay ; y:β pay ) : buyer

[P * ] | seller[Q * ] (1)
U xy defines two possibilities for runtime adaptation. If the protocol has just been established (i.e., current types are α and β) then only the buyer is updated-its new behavior will be given by R above. If both item and price information have been already exchanged then implementations P * and Q * , compliant with types α pay and β pay , are installed. Update processes rely on the protocol state at a given location to assess the suitability of adaptation routines. Our semantics for update relies on (a) monitors which store the current type for each running session; and (b) a type-directed test on the monitors enclosed in a given location. This test generalizes the typecase construct in [START_REF] Kouzapas | A Study of Bisimulation Theory for Session Types[END_REF].

While expressive, our typeful update processes by themselves do not specify when adaptation should be available. Even though update processes could be embedded within session communication prefixes (thus creating causal dependencies between communication and adaptation), such a specification style would only allow to handle exceptional conditions which can be fully characterized in advance. Other kinds of exceptional con-ditions, in particular contextual and/or unsolicited runtime conditions, are much harder to express by interleaving update processes within structured protocols.

To offer a uniform solution to this issue, we propose a event-based approach to trigger updates. We endow each location with a queue of adaptation requests; such requests may be internal or external to the location. In our example, an external request could be, e.g., a warning message from the buyer's bank indicating that an exchange with the bank is required before committing to the purchase with the seller.

Location queues are independent from session behavior. Their identity is visible to processes; they are intended as interfaces with other processes and the environment. To issue an adaptation request r for location loc, our process syntax includes adaptation signals, written loc(r). Similar to ordinary communication prefixes, these signals are orthogonal to sessions. Then, we may detect the presence of request r in the queue of loc using the arrival predicate arrive(loc, r) [START_REF] Kouzapas | A Study of Bisimulation Theory for Session Types[END_REF]. As an example, let upd E denote an external adaptation request. To continuously check if an external request has been queued for sys, the process below combines process U xy in (1) with arrival predicates, conditionals, and recursion:

U * xy = µX .if arrive(sys, upd E ) then U xy else X (2)
We couple our process model for session-based concurrency and runtime adaptation with a type system that ensures the following key properties:

-Safety: well-typed programs do not exhibit communication errors (e.g., mismatched messages). -Consistency: well-typed programs do not allow adaptation actions that disrupt already established sessions.

Safety is the typical guarantee expected from any session type discipline, here considered in a richer setting that combines session communication with runtime adaptation. In contrast, consistency is a guarantee unique to our setting: it connects the behavior of the adaptation mechanisms with the preservation of prescribed typed interfaces. We show that well-typed programs are safe and consistent (Theorem 3.6): this ensures that specified session protocols are respected, while forbidding incautious adaptation steps that could accidentally remove or disrupt the session behavior of interacting partners.

Organization. The rest of the paper is organized as follows. Next we present our eventbased process model of session communication with typeful constructs for runtime adaptation ( § 2). Then, we present our session type system, which ensures safety and consistency for processes with adaptation mechanisms ( § 3). In § 4 we discuss a process model of communication and adaptation with explicit compartments; it distills the main features of the model in § 2. At the end, we discuss related works and draw some concluding remarks ( § 5). The appendix gives full sets of reduction and typing rules. The appendix collects omitted definitions and proofs. variables, ranged over by x, y, . . .. Values, ranged over v, v ′ , . . ., may include booleans (written false and true), integers, names, and channels. We use r to range over adaptation messages: two instances are upd I and upd E , for internal and external requests. We use • to denote finite sequences. Thus, e.g., x is a sequence of variables x 1 , . . . , x n . We use ǫ to denote the empty sequence. Table 1 reports the syntax of expressions and processes. Processes include usual constructs for input, output, and labeled choice. Common forms of recursion, parallel composition, conditionals, and restriction are also included. As illustrated in § 1, constructs for session establishment are annotated with a session type α, which is useful in derived static analyses. A prefix for closing a session, inherited from [START_REF] Giusto | Disciplined structured communications with disciplined runtime adaptation[END_REF], is convenient to structure specifications. Variable x is bound in processes u(x:α).P , u(x:α).P , and k(x).P . Binding for name and channel restriction is as usual. Also, recursion variable X is bound in process µX .P . Given a process P , its sets of free/bound channels, names, variables, and recursion variables-noted fc(P ), fn(P ), fv(P ), fpv(P ), bc(P ), bn(P ), bv(P ), and bpv(P ), respectively-are as expected. We always rely on usual notions of α-conversion and (capture-avoiding) substitution, denoted [ k /x] (for channels) and [ P /X ] (for processes). We write [ k1, . . . , kn /x1, . . . , xn] to stand for an n-ary simultaneous substitution. Processes without free variables or free channels are called programs.

| loc case x of {(x 1 :β i 1 ; • • • ; x m :β i m ) : Qi}i∈I typeful update process | loc(r) | loc⌊ r⌋ adaptation signal / queue
Up to here, the language is a synchronous π-calculus with sessions. Building upon locations loc, l 1 , l 2 , . . ., constructs for adaptation are: located processes, denoted loc[P ]; update processes,

denoted loc case x 1 , . . . , x m of {(x 1 :β i 1 ; • • • ; x m :β i m ) : Q i } i∈I ; (
session) monitors, denoted κ p ⌊α⌋; location queues, denoted loc⌊ r⌋; and adaptation signals, denoted loc(r). Moreover, expressions include the arrival predicate arrive(loc, r).

We now comment on these elements. Located processes and update processes have been motivated in § 1. Here we just remark that update processes are assumed to refer to at least one variable x i and to offer at least one alternative Q i . Also, variables x 1 , . . . , x m are bound in loc case x 1 , . . . , x m of {(x 1 :

β i 1 ; • • • ; x m :β i m ) : Q i } i∈I ; this process is often abbreviated as loc case x of {(x 1 :β i 1 ; • • • ; x m :β i m ) : Q i } i∈I . Update processes
generalize the typecase introduced in [START_REF] Kouzapas | A Study of Bisimulation Theory for Session Types[END_REF], which defines a case-like choice based on a single channel; in contrast, to specify adaptation for locations with multiple open sessions, our update processes define type-directed checks over one or more channels. Update processes go hand-in-hand with monitors, runtime entities which keep the current protocol state at a given channel. We write κ p ⌊α⌋ to denote the monitor which stores the protocol state α for channel κ p . In [START_REF] Kouzapas | A Study of Bisimulation Theory for Session Types[END_REF], a similar construct is used to store in-transit messages in asynchronous communication. For simplicity, here we consider synchronous communication; monitors store only the current protocol state. This choice is aligned with our goal of identifying the core elements from the eventful session framework that are central in defining runtime adaptation (cf. Remark 3.7).

Location queues, not present in [START_REF] Kouzapas | A Study of Bisimulation Theory for Session Types[END_REF], handle adaptation requests, modeled as a possibly empty sequence of messages r. Location queues enable us to give a unified treatment to adaptation requests, internal and external. Given loc⌊ r⌋, it is worth observing that messages r are not related to communication as abstracted by session types. This represents the fact that we handle adaptation requests and structured session exchanges as orthogonal issues. An adaptation signal loc(r) enqueues request r into the location queue of loc. To this end, as detailed below, the operational semantics defines synchronizations between adaptation signals and location queues. To connect runtime adaptation and communication, our language allows the coupling of update processes with the arrival predicate on locations, denoted arrive(loc, r). Inspired by the arrive predicate in [START_REF] Kouzapas | A Study of Bisimulation Theory for Session Types[END_REF], this predicate detects if a message r has been placed in the queue of loc.

Our language embodies several concerns related to runtime adaptation: using adaptation signals and location queues we may formally express how an adaptation request is issued; arrival predicates enable us to specify when adaptation will be handled; using update processes and monitors we may specify what is the goal of an adaptation event.

Semantics. The semantics of our language is given by a reduction semantics, the smallest relation generated by the rules in Table 2. We write P -→ P ′ for the reduction from P to P ′ . Reduction relies on a standard notion of structural congruence, denoted ≡ (see Appendix A). It also relies on evaluation and location contexts:

E ::= -| k(-).P | if -then P else Q C, D ::= -| loc[C | P ] Given C -(resp. E[-]
), we write C P (resp. E[e]) to denote the process (resp. expression) obtained by filling in occurrences of holein C with P (resp. in E with e). We comment on the reduction rules below. The first four rules formalize session behavior within hierarchies of nested locations. Using duality for session types, denoted ⊥ C (see [START_REF] Gay | Subtyping for session types in the pi calculus[END_REF] and § 3), in rule :O the synchronization on a name u leads to establish a session on fresh channels κ p and κ p ; also, two monitors with the declared session types are created. Duality for polarities p is as expected: + =and -= +. Monitors are local by construction: they are created in the same contexts in which the session is established. Rule :C represents communication of a value: we require both complementary prefixes and that the monitors support input and output actions. After reduction, prefixes in processes and monitors are consumed. Similarly, rule :S for labeled choice is standard, augmented with monitors. Rule :C formalizes session termination, discarding involved monitors. The monitors in these three rules allow us to track the evolution of active session protocols. The remaining rules in Table 2 define our event-based approach to runtime adaptation. Rule :UR treats the issue of an adaptation request r as a synchronization between a location queue and an adaptation signal. The queue and the signal may be in different contexts; this enables "remote" requests. Rules :A and :A resolve arrival predicates by querying the (possibly remote) queue r. Rule :U defines the typeful update of the current protocol state at loc, which is given by an indexed set of open sessions with their associated monitors. The rule attempts to match such protocol state with the first suitable option offered by an update process for loc. If there is no matching alternative the current protocol state at loc is kept unchanged. By an abuse of notation, we write P 1 ∈ P to indicate that P 1 occurs in P , i.e., if P = C[P 1 ] for some C. Formally, given an index set I over the update process, suitability with respect to the behavior at loc is defined by predicate match I in Definition 2.1 below. Using subtyping ≤ C (see [START_REF] Gay | Subtyping for session types in the pi calculus[END_REF] and § 3), the predicate holds for an l ∈ I which defines a new protocol state.

:O C u(x : α).P | D u(y : β).Q -→ (νκ) C P [ κ p /x] | κ p ⌊α⌋ | D Q[ κ p /y] | κ p ⌊β⌋ (α ⊥C β) :C C κ p (v).P | κ p ⌊!(T ).α⌋ | D κ p (x).Q | κ p ⌊?(T ).β⌋ -→ C P | κ p ⌊α⌋ | D Q[ v /x] | κ p ⌊β⌋ :S C κ p ⊲ {nj:Pj}j∈J | κ p ⌊&{nj:αj}j∈J ⌋ | D κ p ⊳ ni; Q | κ p ⌊⊕{nj : βj}j∈J ⌋ -→ C{Pi | κ p ⌊αi⌋} | D{Q | κ p ⌊βi⌋} (i ∈ J) :C C close (κ p ).P | κ p ⌊ε⌋ | D close (κ p ).Q | κ p ⌊ε⌋ -→ C P | D Q :E if e -→ e ′ then E[e] -→ E[e ′ ] :P if P -→ P ′ then P | Q -→ P ′ | Q :R N if P -→ P ′ then (νa)P -→ (νa)P ′ :R C if P -→ P ′ then (νκ)P -→ (νκ)P ′ :S if P ≡ P ′ , P ′ -→ Q ′ , and Q ′ ≡ Q then P -→ Q :R rec X .P -→ P [ rec X .P /X ] :I T if true then P else Q -→ P :I F if false then P else Q -→ Q :UR C loc⌊ r1⌋ | D loc(r) -→ C loc⌊ r1 • r⌋ | D 0 :A r = r1 • r0 C E[arrive(loc, r1)] | D loc⌊ r⌋ -→ C E[true] | D loc⌊ r0⌋ :A ( r = r2 • r0 ∧ r1 = r2) ∨ r = ǫ C E[arrive(loc, r1)] | D loc⌊ r⌋ -→ C E[false] | D loc⌊ r⌋ :U fc(P ) = {κ p 1 , . . . , κ p m } ∀j ∈ [1, .., m].(κ p j ⌊αj⌋ ∈ P ) (V = P ) ∃l. matchI (l, {α1, . . . , αm}, {β i 1 , . . . , β i m }i∈I ) ∧ V = Q l [ κ p 1 , . . . , κ p m/ x1, . . . , xm] C loc[P ] | D loc case x of {(x 1 :β i 1 ; • • • ; x m :β i m ) : Qi}i∈I -→ C loc[V ] | D 0
In addition, our semantics includes standard and/or self-explanatory treatments for reduction under evaluation contexts, parallel composition, located context, and restriction. Also, it accounts for applications of structural congruence, recursion and conditionals.

Definition 2.1 (Matching).

Given an index set I, session types α 1 , . . . , α m , an indexed sequence of session types {β i 1 , . . . , β i m } i∈I , and an l ∈ I, we write

match I (l, {α 1 , . . . , α m }, {β i 1 , . . . , β i m } i∈I ) if and only if ∀n < l.(∃j ∈ [1..m]. β n j ≤ C α j ) ∧ ( h∈[1..m] β l h ≤ C α h ).
Example 2.2. Recall process W given in the Introduction. According to our semantics:

W -→ (νκ) sys buyer P [ κ p /x] | κ p ⌊α⌋ | seller Q[ κ p /y] | κ p ⌊β⌋ -→ 2 (νκ) sys buyer P ′ | κ p ⌊α pay ⌋ | seller Q ′ | κ p ⌊β pay ⌋
Suppose that following an external request the seller must offer a new payment method. (a gift card). Precisely, we would like S to act according to the type β gift given in §1. Let α gift be the dual of β gift . We then may define the following update process R 1 xy :

sys case x, y of {(x:α pay ; y:β pay ) : buyer

P ′ | x⌊α gift ⌋ | seller Q ′′ | y⌊β gift ⌋ }
Thus, R 1 xy keeps the expected implementation for the buyer (P ′ ), but updates its associated monitor. For the seller, both the implementation and monitor are updated; above, Q ′′ stands for a process offering the three payment methods. We may then specify the whole system as: W | µX .if arrive(sys, upd E ) then R 1 xy else X . The type system introduced next ensures, among other things, that updates such as R 1 xy consider both a process and its associated monitors, ruling out the possibility of discarding the monitors that enable reduction.

Session Types for Eventful Runtime Adaptation

This section introduces a session type system for the process language of § 2. Our main result (Theorem 3.6) is that well-typed programs enjoy both safety (absence of runtime communication errors) and consistency properties (update actions do not disrupt established sessions). Our development follows the lines of the typed framework in [START_REF] Giusto | Disciplined structured communications with disciplined runtime adaptation[END_REF].

The syntax of session types (ranged over by α, β, . . .) has been already presented in the Introduction. We consider basic types (ranged over by τ, σ, . . .) and write T, S, . . . to range over τ, α. Therefore, although our process language copes with runtime adaptation, our type syntax is standard and retains the intuitive meaning of session types [START_REF] Honda | Language primitives and type discipline for structured communication-based programming[END_REF], which we now briefly recall. Type ?(τ ).α (resp. ?(β).α) abstracts the behavior of a channel which receives a value of type τ (resp. a channel of type β) and then continues as α. Dually, type !(τ ).α (resp. !(β).α) represents the behavior of a channel which sends a value of type τ and then continues as α. Type &{n 1 : α 1 . . . n m : α m } describes a branching behavior: it offers m behaviors, and if the j-th alternative is selected then it behaves as described by type α j (1 ≤ j ≤ m). In turn, type ⊕{n 1 : α 1 . . . n m : α m } describes the behavior of a channel which may select a single behavior among α 1 , . . . , α m and then continues as α j . We use ε to type a channel with no communication behavior. Type µt.α describes recursive behavior; as usual, we consider recursive types under equi-recursive and contractive assumptions.

Along the paper we have informally appealed to duality and subtyping over session types (denoted ⊥ C and ≤ C , resp.). For the sake of space, we omit their full definitions; we just remark that since our session type structure is standard, we may rely on the (coinductive) definitions given by Gay and Hole [START_REF] Gay | Subtyping for session types in the pi calculus[END_REF], which are standard and well-understood.

Our typing judgments generalize usual notions with an interface I. Based on the syntactic occurrences of session establishment prefixes a(x:α), and a(x:α), the interface of a process describes the services appearing in it. We annotate services with a qualification q, which may be 'lin' (linear) or 'un' (unrestricted). Thus, the interface of a process gives an "upper bound" on the services that it may execute. The typing system uses interfaces to control the behavior contained by locations after an update. We have: Definition 3.1 (Interfaces). We define an interface as the multiset whose underlying set of elements is I = {q u:α | q ∈ {lin, un}} (i.e., a set of assignments from names to qualified session types). We use I, I ′ , . . . to range over interfaces. We write dom(I) to denote the set {u | u : α q ∈ I} and # I (a) = h to mean that a occurs h times in I.

The union of two interfaces is essentially the union of their underlying multisets. We sometimes write I ⊎ a : α lin and I ⊎ a : α un to stand for I ⊎ {lin a:α} and I ⊎ {un a:α}, respectively. Moreover, we write I lin (resp. I un ) to denote the subset of I involving only assignments qualified with lin (resp. un). We now define an ordering relation over interfaces, relying on subtyping: We now define our typing environments. We write q to range over qualifiers lin and un.

∆ ::= ∅ | ∆, k : α | ∆, k : ⌊α⌋
typing with active sessions

Γ ::= ∅ | Γ, e : τ | Γ, u : α q , β q first-order environment (with α q ⊥ C β q ) Θ ::= ∅ | Θ, X : ∆; I | Θ, loc : I higher-order environment
We consider typings ∆ and environments Γ and Θ. Typing ∆ collects assignments from channels to session types; it describes currently active sessions. In our system, ∆ also includes bracketed assignments, denoted κ p : ⌊α⌋, which represent the type for monitors. Subtyping extends to these assignments (⌊α⌋ ≤ C ⌊β⌋ if α ≤ C β) and thus to typings. We write dom(∆) to denote the set

{k p | k p : α ∈ ∆ ∨ k p : ⌊α⌋ ∈ ∆}. We write ∆, k : α Θ, loc : I ⊢ loc ⊲ I :L E Γ ; Θ ⊢ k⌊α⌋ ⊲ k : ⌊α⌋; ∅ :Q Γ ⊢ r1 ⊲ msg : Γ ⊢ r ⊲ msg Γ ⊢ r1 ⊲ msg Γ ⊢ r1; r ⊲ msg : Q Θ ⊢ loc ⊲ I Γ ⊢ r ⊲ msg Γ ; Θ ⊢ arrive(loc, r) ⊲ bool : Γ ⊢ r ⊲ msg Γ ; Θ ⊢ loc(r) ⊲ ∅; ∅ :S Γ ; Θ ⊢ P ⊲ ∆; I ∆ ≤C ∆ ′ I ⊑ I ′ Γ ; Θ ⊢ P ⊲ ∆ ′ ; I ′ : Γ ; Θ ⊢ P ⊲ ∆; I ∪ Iu u / ∈ dom(I)
Γ ; Θ ⊢ (νu)P ⊲ ∆; I :NR where k ∈ dom(∆). Furthermore, we write ∆, k : α to abbreviate ∆, k : α, k : ⌊α⌋. That is, k : α describes both a session and its associated monitor.

Γ is a first-order environment which maps expressions to basic types and names to pairs of qualified session types. As motivated earlier, a session type is qualified with 'un' if it is associated to a unrestricted/persistent service; otherwise, it is qualified with 'lin'. The higher-order environment Θ collects assignments of typings to process variables and interfaces to locations. While the former concerns recursive processes, the latter concerns located processes. As we explain next, by relying on the combination of these two pieces of information the type system ensures that runtime adaptation actions preserve the behavioral interfaces of a process. We write vdom(Θ) = {X | X : I ∈ Θ} to denote the variables in the domain of Θ. Given these environments, a type judgment is of form Γ ; Θ ⊢ P ⊲ ∆; I meaning that, under environments Γ and Θ, process P has active sessions declared in ∆ and interface I. Selected typing rules are shown in Table 3; remaining rules can be found in Table 5 (Appendix A.3). Below we comment on some of the rules in Table 3: the rest are standard and/or self explanatory. Rule :A types update processes.

Notice that the typing rule ensures that each process Q i has exactly the same active sessions that those declared in the respective case. Also, we require that alternatives contain both processes and monitors. With I j ⊑ I we guarantee that the process behavior does not "exceed" the expected behavior within the location. Rule : takes care of subtyping both for typings ∆ and interfaces. Rule :CR types channel restriction that ensures typing duality among partners of a session and their respective queues. Typing of queues is given by rule :Q that simply assigns type k : ⌊α⌋ to queue k⌊α⌋. Finally, rule :NR types hiding of service names, by simply removing their declarations from the interface I of the process. In the rule, I u contains only declarations for u, i.e., ∀v = u, v / ∈ dom(I u ). Our type system enjoys the standard subject reduction property. We rely on balanced typings: ∆ is balanced iff for all κ p : α ∈ ∆ (resp. κ p : ⌊α⌋ ∈ ∆) then also κ p : β ∈ ∆ (resp. κ p : ⌊β⌋ ∈ ∆), with α ⊥ C β. The proof detailed in the Appendix, proceeds by induction on the last rule applied in the reduction; it adapts the one given in [START_REF] Giusto | Disciplined structured communications with disciplined runtime adaptation[END_REF].

Theorem 3.3 (Subject Reduction).

If Γ ; Θ ⊢ P ⊲∆; I with ∆ balanced and P -→ Q then Γ ; Θ ⊢ Q ⊲ ∆ ′ ; I ′ , for some I ′ and balanced ∆ ′ .

We now define and state safety and consistency properties. While safety guarantees adherence to prescribed session types and absence of runtime errors, consistency ensures that sessions are not jeopardized by careless runtime adaptation actions. Defining both properties requires the following notions of κ-processes, κ-redexes, and error process.

Definition 3.4 (κ-processes, κ-redexes, errors).

A process P is a κ-process if it is a prefixed process with subject κ p , i.e., P is one of the following:

κ p (x).P ′ κ p (v).P ′ close (κ p ).P ′ κ p ⊲ {n i :P i } i∈I κ p ⊳ n.P ′
Process P is a κ-redex if it contains the composition of exactly two κ-processes with opposing polarities. P is an

error if P ≡ (ν κ)(Q | R)
where, for some κ, Q contains either exactly two κ-processes that do not form a κ-redex or three or more κ-processes.

Informally, a process P is called consistent if whenever it has a κ-redex then update actions do not destroy such a redex. Below, we formalize this intuition. Let us write P -→ upd P ′ for any reduction inferred using rule :U . We then define: Definition 3.5 (Safety, Consistency). Let P be a process. We say P is safe if it never reduces into an error. We say P is update-consistent if and only if, for all P ′ and κ such that P -→ * P ′ and P ′ contains a κ-redex, if P ′ -→ upd P ′′ then P ′′ contains a κ-redex.

We now state our main result; it follows as a consequence of Theorem 3.3.

Theorem 3.6 (Typing Ensures Safety and Consistency).

If Γ ; Θ ⊢ P ⊲ ∆; I with ∆ balanced then program P is update consistent and safe.

Remark 3.7 (Asynchronous Communication).

We have focused on synchronous communication: this allows us to give a compact semantics, relying on a standard type structure. To account for asynchrony, we would require a runtime syntax for programs with queues for in-transit messages (values, sessions, labels). The type system must be extended to accommodate these new runtime processes. In our case, an extension with asynchrony would rely on the machinery defined in [START_REF] Kouzapas | A Study of Bisimulation Theory for Session Types[END_REF].

Discussion: A Compartmentalized Model of Communication and Adaptation

Given that the process model in § 2 enables the interplay of communication and adaptation, how can we organize specifications to reflect a desirable separation of concerns? In ongoing work, with the aim of specifying systems at a high-level of abstraction, we have developed a model which defines compartments to isolate communication behavior and adaptation routines. Here we briefly describe this model, which is given in Table 4.

In a nutshell, programs of § 2 are now organized into systems. A system G is the composition of a set of applications A 1 , . . . , A n each comprising three elements: a behavior R, a state S, and a manager M. As a simple example of a system, we may consider the operating system of a smartphone, which is meant to manage a number of applications that may interact among them. Applications in our model can communicate between each other or exhibit intra-application communication. The behavior R is specified as a process; we distinguish between located processes representing service definitions from located processes which make use of such definitions. A reduction semantics (omitted) ensures that locations enclosing service definitions do not contain open (active) sessions. This may be convenient for defining adaptation strategies, since updates to service definitions may now be performed without concerns of disruption of active sessions. The state S collects session monitors and location queues and it is kept separate from R. As a simple example, the buyer-seller scenario given in § 1 can be casted in our model as byr buyer u@slr(x : α).P ; S b ; M b slr seller * u(y:β).Q ; S s ; M s That is, buyer and seller are implemented as separate applications, named byr and slr, respectively. Above, we have S b = buyer⌊ǫ⌋ and S s = seller⌊ǫ⌋.

While the manager M implements adaptation at the application (local) level, a handler H defines adaptation at the system (global) level. As we wish to describe communication behavior separately from adaptation routines, update processes are confined to handlers and managers. A manager is meant to react upon the arrival of an internal adaptation message upd I . As in § 2, managers may act upon the issue of an internal update request upd I for some location, whereas handlers may act upon the arrival of an external update request or an application upgrade request (denoted upd E and upg, respectively). A handler may either update or upgrade the behavior at some location loc within application a; this is written loc@a. Upgrades are denoted l 1 P ; they are a particular form of update intended for service definitions only. In Table 4 we write * if e then P and * u(x:α).P as shorthands for persistent conditionals and services, respectively.

Our compartmentalized model induces specifications in which communication, runtime adaptation, and state (as in, e.g., asynchronous communication) are jointly expressed, while keeping a desirable separation of concerns. Notice that the differences between "plain" processes (as given in § 2) and systems (as defined in Table 4) are mostly conceptual, rather than technical. In fact, the higher level of abstraction that is enforced by our model does not result in additional technicalities. We conjecture that a reduction-preserving translation of application-based specifications into processes does not exist-a main difficulty being, unsurprisingly, properly representing the separation between behavior and state. This difference in terms of expressiveness does not appear

G ::= A | H | (νκ)A | G1 G2 | 0 A ::= a R ; S ; M H ::= * if arrive(l1@a, upd E ) then l1 case x of {(x 1 :β i 1 ; • • • ; x m :β i m ) : Qi}i∈I | * if arrive(l1@a, upg) then l1 P R ::= loc u(x:α).P | loc * u(x:α).P | loc P -| R1 | R2 S ::= κ p ⌊α⌋ | loc⌊ r⌋ | S1 ⋄ S2 | 0 M ::= * if arrive(l1, upd I ) then l1 case x of {(x 1 :β i 1 ; • • • ; x m :β i m ) : Qi}i∈I | M1 • M2 | 0 Table 4. A Compartmentalized Model of Communicating Systems: Syntax.
to affect the type system. In future work we plan to extend the typing discipline in § 3 (and its associated safety and consistency guarantees) to systems.

Related Work and Concluding Remarks

Related Work. The combination of static typing and type-directed tests for dynamic reconfiguration is not new. For instance, Seco and Caires [START_REF] Seco | Types for dynamic reconfiguration[END_REF] study this combination for a calculus for object-oriented component programming. To the best of our knowledge, ours is the first work to develop this combination for a session process language. As already discussed, we build upon constructs proposed in [START_REF] Hu | Type-safe eventful sessions in java[END_REF][START_REF] Kouzapas | On asynchronous session semantics[END_REF][START_REF] Kouzapas | On asynchronous eventful session semantics[END_REF][START_REF] Kouzapas | A Study of Bisimulation Theory for Session Types[END_REF]. The earliest works on eventful sessions, covering theory and implementation issues, are [START_REF] Hu | Type-safe eventful sessions in java[END_REF][START_REF] Kouzapas | On asynchronous session semantics[END_REF]. Kouzapas's PhD thesis [START_REF] Kouzapas | A Study of Bisimulation Theory for Session Types[END_REF] provides a unified presentation of the eventful framework, with case studies including event selectors (a building block in event-driven systems) and transformations between multithreaded and event-driven programs. At the level of types, the work in [START_REF] Kouzapas | A Study of Bisimulation Theory for Session Types[END_REF] introduces session set types to support the typecase construct. We use dynamic session type inspection only for runtime adaptation; in [START_REF] Kouzapas | A Study of Bisimulation Theory for Session Types[END_REF] typecase is part of the process syntax. This choice enables us to retain a standard session type syntax. Runtime adaptation of session typed processes-the main contribution of this paper-seems to be an application of eventful session types not previously identified. Previous works on runtime adaptation for session types (binary and multiparty) include [START_REF] Giusto | Disciplined structured communications with disciplined runtime adaptation[END_REF]1,3]. We have already commented on how our current approach enhances that in our previous work [START_REF] Giusto | Disciplined structured communications with disciplined runtime adaptation[END_REF]. Both [1] and [3] study adaptation for multiparty communications, which already sets a substantial difference with respect to our work. In [3], a set of monitors which govern the behavior of participants are derived from a global specification. Self-adaptation for monitored processes is triggered by an external adaptation function, which is often left unspecified. As in our work, the operational semantics for adaptation in [3] uses (local) types and monitors; key differences include the use of type-directed checks for selecting adaptation routines that preserve consistency, and the use of events and queues to handle adaptation requests. The work [1] studies dynamic update for message passing programs; a form of consistency for updates over threads is ensured using multiparty session types, following an asynchronous communication discipline.

Concluding Remarks.

Building upon [START_REF] Kouzapas | A Study of Bisimulation Theory for Session Types[END_REF], we have introduced an eventful approach to runtime adaptation of session typed processes. We identified the strictly necessary eventful process constructs that enhance and refine known mechanisms for runtime adaptation. Adaptation requests, both internal and external, are handled via event detectors and queues associated to locations. Our approach enables us to specify rich forms of updates on locations with running sessions; this represents a concrete improvement with respect to previous works [START_REF] Giusto | Disciplined structured communications with disciplined runtime adaptation[END_REF]. We notice that expressing both internal and external exceptional events is useful in practice; for instance, both kinds of events coexist in BPMN 2.0 (see, e.g., [START_REF] Dumas | Fundamentals of Business Process Management[END_REF]Chap.4]). To rule out update steps that jeopardize running session protocols, we also introduced a type system that ensures communication safety and update consistency for session programs. We have also outlined a high-level model of structured interaction which organizes communication and adaptation components into a sensible structure.

Adaptation in our framework is "monotonic" or "incremental" in that changes always preserve/extend active session protocols, exploiting subtyping for enhanced flexibility. Interestingly, our framework can be modified so that arbitrary protocols are installed as a result of an update. One needs to ensure that the endpoints of a session are present in the same location: arbitrary updates are safe as long as both endpoints are simultaneously updated with dual protocols. To relax our framework in this way, we would need to modify definitions for session matching (Def. 2.1) and interface ordering (Def. 3.2).

In future work, we plan to further validate the constructs in our framework by revisiting the model of supervision trees (a mechanism for fault-tolerance in Erlang) that we gave in [4]. Other interesting topics for further development include accounting for asynchronous communication (cf. Remark 3.7) and extending our event-based approach to choreographic protocols; the framework in [3] may provide a good starting point.

5.

If unfold(T ) =?(τ 1 , . . . , τ n ).T 1 then unfold(S) =?(σ 1 , . . . , σ n ).S 1 then for all i ∈ [1.

.n], we have that (T 1 , S 1 ) ∈ R and τ i ≤ C σ i and σ i ≤ C τ i . 6. If unfold(T ) =!(τ 1 , . . . , τ n ).T 1 then unfold(S) =?(σ 1 , . . . , σ n ).S 1 then for all i ∈ [1.

.n], we have that (T 1 , S 1 ) ∈ R and

τ i ≤ C σ i and σ i ≤ C τ i . 7. If unfold(T ) = &{n 1 : T 1 . . . n m : T m } then unfold(S) = ⊕{n 1 : S 1 . . . n m :
S m } and for all i ∈ [1.

.m], we have that

(T i , S i ) ∈ R. 8. If unfold(T ) = ⊕{n 1 : T 1 . . . n m : T m } then unfold(S) = &{n 1 : S 1 . . . n m :
S m } and for all i ∈ [1.

.m], we have that (T i , S i ) ∈ R.

Definition A.3. A relation R ⊆ T × T is a type simulation if (T, S) ∈ R implies the following conditions: 1. If unfold(T ) = τ then unfold(S) = σ and τ ≤ B σ. 2. If unfold(T ) = ε then unfold(S) = ε. 3. If unfold(T ) =?(T 2 ).T 1 then unfold(S) =?(S 2 ).S 1 and (T 1 , S 1 ) ∈ R and (T 2 , S 2 ) ∈ R. 4. If unfold(T ) = !(T 2 ).T 1 then unfold(S) = !(S 2 ).S 1 and (T 1 , S 1 ) ∈ R and (S 2 , T 2 ) ∈ R. 5. If unfold(T ) =?(τ 1 , . . . , τ n ).T 1 then unfold(S) =?(σ 1 , . . . , σ n ).S 1 then for all i ∈ [1..n], we have that (τ i , σ i ) ∈ R and (T 1 , S 1 ) ∈ R. 6. If unfold(T ) =!(τ 1 , . . . , τ n ).T 1 then unfold(S) =!(σ 1 , . . . , σ n ).S 1 then for all i ∈ [1.
.n], we have that (σ i , τ i ) ∈ R and (T 1 , S 1 ) ∈ R. 7. If unfold(T ) = ⊕{n i : T i } i∈I then unfold(S) = ⊕{n j : S j } j∈J and I ⊆ J for all i ∈ I, we have that (T i , S i ) ∈ R. 8. If unfold(T ) = &{n i : T i } i∈I then unfold(S) = &{n j : S k } j∈J and J ⊆ I for all j ∈ J, we have that (T j , S j ) ∈ R. The extension of ≤ C to typings, written ∆ ≤ C ∆ ′ , arises as expected.

A.3 Additional Typing Rules

Table 5 gives additional typing rules for the system in § 3.

B Omitted Proofs

The following auxiliary result concerns substitutions for channels, expressions, and process variables. Observe how the case of process variables has been relaxed so as to allow substitution with a process with "smaller" interface (in the sense of ⊑). This extra flexibility is in line with the typing rule for located processes (rule :L ), and will be useful later on in proofs.

Γ ⊢ true, false ⊲ bool : Γ ⊢ u ⊲ name : As reduction may occur inside contexts, in proofs it is useful to have typed contexts. These are contexts in which the hole has associated typing information-concretely, the typing for processes which may fill in the hole. Defining context requires a simple extension of judgments, in the following way: Proof. By induction on the last rule applied in the reduction. We assume that e ↓ c is a type preserving operation, for every e. We examine only a few interesting cases, namely those for session establishment, runtime update, and intra-session communication; remaining cases are similar or simpler.

Γ, x : bool ⊢ x ⊲ bool : V Γ, x : name ⊢ x ⊲ name : V d = u ∨ d = κ p ∨ d = x Γ ⊢ d = d ⊲ bool : α ⊥C β Γ, u : αq, βq ⊢ u ⊲ αq, βq :S Γ ; Θ ⊢ 0 ⊲ ∅; ∅ :N Γ ; Θ ⊢ P ⊲ ∆, k : β; I Γ ; Θ ⊢ k(k ′ ).P ⊲ ∆, k :!(α).β, k ′ : α; I :T Γ ; Θ ⊢ P ⊲ ∆, k : β, x : α; I Γ ; Θ ⊢ P1 ⊲ ∆, k : α1; I1 • • • Γ ; Θ ⊢ Pm ⊲ ∆, k : αm; Im I = I1 ⊎ ... ⊎ Im Γ ; Θ ⊢ k ⊲ {n1:P1 []
Proof. Safety is a direct consequence of Theorem 3.3. For consistency, we assume, towards a contradiction, that there exist P 1 , P 2 , and κ 1 such that 1. P -→ * P 1 , 2. P 1 has a κ 1 -redex, 3. P 1 -→ upd P 2 , and 4. P 2 does not have a κ 1 -redex.

Without loss of generality, we suppose that the reduction P 1 -→ upd P 2 is due to a synchronization on location l 1 ∈ Θ. Since the κ 1 -redex is destroyed by the update action from P 1 to P 2 , the κ 1 -redex in P 1 must necessarily be a located κ 1 -redex, i.e., in P 1 , one or both κ 1 -processes are contained inside l 1 . Now, our reduction semantics (rule :U ) decrees that for such an update action to be enabled, the type of the process located in l 1 must be preserved. We also know, by Theorem 3.3 (Subject Reduction), that P 1 is well-typed under a balanced typing ∆ 1 . Hence, update steps which destroy a κ-redex (located and unlocated) can never be enabled from a well-typed process with a balanced typing (such as P ) nor from any of its derivatives (such as P 1 ). We thus conclude that well-typedness implies update consistency.

⊓ ⊔

C A Compartmentalized Model of Communication and Adaptation: extended discussion

Given that the process model in § 2 describes the interplay of both communication and adaptation concerns, how should specifications be organized in order to reflect a desirable separation of concerns? Here we propose to organize specifications using compartments which isolate communication behavior and adaptation routines. Our model offers an alternative for specifying systems at a high-level of abstraction. It defines systems in a two-level scheme: from a global perspective, a system is the composition of applications. There are handler processes, which are responsible for adaptation at the system (global) level: a handler may update a location at some specific application or upgrade a service definition. Applications comprise three elements: behavior, state, and a manager. While the first concerns session processes, the second comprises monitors and location queues. Managers implement adaptation policies at the application (local) level. As we wish to isolate communication behavior from adaptation routines, the presence of update processes is confined to handlers and managers.

Our model of compartmentalized communication is defined in Table 4. The process syntax that we use in this section is a subset of that introduced in Table 1:

P, Q ::= u@a(x : α).P | u(x : α).P | loc@a(r) | k(e).P | k(x).P | k ⊳ n; P | k ⊲ {n 1 :P 1 [] • • • [] n m :P m } | close (k).P | µX .P | X | if e then P else Q | P | P | (νκ)P | (νa)P | 0
Our set of processes is thus comparable to most session π-calculi, only extended with the (possibly remote) adaptation request loc@a(r), which refers to location loc in application a. Similarly, our notation for session requests refers to a service u at application a.

We shall write * if e then P to stand for µX .if e then P else X , and * u(x:α).P to stand for

:LU fc(P ) = {κ p 1 , . . . , κ p m } S ≡ S1 ⋄ κ p 1 ⌊α1⌋ ⋄ • • • ⋄ κ p m ⌊αm⌋ ⋄ S2 (V = P ∧ S ′ = S) ∃l. matchI (l, {α1, . . . , αm}, {β i 1 , . . . , β i m }i∈I ) ∧ V = Q l [ κ p 1 , . . . , κ p m/ x1, . . . , xm] ∧ S ′ = S1 ⋄ κ p 1 ⌊β1⌋ ⋄ • • • ⋄ κ p m ⌊βm⌋ ⋄ S2 a l1 P | R ; S ; M | l1 case x of {(x 1 :β i 1 ; • • • ; x m :β i m ) : Qi}i∈I -→ a l1 V | R ; S ′ ; M | 0 Table 6.
Reduction Rule for Managers in the Compartmentalized Model µX .u(x:α).(P | X ). Also, we write P -to denote the sublanguage of processes without service definitions u(x:α).P .

A system G is the composition of finite sets of applications A and handlers H; this composition is denoted . Given A i = a i R i ; S i ; M i , we refer to a i as the name of A i . A handler is a persistent process which spawns an adaptation strategy as soon as a request arrives to an appropriate queue. Handlers may either update or upgrade the behavior at some location loc within application a; this is written loc@a. Upgrades are denoted l 1 P ; they are a particular form of update intended for service definitions only. We use R to denote the communication behavior of an application. As before, locations are transparent; for simplicity, here we rule out their nesting. We distinguish between located processes representing service definitions from the located processes which make use of such definitions. Our operational semantics (motivated below) ensures that locations enclosing service definitions do not contain open (active) sessions. This may be convenient for organizing adaptation strategies, since updates to service definitions may now be performed without concerns of disruption of active sessions. The state S of an application collects session monitors and location queues. A manager M is meant to react upon the arrival of an internal adaptation message upd I . We use S 1 ⋄ S 2 and M 1 • M 2 to denote the composition of S 1 and S 2 and M 1 and M 2 , respectively. Appendix D illustrates the use of compartments in the buyer-seller example.

Even if the syntax in Table 4 already induces useful structuring principles for systems, we find it desirable to give the following well-formedness conditions. Recall that we write P 1 ∈ P if P 1 occurs in P . First, all applications in G should have pairwise distinct names. Second, for each a i R i ; S i ; M i ∈ G, we have: (a) Processes in M i only refer to locations occurring in R i . (b) For each location loc j occurring in R i there is exactly one queue loc j ⌊ r⌋ ∈ S i . We now comment on the reduction semantics for well-formed systems. We illustrate how such a semantics builds upon the principles embodied by the semantics for "plain" processes (cf. § 2) but propagating the structural organization introduced above.

Our semantics enables remote session establishment in which a request for service u in application a 2 is served by a definition in application a 1 (below we assume α ⊥ C β):

a 1 l 1 u(x:α).P | R ; S 1 ; M 1 a 2 l 2 u@a 1 (y:β).Q ; S 2 ; M 2 -→ (νκ) a 1 l 1 R ; S 1 ; M 1 a 2 l 2 (P [ κ + /x] | Q[ κ - /y]) ; S 2 ⋄ κ + ⌊α⌋ ⋄ κ -⌊β⌋ ; M 2
Above, it is worth observing how the instance of the service is deployed at the caller location (denoted l 2 ). Since we would like to impose a certain degree of isolation between applications, this will be the only rule admitted at the application level. Local session establishment takes place between services and clients inside a certain application a: a l 1 u(x:α).P | R | l 2 u(y : β).Q ; S 1 ; M 1 -→

(νκ) a l 1 R | l 2 P [ κ + /x] | Q[ κ - /y] ; S 1 ⋄ κ + ⌊α⌋ ⋄ κ -⌊β⌋ ; M 1
Here again the instantiated service "moves" from l 1 to l 2 . Let us consider rules for adaptation. At the application level, the semantics of managers relies on rule :LU , given in Table 6. Such a rule strictly refines rule :U in Table 2. Observe how having the state S allows us to precisely specify the elements that have influence on (and are modified by) dynamic reconfiguration. At the level of systems, the semantics of handlers is given by two rules: one for update (similar to the rule above) and the following rule for service upgrade:

a l 1 P | R ; S ; M l 1 Q -→ a l 1 Q | R ; S ; M 0
Tables 7 and8 show some of the reduction rules for systems G, denoted -→. For all entities (processes, managers, applications, etc.) we assume a structural congruence relation ≡ that validates the usual properties for their associated parallel composition operator, with neutral element 0. Similarly as process reduction, -→ relies on an evaluation relation on expressions, denoted e ↓ v (where v is a value). Also, it relies on the definition of evaluation contexts E[-] given before. Furthermore, we assume a rule :GU which is very similar to :LU . Our model induces specifications in which requirements of communication, runtime adaptation, and state (as useful in, e.g., asynchronous communication) are jointly expressed, while keeping a desirable separation of concerns. Notice that the differences between "plain" processes (as given in § 2) and well-formed systems are mostly conceptual, rather than technical. In fact, the higher level of abstraction that is enforced by well-formed systems does not result in additional technicalities. Although our compartmentalized model builds upon plain processes, we conjecture that a reduction-preserving translation of application-based specifications into processes does not exist-a main difficulty being, unsurprisingly, properly representing the separation between behavior and state. This difference in terms of expressiveness does not appear to affect the type system. We are confident that the typing discipline developed in § 3 (and its associated guarantees) extend to well-formed systems without major technical difficulties. We plan to address this conjecture in future work.

D An Example of the Compartmentalized Model

We now illustrate how the buyer-seller scenario discussed in the Introduction can be casted in the compartmentalized model given in § C. Buyer B and seller S are implemented as two separate applications, named byr and slr, respectively: Notice that the service offered by S is given as a service definition. Since applications are intended to be distributed containers of communication behavior, we slightly reformulate the adaptation discussed in the Introduction as follows. We will assume that the seller may receive an update request from its environment. Upon reception of such a request, its associated handler H s will not only spawn an update process but will also issue an adaptation request for the buyer. From the perspective of the buyer such a request is internal, for it comes from the seller. That is, the seller acts an an intermediate manager for the buyer. As soon as the buyer receives the internal request, its (local) manager M b may spawn an update process at the local level. More precisely, letting g s = arrive(seller@slr, upd E ) and g b = arrive(buyer, upd I ), we have:

  α, β ::= ?(T ).β input a value of type T , continue as β | !(T ).β output a value of type T , continue as β | &{n 1 :α 1 . . . n m :α m } branching (external choice) | ⊕{n 1 :α 1 . . . n m :α m } selection (internal choice) | ε | µt.α | t terminated and recursive session

Definition 3 . 2 (

 32 Interface Ordering). Given interfaces I and I ′ , we write I ⊑ I ′ iff 1. ∀(lin a:α) such that # I lin (lin a:α) = h with h > 0, then one of the following holds:(a) there exist h distinct elements (lin a:β i ) ∈ I ′ lin such that α ≤ C β i for i ∈ [1..h]; (b) there exists (un a:β) ∈ I ′ un such that α ≤ C β. 2. ∀(un a:α) ∈ I un then (un a:β) ∈ I ′ un and α ≤ C β, for some β.

Definition A. 4 .-

 4 Let T, S be types. The coinductive duality relation, denoted ⊥ C , is defined by T ⊥ C S if and only if there exists a duality relation R such that (T, S) ∈ R. -The coinductive subtyping relation, denoted ≤ C , is defined by T ≤ C S if and only if there exists a type simulation S such that (T, S) ∈ S.

Lemma B. 1 (

 1 Substitution Lemma). 1. If Γ ; Θ ⊢ P ⊲ ∆, x : α; I then Γ ; Θ ⊢ P [ κ p /x] ⊲ ∆, κ p : α; I 2. If Γ, x : τ ; Θ ⊢ P ⊲ ∆; I and Γ ⊢ e ⊲ τ then Γ ; Θ ⊢ P [ e /x] ⊲ ∆; I. Proof. Easily shown by induction on the structure of P .

HTheorem ( 3 . 3

 33 ; Γ ; Θ ⊢ C ⊲ ∆; I Intuitively, H contains the description of the type associated to the hole in C. Typing rules are extended in the expected way. Because contexts have a single hole, H is either empty of has exactly one element. When H is empty, we write Γ ; Θ ⊢ P ⊲ ∆; I instead of • ; Γ ; Θ ⊢ P ⊲ ∆; I. Two additional typing rules are required::H • Γ ;Θ⊢∆;I ; Γ ; Θ ⊢ • ⊲ ∆; I :F • Γ ;Θ⊢∆;I ; Γ ; Θ ⊢ C ⊲ ∆ 1 ; I 1 Γ ; Θ ⊢ P ⊲ ∆; I Γ ; Θ ⊢ C{P } ⊲ ∆ 1 ; I 1Axiom :H allows us to introduce typed holes into contexts. In rule :F , P is a process (it does not have any holes), and C is a context with a hole of type Γ ; Θ ⊢ ∆; I. The substitution of occurrences of • in C with P , noted C{P } is sound as long as the typings of P coincide with those declared in H for C. We introduce some convenient notation for typed holes. Notation B.2 Let us use S, S ′ , . . . to range over judgments attached to typed holes. This way, • S denotes the valid typed hole associated to S = Γ ; Θ ⊢ ∆; I. Lemma B.3. Let P and C be a process and a typed context such thatΓ ; Θ ⊢ C{P } ⊲ ∆; I is a derivable judgment. There exist ∆ 1 , I 1 such that (i) Γ ; Θ ⊢ P ⊲ ∆ 1 ; I 1 is a welltyped process, and (ii) ∆ 1 ⊆ ∆ and I 1 ⊑ I. Lemma B.4. Let C be a context. Suppose • S ; Γ ; Θ ⊢ C ⊲ ∆ C ∪ ∆ S ; I C ⊎ I S with S = Γ ; Θ ⊢ ∆ S ; I S is well-typed. Let S ′ = Γ ; Θ ⊢ ∆ S ′ ; I S ′ . Then • S ′ ; Γ ; Θ ⊢ C ⊲ ∆ C ∪ ∆ S ′ ; I C ⊎ I S ′is a derivable judgment. Theorem B.5 (Subject Congruence). If Γ ; Θ ⊢ P ⊲ ∆; I and P ≡ Q then Γ ; Θ ⊢ Q ⊲ ∆; I.Proof. The proof proceeds by induction on the derivation of P ≡ Q, with a case analysis on the last applied rule. ⊓ ⊔ Subject Reduction). If Γ ; Θ ⊢ P ⊲ ∆; I with ∆ balanced and P -→ Q then Γ ; Θ ⊢ Q ⊲ ∆ ′ ; I ′ , for some I ′ and balanced ∆ ′ .

Table 7 .

 7 sys ::= byr R b ; S b ; M b slr R s ; S s ; M s H s R b ::= buyer u@slr(x : α).P 50 x S b ::= buyer⌊ǫ⌋ R s ::= seller * u(y:β).Q y S s ::= seller⌊ǫ⌋:RO a1 l1 u(x:α).P | R ; S1 ; M1 a2 l2 u@a1(y:β).Q ; S2 ; M2 -→ (νκ) a1 l1 R ; S1 ; M1 a2 l2 (P [ κ + /x] | Q[ κ - /y]) ; S2 ⋄ κ + ⌊α⌋ ⋄ κ -⌊β⌋ ; M2 :LO a1 l1 u(x : α).P | R | l2 u(y : β).Q ; S1 ; M1 -→ (νκ) a1 l1 R | l2 P [ κ + /x] | Q[ κ - /y] ; S1 ⋄ κ + ⌊α⌋ ⋄ κ -⌊β⌋ ; M1 :C a l1 κ p (v).P | κ p (x).Q ; S ⋄ κ p ⌊!(T ).α⌋ ⋄ κ p ⌊?(T ).β⌋ ; M -→ a l1 P | Q[ v /x] ; S ⋄ κ p ⌊α⌋ ⋄ κ p ⌊β⌋ ; M :S a l1 κ p ⊲ {nj:Pj}j∈J | κ p ⊳ nj; Q ; S ⋄ κ p ⌊&{nj:αj}j∈J ⌋ ⋄ κ p ⌊⊕{nj : βj}j∈J ⌋ ; M -→ a l1 Pj | Q ; S ⋄ κ p ⌊αj⌋ ⋄ κ p ⌊βj⌋ ; M (j ∈ J) :C a l1 close (κ p ).P | close (κ p ).Q ; S ⋄ κ p ⌊ε⌋ ⋄ κ p ⌊ε⌋ ; M -→ a l1 P | Q ; S ; M :LU fc(P ) = {κ p 1 , . . . , κ p m } S ≡ S1 ⋄ κ p 1 ⌊α1⌋ ⋄ • • • ⋄ κ p m ⌊αm⌋ ⋄ S2 (V = P ∧ S ′ = S) ∃l. matchI (l, {α1, . . . , αm}, {β i 1 , . . . , β i m }i∈I ) ∧ V = Q l [ κ p 1 , . . . , κ p m/ x1, . . . , xm] ∧ S ′ = S1 ⋄ κ p 1 ⌊β1⌋ ⋄ • • • ⋄ κ p m ⌊βm⌋ ⋄ S2 a l1 P | R ; S ; M | l1 case x of {(x 1 :β i 1 ; • • • ; x m :β i m ) : Qi}i∈I -→ a l1 V | R ; S ′ ; M | 0 :GU fc(P ) = ∅ a l1 P | R ; S ; M l1 Q -→ a l1 Q | R ; S ; M0Selected Reduction Rules for Compartmentalized Processes (I). We assume α ⊥C β.

2 The Process Model: Syntax and Semantics

		channel / name hiding / conditional
	| k⌊α⌋	session monitor
	| loc[P ]	located process
	Syntax. We rely on base sets for names, ranged over by u, a, b . . .; (session) channels,
	ranged over by k, κ p , . . ., with polarity p ∈ {+, -}; labels, ranged over by n, n ′ , . . .; and

e ::= v | x, y, z | k = k | a = a expressions | arrive(loc, r) arrival predicate P ::= u(x : α).P | u(x : α).P | close (k).P session request / acceptance / closure | k(e).P | k(x).P data output /input | k ⊳ n; P | k ⊲ {ni:Pi}i∈I selection / branching | µX .P | X recursion / rec. variable | P | P | 0 parallel composition / inaction | (νκ)P | (νu)P | if e then P else Q

Table 1 .

 1 Process Syntax. Above, annotation α denotes a session type.

Table 2 .

 2 Reduction

Semantics: Full Set of Rules. Above, α and β denote session types.

Table 3 .

 3 Well-Typed Processes: Selected Rules.

Table 5 .

 5 • • • [] nm:Pm} ⊲ ∆, k : &{n1:α1, . . . , nm:αm}; I :B Additional Typing Rules.

Γ ; Θ ⊢ P ⊲ ∆, k : αi; I 1 ≤ i ≤ m Γ ; Θ ⊢ k ⊳ ni; P ⊲ ∆, k : ⊕{n1 : α1, .

. . , nm : αm}; I :S

Θ ⊢ loc ⊲ I Γ ; Θ ⊢ P ⊲ ∆;I ′ I ′ ⊑ I Γ ; Θ ⊢ loc[P ] ⊲ ∆; I ′ :L Γ ⊢ r ⊲ msg Γ ; Θ ⊢ loc⌊ r⌋ ⊲ ∅; ∅ :QL α ⊥C β Γ ⊢ u ⊲ α lin , β lin γ ≤C α Γ ; Θ ⊢ P ⊲ ∆, x : γ; I Γ ; Θ ⊢ u(x : γ).P ⊲ ∆; I ⊎ u : γ lin :A α ⊥C β Γ ⊢ u ⊲ αq, β lin γ ≤C β Γ ; Θ ⊢ P ⊲ ∆, x : γ; I Γ ; Θ ⊢ u(x : γ).P ⊲ ∆; I ⊎ u : γ lin :R Γ ; Θ ⊢ P ⊲ ∆; I k / ∈ dom(∆) Γ ; Θ ⊢ close (k).P ⊲ ∆, k : ε; I :C Γ ; Θ ⊢ P ⊲ ∆1; I1 Γ ; Θ ⊢ Q ⊲ ∆2; I2 Γ ; Θ ⊢ P | Q ⊲ ∆1 ∪ ∆2; I1 ⊎ I2 :P Θ ⊢ loc ⊲ I ∀j ∈ J, fv(Qj) \ {x1, . . . , xm} = ∅ Γ ; Θ ⊢ Qj ⊲ x1: β j 1 ; • • • ; xm: β j m ; Ij Ij ⊑ I Γ ; Θ ⊢ loc case x of {(x 1 :β j 1 ; • • • ; x m :β j m ) : Qj}j∈J ⊲ ∅; ∅ :A Γ ; Θ ⊢ P ⊲ ∆,κ p : α1 , κ p : α2 ; I α1 ⊥C α2 Γ ; Θ ⊢ (νκ)P ⊲ ∆; I :CR

Γ ; Θ ⊢ k(x).P ⊲ ∆, k :?(α).β; I :C Γ, x : τ ; Θ ⊢ P ⊲ ∆, k : α; I Γ ; Θ ⊢ k(x).P ⊲ ∆, k :?(τ ).α; I :I Γ ; Θ ⊢ P ⊲ ∆, k : α; I Γ ⊢ e ⊲ τ Γ ; Θ ⊢ k(e).P ⊲ ∆, k :!(τ ).α; I :O Γ ; Θ ⊢ P ⊲ ∆; I κ + , κ -/ ∈ dom(∆) Γ ; Θ ⊢ (νκ)P ⊲ ∆; I :W Γ ; Θ ⊢ P ⊲ ∆; I u / ∈ dom(I) Γ ; Θ ⊢ (νu)P ⊲ ∆; I :W Γ ; Θ ⊢ e ⊲ bool Γ ; Θ ⊢ P ⊲ ∆; I Γ ; Θ ⊢ Q ⊲ ∆; I Γ ; Θ ⊢ if e then P else Q ⊲ ∆; I :I

Acknowledgments. We are grateful to Ilaria Castellani, Mariangiola Dezani-Ciancaglini, and the anonymous reviewers for useful remarks. This research was partially supported by COST Action IC1201: Behavioural Types for Reliable Large-Scale Software Systems.

A Supplementary Definitions

A.1 Structural Congruence Definition A.1 (Structural Congruence).

Structural congruence is the smallest congruence relation on processes that is generated by the following laws:

(νs)loc[P ] ≡ loc[(νs)P ] with s, s ′ , . . . ranges over both names and session channels. The extension of ≡ to contexts is as expected.

A.2 Coinductive Subtyping and Duality

For all types, define unfold(T ) by recursion on the structure of T : unfold(µt.T ) = unfold(T [ µt.T /t])

and unfold(T ) = T otherwise. The following definitions are used by Definition A. 4. Given an index set I = {1, . . . , m}, we use &{n i : T i } i∈I and ⊕{n i : T i } i∈I to abbreviate &{n 1 : T 1 , . . . , n m : T m } and ⊕{n 1 : T 1 , . . . , n m : T m }, respectively.

Definition A.2. A relation R ⊆ T × T is a duality relation if (T, S) ∈ R implies the following conditions:

Case :O From Table 2 we have:

By assumption Γ ; Θ ⊢ C{u(x : α).P 1 } | D{u(y : β).P 2 } ⊲ ∆; I with balanced ∆. Then, by inversion on typing, using rules :A , :R , and :P we infer there exist ∆ ′ , I ′ such that

where, letting 4) is as follows:

with

Then, subtree ( 6) is as follows:

with

By Lemma B.3 we have that ∆ 1 ⊆ ∆ ′ 1 and ∆ 2 ⊆ ∆ ′ 2 . We also infer I 1 ⊑ I ′ 1 , I 2 ⊑ I ′ 2 , and I ′ ⊑ I. Now, using Lemma B.1(1) on judgments for P 1 and P 2 , we obtain:

We may now reconstruct the derivation given in (4) using Lemma B.4 and rule :P :

and

For D, we proceed analogously from ( 6) and infer:

with

We may finally derive the type for the result of the reduction: using rules :P and :CR we obtain:

(8) ( 11)

This concludes this case.

Case :U

From Table 2 we have:

By assumption we have

with ∆ balanced. Then, by inversion on typing, using rules :F , :P , :A , and :L we infer: 14) is as follows:

with S 1 = Γ ; Θ ⊢ ∆ 1 ; I 1 , and I 1 ⊑ I ′ 1 (by Lemma B.3). Subtree (15) is as follows:

(15) with S 2 = Γ ; Θ ⊢ ∅; ∅. We now consider the two cases for V and reconstruct the derivation after the reduction, using rules :P , :F and Lemma B.4. The case for V = P is trivial as everything is left unchanged and thus

By derivation (15) we know that

thus applying Lemma B.1(1) we have:

(17) Case :I/O From Table 2 we have:

By assumption, we have Γ ; Θ ⊢ C κ p (v).P 1 | κ p ⌊!(τ ).α⌋ | D κ p (x).P 2 | κ p ⌊?(τ ).β⌋ ⊲ ∆; I, with ∆ balanced. By inversion on typing, using rules :F , :P , :I , and :O , we infer:

where:

.α, κ p : ⌊!(τ ).α⌋, κ p :?(τ ).β, κ p : ⌊?(τ ).β⌋ (18)

We have that subtree (20) is as follows:

(21)

and

Similarly, for subtree (22) we obtain (we show only the last step of the derivation):

(23) Γ ; Θ ⊢ κ p (x).P 2 | κ p ⌊?(τ ).β⌋ ⊲ ∆ 2 , κ p :?(τ ).β, κ p : ⌊?(τ ).β⌋;

and 4(3) and rules :P and :F we obtain the following type derivations:

Since by inductive hypothesis ∆ ′ 1 and ∆ ′ 2 are balanced, we infer that ∆ ′ 1 ∪ ∆ ′ 2 , κ p : α, κ p : β is balanced as well; this concludes the proof for this case.

⊓ ⊔

Theorem (3.6 Typing Ensures Safety and Consistency).

If Γ ; Θ ⊢ P ⊲ ∆; I with ∆ balanced then P is update consistent and safe.