Cooperative decoupled processes

Abstract

Event-driven programming has become a major paradigm in developing concurrent, distributed systems. Its benefits are often informally captured by the key tenet of “decoupling,” a notion which roughly captures the ability of processes to join and leave (or fail) applications dynamically, and to be developed by independent parties. Programming models for event-driven programming either make it hard to globally reason about control flow, thus hampering sound execution, or sacrifice decoupling to aid in reasoning about control flow. This work fills the gap by introducing a programming model—dubbed cooperative decoupled processes—that achieves both decoupling and global reasoning about control flow. We introduce this programming model through an event calculus, loosely inspired by the Join calculus, that enables reasoning about cooperative decoupled processes through the concepts of pre- and postconditions. A linear type system controls aliasing of events to avoid a break of control flow and thus safe exchange of shared events. Fundamental properties of the type system such as subject reduction, migration safety, and progress are established.

1 Introduction

Events representing happenings such as sensor readings, communication actions, or state changes in software components have long been used for driving interactions in concurrent (Pnueli 1977) and distributed (Lamport 1978) systems. Ever since the advent of concurrent operating systems and interrupts, events (and event handlers respectively) have also served as a programming abstraction. In the last decade, event-driven programming (see Adya et al. 2002; Bolosky et al. 2000; Cunningham and Kohler 2005; Desai et al. 2013; Floyd et al. 1997; Ousterhout 1996; Franklin and Zdonik1997; Welsh et al. 2001; Shih et al. 2002; Gustafsson 2005; Haller and Odersky 2006, 2009; Li and Zdancewic 2007; Foltzer et al. 2012) has become a major paradigm for developing distributed systems. Garcia et al. (2013) show the 20-fold increase of the licenses for so-called “messaging” middleware systems.

Modularity

Event-driven systems are organized as collections of decoupled concurrent processes that communicate through shared events. Decoupling, as presented in Courtenage (2002), Hinze and Voisard (2002), Sánchez et al. (2003), Gasiunas et al. (2011), Eugster et al. (2003), Benton et al. (2004), and Haller and Cutsem (2008) and Ham et al. (2014), is a key tenet in advocating for event-driven over point-to-point, synchronous interaction. Decoupling is desired in terms of both development-time and runtime characteristics. It enables processes to be developed independently, e.g., without being explicitly bound to other processes, adding new process instances at runtime, or continue operating as existing process instances fail or are removed. However, one cannot just throw together processes that were independently developed. At the least, they need to agree on the content of the events they exchange to accomplish some common goal.

Global reasoning about control flow

Straightforward decoupling makes it hard to globally reason about control flow of event-driven processes because (1) shared events as a means of communication leads to competing recipients (Chin and Millstein 2006) and (2) structuring processes as collections of event handlers leads to the problem of stack management (von Behren et al. 2003) as interaction logic is fragmented across multiple event handlers. This has led to the emergence of a family of event-driven systems (see Adya et al. 2002; Bolosky et al. 2000; Cunningham and Kohler 2005; Ousterhout 1996; Welsh et al. 2001; Shih et al. 2002; Gustafsson 2005; Haller and Odersky 2006, 2009; Li and Zdancewic 2007; Foltzer et al. 2012) that address these challenges by either using “call-return” (see Adya et al. 2002; Bolosky et al. 2000; Cunningham and Kohler 2005; Ousterhout 1996; Welsh et al. 2001) or coroutine primitives (see Shih et al. 2002; Gustafsson 2005; Haller and Odersky 2006, 2009; Li and Zdancewic 2007; Foltzer et al. 2012). Both approaches sacrifice decoupling, i.e., processes are unnamed and do not refer to each other. They lead to (a) one-event-one-handler definitions (“call-return” approach), as in rule-based systems such as event condition action, and (b) a non-general model, i.e., language API dependent (co-routines approach).

To summarize, event-driven programming approaches either emphasize decoupling but do not allow for reasoning about control flow or address the latter by sacrificing the former. In this paper, we bridge this gap by proposing the model of cooperative decoupled processes (CDP for short), which supports reasoning about control flow without sacrificing decoupling. Concretely, we propose:

• (I) Global control flow for event-driven processes Processes are asynchronous and concurrent. They can express interest in an event or pattern of events and can subsequently receive any event generated by another process that matches their interest. On top of this standard event-driven communication semantics, called migration, CDP models control flow by attaching pre-/postcondition transitions to handlers. Preconditions control which handler may take place and postconditions drive the occurrence of the next one. We present the E-Calculus, a formal account of the CDP model, which is loosely inspired by the Join calculus of Fournet and Gonthier (1996), contributing towards leveraging the popularity and expressivity of process calculi for the characterization of modular event-driven systems. We study the control flow formally as a preorder relation over pre-/postconditions attached to handlers. We have encoded a variant of the Join calculus to the E-Calculus. It turns out that (i) preordering of handlers of more than one postconditions in our model is analogous to reflexion in the core (recursive) Join calculus without message exchange over explicit channels, and (ii) migration of events between processes is analogous to nesting of processes modulo scoping on free product names.

• (II) Safe composition of event-driven processes Aliasing of events is created when processes are composed together. It is an important feature to model shared events, but may break the control flow. Multiple references to pre-/postconditions means multiple racing control flows, consequently introducing also conflicts on shared events. Thus, control of aliasing is needed to avoid break , i.e., avoid races, of control flow, and safe exchange of shared events when composing processes. This is achieved through a linear type system that gives the capability linear to pre-/postconditions (uniqueness) and nonlinear to (possible) shared events, where terms linear and nonlinear are used as in Girard (1987) linear logic. We establish subject reduction, migration safety, and progress for the type system. Subject reduction guarantees that handler occurrence and exchange of linear and nonlinear events is done in accordance with linearity constraints; migration safety guarantees that control flow is not broken and there are no conflicts when shared events are exchanged; progress ensures that the evaluation of a simple and well-typed process will never get stuck.

To recap, CDP with the linear type system is a (true) concurrent model and does not suffer from fragmentation of interactions across multiple handlers or from explicit conflict resolution of competing recipients on shared events. Pre-/postconditions control the interactions and their linearity prevents conflicts from happening, hence, solving the stack management and shared event problems.

This article is an expanded version of the conference paper version of Bejleri et al. (2016), which differs from it in several aspects. In particular, apart from the full definitions omitted from the conference paper, for instance full encoding of the variant of the join-calculus and typing rules for the runtime, we have provided formal proofs of our results and more examples showing the expressivity of the calculus and illustrating how the operational semantics and type system work, and also, we have given an expanded discussion with the related work and possible extensions that are currently been addressed.

The paper is structured as follows. Section 2 illustrates the problems of stack management and shared events. Section 3 introduces the CDP model and indicates how it addresses these problems. Section 4 presents the E-Calculus and the encoding of a variant of the Join calculus. Section 5 introduces the linear type system and Section 6 states subject reduction, migration safety, and progress. Section 7 surveys related work and Section 8 concludes with an outlook on future work. Proofs of properties are provided in Appendix A.

2 Background and motivation

In this section, we briefly illustrate the issues mentioned with stack management and shared events.

2.1 Stack management

We use the example of a fire protection system based on the standards defined by NFP Association (2015), which consists of two processes: (a) fire alarm and (b) fire suppression. The former includes the interaction of heat and smoke sensors to warn personnel in the event of fire; the latter includes the interaction of smoke sensors to suppress fire by releasing chemical agents. It is crucial that the second interaction occurs after the first: the warning alarm must occur before agents are released to advise personnel for immediate evacuation.

Event-based systems that support reasoning about control flow have traditionally employed manual stack management (see Adya et al. 2002; Bolosky et al. 2000; Cunningham and Kohler 2005; Ousterhout 1996; Welsh et al. 2001). Programs are organized as collections of event handlers. Control is defined through handlers that “call” other handlers passing along state, initiating so a new task, and expect a “return” from those to return the control to the originating task. As a result, the control flow for a task and its state are broken across several handlers, discarding so locality features. Programmers must match “call-return” pairs to reason about flow even in scenarios where handlers are present in different parts of the code.

Figure 1 gives the model¹ of the fire alarm and suppression relying on the syntax of representing events as objects and handlers as functions in a syntax. Receiving an event means reading and consuming that event. Method , defined below, reads the pointer to the event object, printing it to the standard output and consumes the event by invoking the function ( API) to deallocate the object from the memory.

Fig. 1

Fire protection in . a Fire alarm. b Fire suppression tasks. ı^* and ampersand denote, respectively, pointers and addresses of values in

Triggering new events is expressed through the new operator, i.e., creating new event objects. Events not declared within a function are .

The model uses a continuation object , defined below, to store the function to call, and the continuation object that stores the function where the control will be returned at the end of the call chain.

The scheduler, defined below, takes as input a object and invokes the function with the continuation object as input parameter. It is responsible of managing concurrency between the several tasks.

Figure 1a presents the task that is responsible for detecting smoke and heat in a room by receiving events and , and for driving their transformation into two new notification events and . These events are global. Function receives event and creates a continuation that stores the next handler function in the call chain and the continuation object , storing the function that the control needs to be returned at the end of the handler call chain. then passes control to the scheduler with as an argument. The scheduler invokes along state as an argument. Similarly to receives event and creates an object with the next handler function and the object , subsequently returning control to the scheduler which invokes along state. triggers events and .

does not return the control to the function in that triggered the chain of handlers of the fire alarm task, which would capture the end of the fire alarm task. Instead, it passes to the functions of the fire suppression task (shown in Fig. 1b) to thus modeling the composition of the two tasks. The fire suppression task consists of receiving another event and triggering event . The received event denotes detection of smoke in a room and the triggered event denotes the release of gas. Function receives event , creates its , and returns control to the scheduler, which invokes along state. Event is duplicated to model the reception on both and . triggers event and returns control to the scheduler on .

The above design fragments the interaction logic over five handlers (functions). It imposes strong coupling between handlers even across tasks: Each handler holds a reference to the next in the flow. Also the handlers explicitly manage control and state of the execution (“manual stack management”). The object stores the function, where the control will be returned and it is passed on to the other functions.

2.2 Shared events

Handler functions may compete for receiving shared events, which calls for a mechanism to handle potential conflicts, and, as we will see later, can lead to a series of issues from erroneous behaviors to deadlocks. To illustrate the problem with shared events, consider a scenario when functions and depicted above are both active, e.g. the client invokes the scheduler concurrently on both functions. Hence, and will compete for receiving event .

The manual control of the flow as shown in Fig. 1 allows to be active only after has received, hence consumed, its event before invoking the scheduler and moved to a program state that will not compete with . The order of consuming and invoking the scheduler, by virtue of instantiating , will guarantee the sequential use of events in case of dependencies.

Thus, the explicit modeling of the control flow supports programmers in handling conflicts between cooperating tasks on shared events, i.e., programmers do not employ any mutexes to model synchronization. However, the approach is tedious and error prone, as programmers must programmatically match points where shared events are consumed and new tasks are scheduled. Also, reasoning about control flow does not support programmers in handling conflicts between tasks that are not of the same flow, i.e., two tasks of independent flows can access some shared state.

3 Cooperative decoupled processes

This section discusses how CDP addresses the challenges of stack management and shared events, while retaining decoupling.

3.1 Decoupling

CDP provides concepts that support decoupling along its three dimensions: space, synchronisation, and time.

3.1.1 Space decoupling

The key concept for modeling space decoupling—which roughly posits that processes should not refer to each other (Gelernter 1985)—is that of a site. A site composes events and handlers into a scoping construct. Handlers of a site (a) describe the logic over many events and (b) compose handlers in disjunction. Feature (a) is in the spirit of many modern event-driven systems by Benton et al. (2004) and Haller and Cutsem (2008) and Ham et al. (2014). Feature (b) models choice, including non-deterministic choice, allowing terms that specify various ways of behavior. These features allow many events in a site to transform only according to handlers associated to that site, and the site’s handlers to drive the transformation of only the site’s events. Site is an abstraction that limits the visibility of events, offering a characteristic for processes. Abstraction and information hiding are the basic principles that influence structured programming (see Fiege et al. 2002; Parnas1972).

For illustration, consider the site of the fire alarm below. The site definition is made of two clauses and . The former presents the definition of a handler and the later represents the events which currently occur within the site.

In the handler, (1) the operator specifies parallel composition, (2) names and are called, respectively, reactants and products, (3) the infix operator $\rhd$ distinguishes names denoting reactants from names denoting products, and (4) the arrangement of reactants is called join pattern. In the events occurring in a site, names denote events and specifies parallel composition of events. Reactants serve as binders to events defining so their visibility to the other sites. In the example cited above, events and occurring in the in clause are bound by the reactants of the handler and consequently can be transformed; in turn, this handler can transform only the events present in the site.

Non-determinism

Consider a variant of the fire suppression system that controls fire through a sprinkler or a gaseous system (see below). The suppression system controls fire by using the component detecting it first.

The infix operator or defines the two different ways the suppression system can behave. If the smoke detector of the gaseous system and the heat detector of the sprinkler system detect an event of fire at the same time, the choice to release inert gases or chemical agents is done non-deterministically.

Non-determinism in our model is not limited to the choice of event patterns; handlers having the same reactants but possibly different products are also chosen non-deterministically. That is, a pattern of events can make some handlers with different products able to occur. For example, a gaseous system can use one of the following four means to extinguish a fire: reduction of fuel, reduction of heat, reduction of oxygen and reduction of the chain reaction of the fire ingredients. Below, we give the definition of site.

where handlers, having the same reactants, are not ordered and the product on each handler captures a unique means to extinguish a fire. The choice of the gas to control a fire is made non-deterministically. When a disjunction exerts one of its handlers, the others are rendered void.

The example illustrates how CDP supports space decoupling: Neither of the sites, e.g., and , has a reference to the other and knows with how many it is interacting with.

3.1.2 Synchronization and time decoupling

According to Eugster et al. (2003) and Gelernter (1985), synchronization and time decoupling are supported through the way in which we model the interaction between sites. Sites communicate by (1) letting out (also reversible) events that do not participate in any of their handlers and (2) letting in events that can participate in some of their handlers. To achieve this form of interaction, we allow to express events outside a site, called global events, that model events shared by handlers of different sites, in contrast to events that are local that model events shared by handlers of a single site.

Events that are bound by reactants are trapped within a site by handlers and can be transformed by parallel composition. Conversely, events that are not bound, including product events, are not trapped in the site and so, cannot transform, giving them the ability to leave and (re)enter the site.

For an event to leave a site means that it composes in parallel with the site. For example, after a handler occurrence in the updated site contains the new product events

where events and are not bound by any reactant so they can leave and reenter the site without restriction. Below, event has left the site, becoming global.

The other fundamental feature to achieve migration is by dynamically adding global events into a site. A global event can be added into a site only if it is captured by one of the reactants present in the handlers. Consider a fire alarm site where the event is stated as global and so is composed in parallel with the site as in:

can be added to the site since it is captured by a reactant of the handler. This results in the that now contains both events locally.

In this form of interaction, the possible recipient sites of a global event may not be active in the moment when the global event is produced; i.e., those sites may not be yet “connected” with the others, and, also, an event is asynchronously received in a site.

3.2 Enabling declarative safe composition

In here, we present the features of our composition model: (a) modeling control flow between handlers, (b) exploiting (multiprocessor) parallelism, and (c) implicitly avoiding conflicts between recipients of shared events and its safety properties.

3.2.1 Control flow

To model control flow, handlers in our model do not only reference observed events to trigger new events; they also reference control events that express a flow through their occurrences. Control events are also called pre- and postconditions events; they are declared within square brackets to distinguish them from other reactants and products. Brackets regard the syntax of handlers and the static semantics, and have no meaning at runtime.

Figure 2 gives the model of the fire protection system in CDP. We extend the handler of the with the precondition on reactants and postcondition on products. is a precondition that bounds to the first handler in the system. Also, we extend the handlers of the with the precondition, and and postconditions. The flow between the fire alarm and suppression handlers is represented by including the postcondition of the alarm handler as a precondition in the suppression handlers. Postcondition events use the concept of migration to leave their birth sites and join the sites of the next handler that declare them as precondition events.

Fig. 2

Fire protection in CDP. a Fire alarm (Fire alarm site 4). b Fire suppression tasks (Fire suppression site 2)

A handler occurrence precedes another if some of postconditions are preconditions of . For example, handler precedes () . Our control flow is formalized as a preorder relation, i.e., “almost” a partial order, since anti-symmetry does not hold. Consider the ordering of three handlers as by definition of . By transitivity, we conclude that and, by definition of , we have that . However, handlers and are not equal. In our system, two handlers are equal if they have the same preconditions, reactants, postconditions, and products. Hence, our ordering does not hold anti-symmetry, meaning that three handlers forming a loop do not imply that the first and third are the same.

3.2.2 Multiprocess parallelism

Our model involves exploiting (multiprocessor) parallelism. Processes are allowed to yield control to more than one process. This is modeled by having transitions from many preconditions to many postconditions. To illustrate support for parallelism, consider how one can model a variant of the fire suppression with two components, one using a sprinkler and another one using a gaseous system, both running in case of fire, consequently exploiting parallelism. To enable this, their handlers must be modeled in two parallel sites, each having a different precondition, e.g., and as

The postconditions of the handler of must reflect both names to allow thus the two handlers to occur in parallel as

CDP can also be used to describe more complex behaviors than sequencing and forking such as joining of several handlers. Joining of handlers means that the preconditions of a handler may denote more than one name, allowing it to occur after other handlers have. We consider an event-driven modeling of a variant of the MapReduce programming pattern introduced by Deniélou and Yoshida (2011). A big data process forwards parts of the service data to a particular worker process. Subsequently, the workers compute in parallel the tasks, and then forward the partial results to the result process. In this variant, the service of the pattern is continuously looping and processing jobs. Below we depict the diagram of components and the program in the model.

The postconditions of the big data process denote that the three workers can accomplish the tasks in parallel, and the preconditions of the result process denote that the final result is computed only when all the workers have accomplished their tasks. The postcondition of the result serves as a precondition for the big data, modeling so the loop of the service. For simplicity, we have not modeled the mapper and reducer processes, including their communication patterns.

3.2.3 Solving conflicts

Our model involves also avoiding conflicts on shared events. Only processes that have control can receive shared events, i.e., processes having control events prevent other processes of a flow from receiving shared events. This is modeled by supporting addition of global events to sites that contain the precondition events of the handler capturing them. Thus, control events serve as an implicit lock mechanism to the interaction of shared events. Consider a fire protection system, where the sensors of smoke are not local to the processes of fire alarm and suppression. This is modeled as two sites composed in parallel with the global event . Also, the precondition event is present in the site of the fire alarm.

A conflict between the two processes raises on adding the shared event. Such conflicts can lead to a deadlock; e.g., if the event is erroneously added in the fire suppression site, no handler will be able to occur. However, this cannot happen, since events are only added to sites that have a precondition that holds, which is not the case with the fire suppression site. This event is thus added into the fire alarm site, where the precondition is present, permitting the fire alarm handler to occur.

The above solution relies on the assumption that two handlers of a flow cannot have control at the same time, e.g., the preconditions for fire alarm and suppression cannot have control at the same time. We have defined a number of invariants to capture this assumption and others. The invariants are expressed into the typing rules to guarantee that every handler is part of a flow, flow defined over handlers in parallel is deterministic, and only two handlers of different flows can exchange events.

• (I) No orphan handlers: the name denoting a precondition in a handler must denote a postcondition in another handler or init.

• (II) No racing handlers: preconditions of handlers in parallel must be unique.

• (III) No break of flow: names of preconditions are the same only to postconditions and not to products or reactants, and postconditions of handlers must be unique.

• (IV) No racing flows: products of a flow can be referenced by only reactants of another flow.

To illustrate the importance of establishing these invariants, we consider several versions of the fire suppression system that can describe invariants I, II, III, focussing only on the handlers with some abuse on the notations. Examples of invariant IV will be presented later in this paper. An example not holding the first invariant is defined over the following two handlers composed either in parallel or disjunction:

as the preconditions in both handlers are not and there is no handler having postconditions of those same names. Both handlers are not part of any flow. In such a system, clients are blocked within the sites.

An example not holding the second invariant is the system defined over the following two handlers:

as both handlers in parallel have the same precondition. In here both handlers are in race to receive the control event . In such a system, clients are always racing to achieve control.

A third example not holding the third invariant is defined by the following two handlers composed either in parallel or disjunction

These invariants allow branching of a flow. That is, a flow can be non-deterministic for handlers in disjunction. This is modeled by allowing a precondition to appear in different handlers in disjunction (see Fig. 2b).

In this version, there is a copy of control event in each site. As there may be an arbitrary number of concurrently running clients of fire alarm and suppression, the two sites will run forever without any cooperation ever being established.

Unlike in systems that dot not support establishing these invariant, the CDP model ensures this statically by a type system. Hence, pre-/postconditions are placed within brackets. One can easily verify that the fire protection example (see Fig. 2) holds the invariants.

4 The E-Calculus

We now introduce the core E-Calculus to formalize the intuitions given above. This section contains the syntax, operational semantics, an illustration of the semantics rule through the fire system example, and encoding of a variant of the join-calculus into the E-Calculus. The E-Calculus is based on a small-step operational semantics, defined over inference rules and a relation of structural congruence.

4.1 Syntax

The meta-variables, describing the calculus, along with their meaning are as follows: stands for processes; ranges over names of events, reactants, products, preconditions, and postconditions; stands for handler declarations; stands for local events; stands for join names. Meta-variables with subscript denote the same class of terms; e.g., denotes a process.

Figure 3 gives the syntax of processes. A process is defined as a global event; a site—a process definition inspired by the Join calculus of Fournet and Gonthier (1996), that, in contrast, does not allow reflexion and nesting of sites to ensure decoupling or a composition in parallel of the behavior of two or more processes. A handler is a blueprint that describes transformation of events along with their pre- and postconditions or is defined as disjunction of two or more handlers. Events and pre-/postconditions are denoted by join names . Join names denote non-empty patterns of names (preconditions, postconditions, reactants, or products) or a composition of two or more join names. Local events are defined as (used to express a site without local events), one or including events in parallel. In the following, the definition of free names is given; the association of the parallel operator is weaker over .

Fig. 3

Syntax of processes

Definition 1

The set of free names of a process , written , and the set of defined names of a declaration , written , are defined as follows:

Below, we provide the formal definition of control flow as a chain of handlers defined over a preordering relation, i.e., holding reflexivity and transitivity:

Definition 2 (Preorder)

Write for handlers of a program. Then, we write when the occurrence of precedes the one of . Formally is the preorder such that if . For all in a program, the following properties hold:

• (Reflexivity)

• (Transitivity) if and then

A handler precedes if the postcondition of the former define the precondition of the latter as stated in . If the set would be empty, the two handlers are completely independent.

We write for the transition associated to handlers , i.e., parts containing only the pre- and postconditions: .

Definition 3 (Chain of handlers)

A chain of handlers, written , is defined as , such that for , we have that for .

Structural congruence is the smallest congruence on processes that satisfies the axioms shown in Fig. 4. It defines processes that have the same behavior but different syntax. In other words, given two structurally congruent processes they will behave the same in every possible context. Therefore, it is of interest to build a reduction relation that is also defined on structurally congruent terms.

Fig. 4

Structural congruence

and define that parallel composition of processes, declarations, and local events is commutative and associative. defines structural congruence, i.e., associativity, commutativity, and identity, over local events in a site. ² allows an event not bound by any handler to leave and (re)enter any site, reading the rule from the left to the right and from the right to the left. defines as the identity element of local events with respect to parallel composition.

4.2 Operational semantics

Figure 5 gives the operational semantics of the E-Calculus via the reduction relation where the state of the machine is defined only by terms of the calculus, written , meaning that “process reduces to process in one step.” A handler occurrence is the act of checking for the presence of a pattern from a set of events that matches the pattern of preconditions and reactants, and substituting the event pattern with postcondition and product events as defined in rule . Local events define additional events that are not copies of postcondition events (see side condition , allowing terms of larger patterns to reduce. The side condition is necessary in proving the coherence of the dynamic and static semantics. Global events can be added to a site following the rule expressing addition of precondition events and rule expressing addition of reactant events while solving conflicts between recipients, i.e., a reactant event (possible shared) is added if the control events are present in the site (see side condition and ). Rules and allow to infer the handler that, respectively, matches a pattern of events and allows the addition of a global event from the composed handlers. defines computation in processes composed in parallel, reducing first each subprocess. defines reduction on structurally congruent terms, restructuring before and after a reduction; if applied in a derivation, then it is the final rule.

Fig. 5

Operational semantics

4.3 Reduction steps of the fire protection system

Evidence of the validation of our design and its effectiveness is given by the reduction of the fire protection system introduced in Section 3. Moreover, to keep the presentation tractable, we consider a simplified version while preserving its meaning. The main process is defined as a parallel composition of the alarm (defined through the handler ) and suppression (defined through the handler ) systems as shown below.

In the above definition, each system is defined as a separate site and the events ready to transform are those triggered by their respective detectors . Each system has its own detectors; i. e., the heat detector of the sprinkler is located within the sprinkler head, and the smoke detector of a gaseous system is located on the ceilings of a room.

The initial precondition event is defined as global. The first step consists in adding the event into the site of the alarm handler, since it is captured by a precondition of its handlers. Entering and leaving on other sites by is not interesting since it does not represent or lead to a reduction step.

The second step occurs when the fire alarm handler takes place and raises events and , which, together with event are transformed into events and through the application of the axiom .³

The third step migrates into the site of the fire suppression. To achieve this, the process defined as:

is restructured according to the congruence axioms and where leaves the birth site to be added into the site of the suppression system:

The first three steps described the detection of the fire alarm and the transformation from an initial state with precondition to a new state with precondition . Under such condition, along with one of the events or the second handler of the suppression system take place.

The fourth step consists in the execution of the second handler. Rule is inductively applied to infer the site of the suppression system. Rule guides the choice of the handler that matches the events in the site. If both events occur, two possible transformation are possible. This choice is done non-deterministically (in this example, we have chosen to present the reduction resulting in the production of event in parallel with ). Hence, the derivation tree, following a bottom-up approach using rule , infers the term:

Rule is applied since is not a product name of the handler, resulting in the process:

At this point all the used rules can be applied top-down in the derivation tree, where will result in:

The result of the final step is the postcondition event that signs the end of the computation.

4.4 Encoding a variant of the core (recursive) join calculus

The E-Calculus can express control of extending the machine with reducible sites (reflexion) as in the core (recursive) Join calculus of Fournet and Gonthier (1996) without message-passing over explicit channels. Reflexion in the Join calculus is the ability of reactions (handlers in our model) to extend the machine with new molecules (patterns of events in our model) along reaction rules. Our purpose here is to show that (1) reducible sites can be enabled through the pre-/postcondition mechanism rather than dynamically adding them into the solution, and (2) communication between sites can be done using migration rather than nested definitions, providing a model of computation that offers decoupling and distribution.

Firstly, we translate the syntax of the core Join calculus (a) into a variant of it (b) without messages exchange over explicit channels using the function .

where the scope of is in the process definition construct . Intuitively, the translation removes names attached to reactants and products (rules and ) along their occurrences in and names associated to global names (rule ), including products themselves (rules (1) and (2)).

Secondly we present the encoding of reflexion and nesting. For presentation reasons, the encoding is done in two steps. That is, we encode reflexion of the variant of the Join calculus into a variant of the E-Calculus without disjunction but with nesting and then encode nesting as in into the E-Calculus. The first encoding, written as , is given below

where and the index denotes the preconditions when encoding a Join-like reaction into a handler. Rules and define encodings of a name and parallel composition. Rule defines encoding for a Join-like site, where the product is defined by names and sites for in parallel; if then there are no sites in the product. The encoded “main” Join reaction contains as precondition and postconditions (fresh names) as sites; the process in the scope of the reaction is not part of the reflexion semantics so it is encoded inductively with a different index . Sites are encoded in the solution with an index that corresponds to one of the postconditions. Each of the postconditions relates to the precondition for the handler of each site. Intuitively, this means that sites are reducible only after the “main” handler occurs. The image of the translation is the forking subset of E-Calculus, i.e., transitions associated to handlers are defined by one precondition and many postconditions. As expected, reductions in this subset only produce new flows. The initial encoding index is .

Nested process definitions can be distilled into flat definitions composed in parallel up to the scoping of free product names as:

where . This rule is similar to our congruence rule . One can observe that names loose the scope on . They can gain the scope on free events in using migration but not on the free products .

5 The linear type system

This section gives an informal description of the challenges addressing aliasing in the calculus, introduces the linear type system through a set of rules and followed by the typing of a set of examples.

5.1 The addressed challenges

Two are the main issues that the linear type system deals with: when uncontrolled aliasing can break the uniqueness of control flow and safe exchange of shared events. Aliased events can also be called nonlinear, in contrast to nonaliased events called linear. In this session, we present several scenarios consisting of one precondition and one postcondition per handler without diluting their complexity.

The first scenario considers a global event coming from an unbound product of a previous handler occurrence or stated as global. is referenced by a reactant and also a precondition of two different sites (regardless of the same or different flows) as

The operational semantics allows to add k in one of the two sites, i.e., it can be added in the first since it is referenced by a precondition and in the second since it is referenced by a reactant. Hence, two possible control flows rise. By our assumption that comes from an unbound product, immediately follows that it is not a control event. Thus, adding it to the first site breaks the control flow of both handlers. Here, aliasing can be controlled by distinguishing between consumers (recipients) of events, preconditions, and reactants, and producers of events, postconditions, and products. This problem is relevant also if both handlers are part of a single site

or when is stated as local to the first site. In the latter, stated events do not define control events with the exception of so they can be distinguished as produced by products.

The second scenario, similar to the previous one, is when event is produced by a postcondition, i.e., it is a control event (in here, handler are part of different flows). Thus, adding it to the second site breaks the control flow of both handlers. Aliasing here can be controlled with the same mechanism as above.

A third scenario represents a shared event that is referenced by reactants of two handlers of the same flow

presents a challenge of aliasing that is resolved by the operational semantics; i.e., is added only in the first site, which has control of the flow at that point (precondition event). As expected, the first handler returns control to the second handler. The expectations will also hold for the case when both handlers are part of a single site. However, the operational semantics cannot resolve a similar scenario where handlers are part of different flows

The operational semantics allows to add in one of the two sites, i.e., both sites contain the precondition events. Thus, both sites are possible recipients, rising a conflict between them. Here, aliasing can be controlled by distinguishing between recipients and producers of events of different flows. This problem is relevant also if both handlers are part of the same site. However, if is stated local to each site, i.e., it is not shared, then no issues arise.

To address the challenges presented in this section and in Section 3.2, the type system should not only control aliasing of existing events at definition time but also of the ones that may be created during evaluation to ensure uniqueness of control events and safe exchange (no conflict) of shared events in all steps of computation. So, static control of aliasing should address also blueprints of events. In short, at different handlers, the type system forbids terms of the following form:

• 1. The same name for more than one precondition or by more than one postcondition.

• 2. A name for precondition without a copy for a postcondition, except the name .

• 3. Products referenced by preconditions.

• 4. Postconditions referenced by reactants.

• 5. Products of a flow referenced by more than one reactant of other flows.

• 6. Precondition of the first handler in each flow is not .

5.2 Typing rules

On the typing level, we introduce linear types and nonlinear types for a name. A linear type gives the capability to a name to be used only once and a nonlinear type gives a capability with no multiplicity constraints. can take two forms: and to distinguish between preconditions and postconditions.

Similarly, can take two forms: to distinguish between reactants and products. We introduce also flow typing to track the flows where a name is used.

Type environment and judgments

A type environment is a finite set of linear and nonlinear type assignments to names of the form and , where all names are different. Following, we give the definition: . We write for the union of two type environments, whereby the names of and are disjoint. Type judgments are of the form for processes, for declarations, for preconditions, for reactants, for postconditions, and for products. In addition to union (defined informally by “,”), we define the combination operations on types and environments. They ensure that linear capabilities are exercised to guarantee uniqueness of control events and a safe exchange of shared events in the presence of different flows. We distinguish between combination operators for type environments of preconditions , reactants , preconditions and reactants , postconditions , products , postconditions and products , handlers , disjunction , site , and processes of the same and different flows. Below, we give the formal definition of the sub operators; denotes all the fore-mentioned combination operators: and .

Definition 4 (combinations of type environments)

is defined as:

These operations are associative and commutative. They are not always defined if exists and such that . This is the case, whenever and capture harmful aliasing scenarios listed in Section 5.1. These operations are similar to the product rule in Girard’s linear logic (Girard 1987).

Combination of types

Figure 6 gives the combination of types coming from environments in typing rules. Rules of and prohibit the same name in more than one respectively precondition and postcondition. These rules enforce only one copy of precondition and postcondition in a handler. Rules of Inline and combine names denoting respectively reactant and products, allowing multiple copies. These rules do not enforce any constraint on the number of copies of a reactant and product in a handler. Rules of and prohibit combination of preconditions and reactants types, and postconditions and products types. Rules of (a) combine precondition and postcondition types into a linear type and reactants and products into a nonlinear type and (b) prohibit combination of preconditions with products and postconditions with reactants types. The rules so far are defined over the flow consisting of only the handler in consideration. The following ones consider more than one handler; hence, (possibly) involving many flows. Rules of (1) ensure linearity of pre-/postconditions in handlers composed in disjunction, (2) prohibit combination of linear and nonlinear types, and (3) prohibit conflicts between recipients of different flows and a product (however the rules allow the combination of one reactant and many products of different flows). In here, types can combine since names are composed in disjunction, not breaking so their single-copy capability. The concatenation of two flow typing is defined as where such that . Rules of prohibit combination of linear types to nonlinear type p, prohibiting so conflicts between recipients of different flows and a product, and combine nonlinear types. For presentation reasons, we present the rules that prohibit combination of types for processes in parallel. The side condition ensures that is a single flow. Rules of prohibit (I) the same name for more than one precondition or by more than one postcondition on different sites, (II) referencing of products by preconditions and postconditions referenced by reactants, and (III) products of a flow referenced by reactants of other flows. So, Γ is extended with new non-/linear types: .

Fig. 6

Combination of types

Typing rules for terms of the E-Calculus

are presented in Fig. 7. Rule assigns a linear type to the special event in the environment: the empty flow typing is assigned to every stated event as a distinguished typing. Rule assigns a nonlinear type to a stated event, either local or global, in the environment. For two processes in parallel to be well-typed, the subprocesses must be well-typed and the environments must combine accordingly . For a site to be well-typed, the declaration and the events must be well-typed and the environments must combine accordingly . Handlers composed in disjunction are well-typed if each handler is well-typed and the environments must combine accordingly . Inaction is well-typed with an empty type environment . A handler is well-typed if preconditions, reactants, postconditions and products are well-typed according to their typing judgment and type environments combine with the flow typing of the handler. The four judgment distinguish between the different classes of names to maintain a minimal syntax. In here, the notation Γ@Δ is a shortcut for l ₁@Δ,...,l _n @Δ. Parallel composition of join names is well-typed if the single names are well-typed and the type environments combine. Pre-/postconditions are typed as linear, and reactants and products as nonlinear.

Fig. 7

Static semantics

Proposition 1 (Decidability)

The typing relation is decidable by an algorithm of time complexity .

Proof

The length of a term P is defined by the number of names present in it, including all the occurrences of the same name; i. e., a list of names. By the typing rules, every name in the list is checked whether it is the same and, if yes, how it combines according to rules in Fig. 6. Type combination is done in constant time complexity. Thus, the complexity of typing is determined by the equality check of names in the list. This is done in the worst case—when all names are different—O(|P|²) (for every name a linear search takes place). □

However, the typing rules so far do not ensure that the precondition of the first handler for every flow is and the final type assigned to a name is combined or . Thus, we introduce a new type judgment $\emptyset \vdash _{flows} P$ and a typing rule that captures that constraint as

where . That is, a process P is well-flowed if it is well-typed, for every consumer there is a producer, there may be free postconditions and products, and every flow in it starts with the precondition . Given Γ, this rule is decided in linear time.

5.3 Typing examples

In this section, we present the typing of examples discussed in Section 5.1 and not only.

Example 1

Write the program . If the term is user-defined, then each process has the following type under environments:

• (I)
• (II)
• (III)
• (IV)

where and . Note that () is undefined since the combination of the types for name is by Fig. 6; hence, . If the term is part of the runtime where are linear, created by postconditions of sites in then and . However the combination of types for is by Fig. 6.

Example 2

Write the program . Then each process has the following type under environments, considering the case of event comes from a postcondition of in the second process:

• (I)
• (II)
• (III)
• (IV)

The combination of the types of name is not defined since by Fig. 6.

Example 3

Write the program and . Then each process has the following type under environments:

• (I)
• (II)

where the combination of types for name and is not defined since or by Fig. 6.

6 Properties of typing

In the remainder of this section, we establish the fundamental behavioral properties of typed processes.

Subject reduction

states that the type of a process is preserved following the reductions. As a process runs, handlers occur and events are exchanged between sites. Subject reduction guarantees (a) occurrence of handlers if linear events denoting preconditions and nonlinear events denoting reactants are present in the site, and (b) addition of linear and nonlinear events to a site if referenced respectively by preconditions and reactants while avoiding conflicts in a flow. This rule out terms such those presented in Section 5.

Theorem 1 (Subject congruence and reduction)

• 1. If then iff .

• 2. If and then .

• 3. If and then

Proof

Properties (1) and (2) are proved by induction on the typing judgment assuming respectively and . (3) follows as a corollary from (2). For their proof, we use lemmas and propositions such as typing inversion and associativity of type combinators (see Appendix B). □

Migration safety

ensures that a control event is exchanged only between two processes of one flow and shared events are exchanged between processes of one flow or between two flows (in the latter, only if the “sending” flow has no recipient process). To establish it, we give the reduction context: . We write for precondition contained at a handler of a site in ; analogously, we write for and . We say l is added to if is a global event referenced by a precondition or reactant (in the latter, from a site that contains the control events).

The following result is defined when the initial handler has occurred, i.e., the enabled control event is not .

Theorem 2 (Migration safety)

Suppose then for adding to where such that either contains:

• 1. exactly one and

• 2. exactly one pair of and

• 3. exactly one and many in only one site

• 4. many of the same flow

• 5. many and many of the same flow

• 6. exactly one and many of different flows

Proof

This property is proved by the derivation of the typing judgment, analyzing all possible cases. The observation is that a type combination represents an exchange of shared events between same or different flows, e.g., a type combination for an event will represent an exchange of that shared event (see Appendix B). □

By Theorems 1 and 2, we have that a typed process of many flows will not go wrong, i.e., (1) a handler occurs over events coming from postconditions and products of previous occurrences (or stated products), and an event is added to a site if it comes from a postcondition or a product of previous occurrences and (2) an exchange of a shared event occurs between processes of the same flow or of two different flows (in the latter, only if the “sending” flow has no recipient process).

Progress

asserts that the reduction of a simple, and well-typed process denoting a tree of flows (flows starting with precondition ) will never get stuck, i.e., the process is inactive or can make a reduction step.

Definition 5 (Inactive)

A process P is inactive if defined as a composition of sites where no handlers can occur and no events are exchanged, i.e., there is no such that .

Definition 6 (Simple)

A process P is simple if (1) event is present, (2) reactant events of the first handler are present, either as global or in the handler’s site, (3) there are as many reactants for a handler as declared events and unbound products of handlers in simple processes.

(1) rules out terms like ; (2) rules out terms like ; (3) rules out terms like where only one copy of is present.

Theorem 3 (Progress)

If and is simple then or inactive.

Proof

By induction on the derivation of the typing judgment (see Appendix B). □

Proposition 2 (Properties of the Fire Protection example)

is a simple process. Since then no handler occurrence errors, no lack andduplication of control flow, and no unsafe exchange of shared events.

Proof

Follows immediately from the typing judgment. □

7 Related work

Automatic stack management and decoupling.

The automatic stack management is used by Shih et al. (2002), Gustafsson (2005), Haller and Odersky (2006), Haller and Odersky (2009), and Li and Zdancewic (2007) and Foltzer et al. (2012) to address the problem of storing and communicating the state between tasks without requiring programers to model the stack. Every task is expressed as a single procedure that blocks on an I/O operation while keeping the current state. Closures are used to encapsulate data into callback functions. We address the same problem through sites and migration based on decoupling and without using complex, non-mainstream primitives. In contrast to our proposal, closures, e.g. continuations of Friedman et al. (1984), are based on strong coupling between tasks, i.e., pointers are kept between them, and are not present in low-level languages, e.g. C, C + +. This sacrifices program readability and maintainability, and is dependent of the language API.

Decoupling is used to increase scalability of distributed asynchronous applications. It is implemented in various communication models (Franklin and Zdonik 1997): push-pull, aperiodic-periodic, and unicast-multicast. In our work, decoupling is used to address the stack management problem and is defined over unicast. Extending decoupling to multicast is ongoing work.

Formal languages

The closely related calculi to the E-Calculus are: the Join calculus of Fournet and Gonthier (1996), the M-calculus of Schmitt and Stefani (2003) and Germain et al. (2002), and the Distributed Join (DJ) calculus of Fournet et al. (1996). The relation of the join-calculus to the E-Calculus is given through the encoding of a well-stated variant of the join-caclulus, so we focus here on the M and DJ calculi.

The M-calculus describes a distributed, higher-order version of the Join calculus to investigate concepts in security and failure-handling. Higher-order communication along programmable localities are introduced to address the strong locality of the Join calculus where names are permanently bound to a single locality (our sites). It comes with a cost of complex reduction rules and behavioral type system, based on concepts such as membrane, coming from the cham of Berry and Boudol (1992), and so-called routing rules.

The Kell calculus of Bidinger and Stefani (2003) is a successor of the M-calculus. In contrast to the latter, it is used to investigate concepts and properties of component-based programming. Kell supports local actions and hierarchical localities as in the M-calculus. Thus, the reasoning behind the relation of M-calculus and E-Calculus also applies to Kell.

DJ is the original work on a distributed version of the Join calculus to express mobile agents moving between physical sites. It integrates concepts such as hierarchical localities, transparent mobility and communications. The semantics is defined over multiple solutions where every name is defined in at most one solution. This is similar to our parallel sites but more restrictive to our migration strategy. Despite their expressiveness in modeling distribution, none of these calculi address the challenges of three main tenets in event-driven programming: stack management, shared state and decoupling.

However, neither the Join calculus of Fournet and Gonthier (1996), nor the M-calculus of Schmitt and Stefani (2003) and Germain et al. (2002), nor the Distributed Join (DJ) calculus of Fournet et al. (1996) address concepts such as migration across decoupled sites and preorder. Reflexion in the Join calculus (see Fournet and Gonthier1996), i.e., the ability to dynamically add new handlers to the machine to define different behaviors at different points of execution, does not suffice to capture ordering of handlers. Removing of handlers is another necessary key mechanism to model ordering. Both adding (enabling) and removing (disabling) of handlers are fundamental concepts in expressing order (see Bejleri et al. 2006; Aldrich et al. 2009; Sunshine et al. 2011).

Recently, as shown in Crafa and Padovani (2015), concepts coming from the Join calculus are used to investigate typestate oriented programming in a concurrent setting. At a high level, our pre-/postconditions can be viewed as roughly analogous to typestates (see Strom and Yemini1986) in procedural and object-oriented programming. In contrast, that work does not address reasoning of control flow and decoupling in event-driven programming. Thus, it is of interest to investigate how the E-Calculus can capture object interfaces in the presence of advanced typestate features such as prohibitions and obligations.

Type systems

The area of validation for event-driven programming is relatively novel and not explored. Recently, a model checker was introduced by Desai et al. (2013) for a DSL that supports asynchronous events. A type system based on session types is designed by Hu et al. (2010) for a variant of the π calculus extended with event register.

The π calculus type system (see Kobayashi et al. 1999), which this type system is inspired, controls the number of times a name is used in a term by imposing polarity and multiplicity constraints. Linear and nonlinear types take three forms i/o/# to capture the action of receiving, sending and both; in contrast, our type system captures the behavior of pre-/postconditions, reactants, products, events, and the union of them. A fundamental difference with our work is that no one of these systems captures and guarantees the uniqueness of control flow and safe addition of global events in the presence of aliasing.

The type system of the join-calculus (see Fournet et al. 1997) extends polymorphism of ML to control the correlation between channels and transmitted messages. The first restriction consists of limiting the congruence rules and relaxing the reduction rules of the original work so reactions composed in conjunction reduce. The second requires every name to be defined in exactly one definition. Our type system allows names to appear in different definitions by satisfying linearity constraints, and handlers composed in disjunction are reduced according to rules ⌊R-DisO, R-DisA⌋.

The type system of the M-calculus (see Schmitt and Stefani2003) guarantees the determinacy of the routing mechanism by using additional information that specifies an “address” on the names. The unicity of address is based on a linear concept that does not relate to ours (as a matter of fact, there are no i/o types) and relies on complicated modal rules. In contrast, our type system uses l _r , l _p , p, r types to enforce polarity and multiplicity constraints. The only complex feature of our type system stands in the large number of type combination rules due to the many classes of names; although, each rule in isolation is easy to understand.

8 Conclusions and future work

This paper introduced an event calculus and a linear type system to address the problems of reasoning about control flow in event-driven programming without hampering decoupling in the presence of aliasing. The E-Calculus and the type system add another fundamental stone to the formal study and validation of event-driven systems by proposing a practical model of cooperative decoupled processes. Our system demonstrates the symbiosis between these two main tenets through a concise calculus and type system, including number of constructs, rules of operational semantics and type system, and proofs of properties. Our type system ensures subject reduction, migration safety, and progress. We are currently using this work as basis for further investigations:

Message-passing over explicit channels

is key feature in distributed systems. It is important in event-driven programming to correlate events with data. Its modeling in the calculus poses the challenges of defining the scoping rules for values in parallel sites. A natural feature to be added alongside message-passing is filtering. The addition of this feature should be straightforward and should involve little overhead in the operational semantics.

Multicasting

Floyd et al. (1997) is a distinguishing feature in several event-driven system, i.e., an event is distributed across many sites in paradigms like implicit invocations/publish-subscribe. Multicasting depends on the interested sites of the event and the application semantics. We plan to make the choice of multicasting vs unicasting an integral part of an event’s definition rather than that of individual producers or consumers. Its modeling poses challenges in the syntax and semantics of the E-Calculus, i.e., how to (1) characterize events that will be produced for multicast and (2) add them into every site without being consumed, while preserving decoupling.

Encodings

Encoding of the λ-calculus (cf. Fournet and Gonthier1996) into the E-Calculus is an interesting mathematical problem, where the key issue stands in encoding higher order application into non-hierarchical process definition. Of interest would be to study the properties of the E-Calculus as a process calculus such as observational equivalence, and a comparison to the π-calculus.

Implementation of a safe event-driven library

in a mainstream object-oriented language represents the next step in the implementation of the E-Calculus and its type system. The library must support constructs for join patterns and sites, and explore how such features integrate with core OO features such as late binding and subtype polymorphism. We are using Scala for this implementation, given its rich existing support for event-driven programming (Gasiunas et al. 2011; Ham et al. 2014).

Appendices

Appendix A: Combination of types and typing rules for the runtime

Combination of types for the runtime include combination of postcondition and product events created during evaluation:

to capture exchange of events at runtime. The typing rule for the runtime include typing of init and reactants:

$${init}:{l}_{r}{l}_{p} \vdash_{pre} {init} \quad {\lfloor\textsc{T-RInit}\rfloor}\qquad {l}:rp \vdash_{r} {l} \quad {\lfloor{\textsc{T-RRName}}\rfloor} $$

to preserve the static type with the runtime type, after stated (declared) events are consumed. These rules allow statement and proof of subject reduction. Combination with other products for the name in the $\vdash _{r}$ judgment will combine to the same type rp.

Appendix B: Properties

This section gives the full proof of subject congruence and reduction, migration safety, progress along lemmas used in their proofs. We describe the approach taken for proving type safety for our system. We define important conditions and present the key lemmas needed for proving subject reduction (preservation) and migration safety. We consider all cases for both subject reduction and migration safety. For subject reduction, we use the following lemmas and propositions. Given typeable terms, the first lemma describes structure properties of type environments where I, J, K, M, N denote sets of naturals.

Lemma 1 (Type environment inversion)

• (1) If ${\Gamma } \vdash {M}$ then ${\Gamma } = \{{l}_{i}:\alpha _{i}^{i \in I}\}$ where $\alpha _{i} = \{{l}_{p}@A_{i}, p@ \tilde {A}_{i}\}$.

• (2) If ${\Gamma } \vdash _{r} {M}$ then Γ = {l _i : r ^i∈I}@A.

• (3) If ${\Gamma } \vdash _{p} {M}$ then Γ = {l _i : p ^i∈I}@A.

• (4) If ${\Gamma } \vdash _{D} {D}$ then ${\Gamma } = \{{l}_{i} : \alpha _{i}^{i \in I} \} \cup \{{l}_{i} : \beta _{i}^{i \in J}\} \cup \{{l}_{i} : {l}_{p}@A_{i}^{i \in K}\} \cup \{{l}_{i} : p@\tilde {A}_{i}^{i \in L}\}$ where $\alpha _{i} \in \{{l}_{r}@\tilde {A}_{i}, {l}_{r}{l}_{p}@\tilde {A}_{i}\}$ and $\beta _{i} = \{r@\tilde {A}_{i}, rp@A_{i}\}$ .

• (5) If ${\Gamma } \vdash {\textup {\textsf {def}}\ {D} \ \textup {\textsf {in}}\ {M}}$ then ${\Gamma } = \{{l}_{i} : \alpha _{i}^{i \in I} \} \cup \{{l}_{i} : \beta _{i}^{i \in J}\} \cup \{{l}_{i} : {l}_{p}@A_{i}^{i \in K}\} \cup \{{l}_{i} : p@\tilde {A}_{i}^{i \in L}\}$ where $\alpha _{i} \in \{{l}_{r}@\tilde {A}_{i}, {l}_{r}{l}_{p}@\tilde {A}_{i}\}$ and $\beta _{i} = \{r@\tilde {A}_{i}, rp@A_{i}\}$ .

Proof

The proof is tedious but straightforward by typing and combination rules. □

We note $\mathsf {dom_{ln}}({\Gamma }) = \{{l}_{i}^{i \in I}\}$ if ${l}:{l}_{r}@ \tilde {A}, {l}:{l}_{p}@A, {l}:{l}_{r}{l}_{p}@\tilde {A} \in {\Gamma }$ as the set of names denoting linear types: preconditions and postconditions.

Proposition 3 (Associativity of ⊎)

Given ${\Gamma }_{1} = \{{l}_{i} : \alpha _{i}^{i \in I} \} \cup \{{l}_{i} : \beta _{i}^{i \in J}\} \cup \{{l}_{i} : {l}_{p}@A_{i}^{i \in K}\} \cup \{{l}_{i} : p@\tilde {A}_{i}^{i \in L}\}$ , ${\Gamma }_{2} = \{{l}_{i}:p@\tilde {A}_{i}^{i \in N}\} \cup \{{l}_{i}:{l}_{p}@A_{i}^{i \in N^{\prime }}\}$ , ${\Gamma }_{3} = \{{l}_{i}:p@\tilde {A}_{i}^{i \in M}\} \cup \{{l}_{i}:{l}_{p}@A_{i}^{i \in M^{\prime }}\}$ where $\alpha _{i} \in \{{l}_{r}@\tilde {A}_{i}, {l}_{r}{l}_{p}@\tilde {A}_{i}\}$ and $\beta _{i} = \{r@\tilde {A}_{i}, rp@A_{i}\}$ is defined if and only if Γ₁ ⊎ _S (Γ₂ ⊎Γ₃)is defined, (Γ₁ ⊎ _S Γ₂) ⊎Γ₃ = Γ₁ ⊎ _S (Γ₂ ⊎Γ₃)and $\mathsf {dom_{ln}}({\Gamma }_{1}) \cap \mathsf {dom_{ln}}({\Gamma }_{2}) \cap \mathsf {dom_{ln}}({\Gamma }_{3}) = \emptyset$ .

Proof

Case analysis on the membership of type assertions in Γ₁,Γ₂and Γ₃. We give the proofof “if (Γ₁ ⊎ _S Γ₂) ⊎Γ₃is definedthen Γ₁ ⊎ _S (Γ₂ ⊎Γ₃)is defined”.The proof of “if Γ₁ ⊎ _S (Γ₂ ⊎Γ₃)is defined then (Γ₁ ⊎ _S Γ₂) ⊎Γ₃is defined” is symmetric.

Case l :

∈ d o m(Γ₁), d o m(Γ₂), d o m(Γ₃).We have that ${\Gamma }_{1}({l}) \in \{{l}_{r}@\tilde {A}, {l}_{r}{l}_{p}@\tilde {A}, {l}_{p}@A, r@\tilde {A}$,$rp@A, p@\tilde {A}\}, {\Gamma }_{2}({l}) \in \{{l}_{p}@B, p@\tilde {B}\}$,${\Gamma }_{3}({l}) \in \{{l}_{p}@C, p@\tilde {C}\}$.$\{{l}_{r}@\tilde {A}, {l}_{r}{l}_{p}@\tilde {A}, {l}_{p}@A$,$r@\tilde {A}, rp@A, p@\tilde {A}\} \uplus _{S} \{{l}_{p}@B$,$p@\tilde {B}\}$is defined by assumption and the result is $\{{l}_{r}{l}_{p}@\{\tilde {A}, B\}$,${l}_{p}@A, rp@\{A, B\}, p@\{\tilde {A}, B\}\}$by definition of combination rules. Next, we have that$\{{l}_{r}{l}_{p}@\{\tilde {A}, B\}, {l}_{p}@A, rp@\{A, B\}$,$p@\{\tilde {A}, \tilde {B}\}\} \uplus \{{l}_{p}@C, p@\tilde {C}\}$is defined only for the nonlinear names $\{rp@A, p@\{\tilde {A}, \tilde {B}, \tilde {C}\}\}$.Two linear types and, one linear and one nonlinear do notcombine by definition. On the other side, we have that (Γ₁ ⊎ _S (Γ₂⊎Γ₃))(l) =Γ₁(l)⊎ _S (Γ₂⊎Γ₃)(l) =Γ₁(l)⊎ _S (Γ₂(l)⊎Γ₃(l)).In here, $\{{l}_{p}@B, p@\tilde {B}\} \uplus \{{l}_{p}@C, p@\tilde {C}\}$is defined only for nonlinear events by hypothesis, resulting in$\{p@\{\tilde {B}, \tilde {C}\}\}$.$\{{l}_{r}@\tilde {A}, {l}_{r}{l}_{p}@\tilde {A}, {l}_{p}@A$,$r@\tilde {A}, rp@A, p@\tilde {A}\} \uplus _{S} \{p@\{\tilde {B}, \tilde {C}\}\}$is defined only for nonlinear events, resulting in {r p@A,$p@\{\tilde {A}, \tilde {B}, \tilde {C}\}\}$.

Case l :

∈ d o m(Γ₁), d o m(Γ₂), l∉d o m(Γ₃).So, ((Γ₁ ⊎ _S Γ₂)⊎Γ₃)(l) = (Γ₁ ⊎ _S Γ₂)(l) =Γ₁(l)⊎ _S Γ₂(l)is defined by assumption. On the other side, we have that (Γ₁ ⊎ _S (Γ₂ ⊎Γ₃)) (l) =Γ₁(l) ⊎ _S (Γ₂ ⊎Γ₃)(l) =Γ₁(l) ⊎ _S Γ₂(l)is defined by hypothesis.

Cases l :

∈ d o m(Γ₁), d o m(Γ₃), l∉d o m(Γ₂)and l ∈ d o m(Γ₂), d o m(Γ₃), l∉d o m(Γ₁)are similar to the one above.

Cases l :

∈ d o m(Γ₁), l∉d o m(Γ₂), d o m(Γ₃)and l ∈ d o m(Γ₂), l∉d o m(Γ₁), d o m(Γ₃)and l ∈ d o m(Γ₃), l∉d o m(Γ₂), d o m(Γ₁) are trivial.

□

Lemma 2 (Subject congruence)

If P ≡ Q then ${\Gamma } \vdash {P}$ iff ${\Gamma } \vdash {Q}$ .

Proof

By induction on the proof of P ≡ Q.We present only the case for rule ⌊STR-DEF⌋.Other cases are trivial. □

Case(Rule STR-DEF)

$$({\textup{\textsf{def}}\ {D} \ \textup{\textsf{in}}\ {M}_{1}})\ \textsf{\&}\, {M}_{2} \equiv {\textup{\textsf{def}}\ {D} \ \textup{\textsf{in}}\ ({M}_{1}\ \textsf{\&}\, {M}_{2})} $$

$$\begin{array}{@{}rcl@{}} &&{\Gamma} \vdash {(\textup{\textsf{def}}\ {D} \ \textup{\textsf{in}}\ {M}_{1}})\ \textsf{\&}\, {M}_{2} \text{Assumption}\\ &&{\Gamma}_{1} \vdash {\textup{\textsf{def}}\ {D} \ \textup{\textsf{in}}\ {M}_{1}}~\text{and}~{\Gamma}_{2} \vdash {M}_{2}~\text{where}~{\Gamma} = {\Gamma}_{1} \uplus {\Gamma}_{2}~\text{is defined} \text{{B}y inversion}\\ &&{\Gamma}_{3} \vdash_{D} {D}~\text{and}~{\Gamma}_{4} \vdash {M}_{1}~\text{where}~{\Gamma}_{1} = {\Gamma}_{3} \uplus_{S} {\Gamma}_{4}~\text{is defined}\text{By inversion}\\ &&{\Gamma}_{2} = \{{l}_{i}:\alpha_{i}^{i \in I}\}, {\Gamma}_{4} = \{{l}_{i}:\alpha_{i}^{i \in I^{\prime}}\}~\text{where}~\alpha_{i} \in \{{l}_{p}@\tilde{A}_{i}, p@\tilde{A}_{i}\} \text{By Prop. 1(1)}\\ &&{\Gamma}_{2} \uplus {\Gamma}_{4}~\text{is defined}~\text{By Prop. 3} \\ &&{\Gamma}_{2} \uplus {\Gamma}_{4} \vdash {M}_{1}\ \textsf{\&}\, {M}_{2}\text{{B}y rule } {\lfloor{\textsc{T-GPar}}\rfloor}\\ &&{\Gamma}_{3} = \{{C}_{i} : \alpha^{i \in I} \} \cup \{{l}_{i} : \beta^{i \in J}\} \cup \{{C}^{\prime}_{i} : {l}_{p}^{i \in K}\} \cup \{{l}_{i} : p^{i \in L}\}\\ &&\text{where}~\alpha \in \{{l}_{r}, {l}_{r}{l}_{p}\}~\text{and}~\beta = \{r, rp\}\text{{B}y Prop. 1(4)}\\ &&{\Gamma}_{3} \uplus_{S} ({\Gamma}_{4} \uplus {\Gamma}_{2})~\text{is defined and}~({\Gamma}_{3} \uplus_{S} {\Gamma}_{4}) \uplus {\Gamma}_{2}= {\Gamma}_{3} \uplus_{S} ({\Gamma}_{4} \uplus {\Gamma}_{2})\text{{B}y Prop. 3}\\ &&{\Gamma}_{3} \uplus_{S} ({\Gamma}_{4} \uplus {\Gamma}_{2}) \vdash ({\textsf{def}}\ {D} \ {\textsf{in}}~ {M}_{1})\, \textsf{\&}\, {M}_{2} \text{By rule}~{\lfloor{\textsc{T-Def}}\rfloor}\\ &&\text{Note that}~{\Gamma} = ({\Gamma}_{3} \uplus_{S} {\Gamma}_{4}) \uplus {\Gamma}_{2} \end{array} $$

$$\begin{array}{@{}rcl@{}} &&{\Gamma} \vdash \textup{\textsf{def}}\ {D} \ \textup{\textsf{in}}\ ({M}_{1} \textsf{\&} {M}_{2}) \text{{A}ssumption}\\ &&{\Gamma}_{1} \vdash {D}~\text{and}~{\Gamma}_{2} \vdash {M}_{1}\ \textsf{\&}\, {M}_{2}~\text{where}~{\Gamma} = {\Gamma}_{1} \uplus_{S} {\Gamma}_{2}~\text{is defined}\text{{B}y inversion}\\ &&{\Gamma}_{3} \vdash {M}_{1}~\text{and}~{\Gamma}_{4} \vdash {M}_{2}~\text{where}~{\Gamma}_{2} = {\Gamma}_{3} \uplus {\Gamma}_{4}~\text{is defined} \text{{B}y inversion}\\ &&{\Gamma}_{1} \uplus_{S} {\Gamma}_{3}~\text{is defined}~\text{{B}y Prop. 3}\\ &&{\Gamma}_{1} \uplus_{S} {\Gamma}_{3} \vdash {\textup{\textsf{def}}\ {D} \ \textup{\textsf{in}}\ {M}_{1}}\text{{B}y rule}~{\lfloor\textsc{{T-Def}}\rfloor}\\ &&({\Gamma}_{1} \uplus_{S} {\Gamma}_{3}) \uplus {\Gamma}_{4}~\text{is defined and}~{\Gamma}_{1} \uplus_{S} ({\Gamma}_{3} \uplus {\Gamma}_{4})= ({\Gamma}_{1} \uplus_{S} {\Gamma}_{3}) \uplus {\Gamma}_{4}\text{{B}y Prop. 3}\\ &&({\Gamma}_{1} \uplus_{S} {\Gamma}_{3}) \uplus {\Gamma}_{4} \vdash (\textup{\textsf{def}}\ {D} \ \textup{\textsf{in}}\ {M}_{1})\ \textsf{\&} {M}_{2} \text{{B}y rule}~ {\lfloor\textsc{{T-Par}}\rfloor}\\ &&\text{Note that}~{\Gamma} = {\Gamma}_{1} \uplus_{S} ({\Gamma}_{3} \uplus {\Gamma}_{4}) \end{array} $$

Proposition 4

If $(\{{l}_{i}:{l}_{p}\}^{i \in I}@A, {\Gamma }) \uplus _{S} {\Gamma }^{\prime }$ is defined and $\{l_{i}\}^{i \in I}$ ⊄ $dom({\Gamma }^{\prime })$ where ${\Gamma } = \{{l}_{i}:p@\tilde {A}_{i}\}^{i \in J}, {\Gamma }^{\prime }=\{{l}^{\prime }_{i}:\alpha _{i}\}^{i \in K}$ and $\alpha \in \{{l}_{p}@A, p@\tilde {A}_{i}\}$ then $({l}:\{{l}_{i}:{l}_{p}\}^{i \in I}@A, \{{l}_{i}:p@\tilde {A}_{i}\}^{i \in J}) \uplus \{{l}^{\prime }_{i}:\alpha _{i}\}^{i \in K}$ is defined.

Proof

Straightforward. By$p@\tilde {A}_{i} \uplus p@\tilde {A}_{j} = p@\tilde {A}_{i}, \tilde {A}_{j}$and combination rules. □

Proposition 5

If $(({\Gamma }, \{{l}_{i}:{l}_{r}@\tilde {A}_{i}\}^{i \in I}) \uplus _{H} ({\Gamma }^{\prime }, \{k:{l}_{p}@A_{i}\}^{i \in J})) \uplus _{S} ({\Gamma }_{1} \uplus {\Gamma }_{1}^{\prime })$ is defined, and {k}^i∈J ⊄$dom{({\Gamma }_{1}^{\prime })}$ then $(({\Gamma }, \{{l}_{i}:{l}_{r}@\tilde {A}_{i}\}^{i \in I}) \uplus _{H} ({\Gamma }^{\prime }, \{k:{l}_{p}@A_{i}\}^{i \in J})) \uplus _{S} (\{k:{l}_{p}@A_{i}\}^{i \in J},{\Gamma }^{\prime } \uplus {\Gamma }_{1}^{\prime })$ is defined.

Proof

By assumption {k}^i∈J ⊄ $dom{({\Gamma }_{1}^{\prime })}$then $\{{k}:{l}_{p}@A_{i}\}^{i \in J} \uplus {\Gamma }_{1}^{\prime }$is defined. We must show that assumptions of linear types in${\Gamma }_{1}^{\prime }$are not on names appearing as well on assumptions of nonlinear${\Gamma }^{\prime }$. By Prop. 3, we have that $(({\Gamma }, \{{l}_{i}:{l}_{r}@\tilde {A}_{i}\}^{i \in I}) \uplus _{H} ({\Gamma }^{\prime }, \{{k}:{l}_{p}@A_{i}\}^{i \in J})) \uplus _{S} ({\Gamma }_{1} \uplus {\Gamma }_{1}^{\prime }) = (({\Gamma }, \{{l}_{i}:{l}_{r}@\tilde {A}_{i}\}^{i \in I}) \uplus _{H} ({\Gamma }^{\prime }, \{{k}:{l}_{p}@A_{i}\}^{i \in J})\uplus {\Gamma }_{1}^{\prime }) \uplus _{S} {\Gamma }_{1}$.This implies that $({\Gamma }^{\prime }, \{{k}:{l}_{p}@A_{i}\}^{i \in J})\uplus {\Gamma }_{1}^{\prime }$is defined. By Prop 4, we conclude that $({\Gamma }^{\prime }, \{{k}:{l}_{p}@A_{i}\}^{i \in J})\uplus {\Gamma }_{1}^{\prime }$is defined. From here, one can easily conclude that$(({\Gamma }, \{{l}_{i}:{l}_{r}@\tilde {A}_{i}\}^{i \in I}) \uplus _{H} ({\Gamma }^{\prime }, \{{k}:{l}_{p}@A_{i}\}^{i \in J})) \uplus _{S} (\{{k}:{l}_{p}@A_{i}\}^{i \in J},{\Gamma }^{\prime } \uplus {\Gamma }_{1}^{\prime })$ is defined. □

Proposition 6

If (Γ₁ ⊎ _D Γ₂) ⊎ _S Γ₃ is defined then Γ₁ ⊎ _S Γ₃ is defined.

Proof

Straightforward since Γ₁ ⊎ _D Γ₂(l) ∈ {l _r , l _r l _p , r, r p, l _p , p}and Γ₁(l) ∈ {l _r , l _r l _p , r, r p, l _p , p}. □

Theorem 4 (Subject reduction)

If ${\Gamma } \vdash {P}$ and P → Q then ${\Gamma } \vdash {Q}$ .

Proof

We use induction on the derivation of P → Q. □

Case(R-Occ)

$$\begin{array}{@{}rcl@{}} && {\textsf{def}}\ {[{J}_{1}]}\ \textsf{\&}\, {J}_{2}\, \rhd\, [ {J}_{3}] \ \textsf{\&}\, {J}_{4}~ {\textsf{in}}\ ({{J}}_{1}\ \textsf{\&}\ {J}_{2}\ \textsf{\&}\, {M}) \longrightarrow {\textsf{def}}\ [{J}_{\textsf{1}}]\ \textsf{\&}\ {J}_{2}\, \rhd\, [{J}_{3}]\ \textsf{\&}\, {J}_{4}~{\textsf{in}}\ ({{J}}_{3}\ \textsf{\&}\, {J}_{4}\ \textsf{\&}\, {M})\\ && fn(J_{3}) \cap fn({M}) = \emptyset \end{array} $$

$$\begin{array}{@{}rcl@{}} &&{\Gamma} \vdash {\textsf{def}}\ [{J}_1]\ \textsf{\&}\ {J}_{2}\, \rhd\, {[{J}_3]}\ \textsf{\&}\, {J}_{4}\ {\textsf{in}}\ ({{J}}_{1}\ \textsf{\&}\ {J}_{2}\ \textsf{\&}\ {M}) \text{{A}ssumption} \\ &&{\Gamma}_{1} \vdash [{J}_1]\ \textsf{\&}\, {J}_{2}\, \rhd\, {[{J}_3]}\ \textsf{\&}\, {J}_{4}~\text{and}~{\Gamma}_{2} \vdash ({{J}}_{1}\ \textsf{\&}\ {J}_{2}\ \textsf{\&}\ {M})\\ &&\text{where}~{\Gamma} = {\Gamma}_{1} \uplus_{S} {\Gamma}_{2}~\text{is defined} \text{By inversion}\\ &&{\Gamma}_{2}^{\prime} \vdash {{J}}_{1}\ \textsf{\&}\, {J}_{2}~\text{and}~{\Gamma}_{2}^{\prime\prime} \vdash {M}~\text{where}~{\Gamma}_{2} = {\Gamma}_{2}^{\prime} \uplus {\Gamma}_{2}^{\prime\prime}~\text{is defined} \text{{B}y inversion}\\ &&{\Gamma}_{3} \vdash_{pre} {J}_{1}, {\Gamma}_{4} \vdash_{r} {J}_{2}, {\Gamma}_{5} \vdash_{post} {J}_{3}~\text{and}~{\Gamma}_{6} \vdash_{p} {J}_{4} \\ &&{\Gamma}_{1} = ({\Gamma}_{3} \uplus_{rea} {\Gamma}_{4}) \uplus_{H} ({\Gamma}_{5} \uplus_{pro} {\Gamma}_{6})~\text{is defined} \text{{B}y inversion}\\ &&{\Gamma}_{3}, {\Gamma}_{4}~\text{and}~{\Gamma}_{5}, {\Gamma}_{6} \text{By rules in Fig. 6}\\ &&{\Gamma}_{5} = \{{l}_{i}:{l}_{p}\}^{i \in J}@A \quad {\Gamma}_{6} = \{{l}_{i}:p\}^{i \in I}@A \text{By Lemma 1(2)}\\ &&{\Gamma}_{5} \uplus {\Gamma}_{6} \vdash {J}_{1}\ \textsf{\&}\, {J}_{2}\text{{B}y rule}~{\lfloor\textsc{{T-Par}}\rfloor}\\ &&{\Gamma}_{5} \uplus {\Gamma}_{6} \uplus {\Gamma}_{2}^{\prime\prime}~\text{is defined}\text{{B}y Prop 4}\\ &&{\Gamma}_{6} \uplus {\Gamma}_{5} \uplus {\Gamma}_{2}^{\prime\prime}\vdash {J}_{1}\ \textsf{\&}\, {J}_{2}\ \textsf{\&}\, {M} \text{{B}y rule}~{\lfloor{\textsc{T-Par}}\rfloor}\\ &&{\Gamma}^{\prime} = (({\Gamma}_{3} \uplus_{rea} {\Gamma}_{4}) \uplus_{H} ({\Gamma}_{4} \uplus_{pro} {\Gamma}_{5})) \uplus_{S} ({\Gamma}_{5} \uplus {\Gamma}_{6} \uplus {\Gamma}_{2}^{\prime\prime})~\text{is defined} \text{By Prop. 5}\\ &&{\Gamma}^{\prime} \vdash {\textsf{def}}\ [{J}_1]\ \textsf{\&}\, {J}_{2}\, \rhd\, [{J}_3]\ \textsf{\&}\, {J}_{4}\ {\textsf{in}}\ ({{J}}_{3}\ \textsf{\&}\, {J}_{4}\ \textsf{\&}\, {M}) \text{{B}y rule}~{\lfloor{\textsc{T-Def}}\rfloor} \end{array} $$

Note that $(({\Gamma }_{3} \uplus _{rea} {\Gamma }_{4}) \uplus _{H} ({\Gamma }_{4} \uplus _{pro} {\Gamma }_{5})) \uplus _{S} ({\Gamma }_{2}^{\prime } \uplus {\Gamma }_{2}^{\prime \prime }) = (({\Gamma }_{3} \uplus _{rea} {\Gamma }_{4}) \uplus _{H} ({\Gamma }_{4} \uplus _{pro} {\Gamma }_{5})) \uplus _{S} ({\Gamma }_{5} \uplus {\Gamma }_{6} \uplus {\Gamma }_{2}^{\prime \prime })$.

Case(Rule R-AddPre)

$${{l}\ \textsf{\&}~ {\textsf{def}}\ \textsf{[}{J}_{1}\textsf{]}\ \textsf{\&}\, {J}_{2}\, {{\rhd}}\, \textsf{[}{J}_{3}\textsf{]}\ \textsf{\&~} {J}_{4}\ {\textsf{in}}\ {M} \longrightarrow\ {\textsf{def}}\ \textsf{[}{J}_{1}\textsf{]}\ \textsf{\&}\, {J}_{2}\, {{\rhd}}\, \textsf{[}{J}_{3}\textsf{]}\ \textsf{\&}\, {J}_{4}~\textsf{in}\ ({l}\ \textsf{\&}\, {M})}\quad {l}\ \in\ dn({J}_{1}) $$

$$\begin{array}{@{}rcl@{}} &&{\Gamma} \vdash {l}\ \textsf{\&}~ \textsf{def}\ \textsf{[}{J}_1\textsf{]}\ \textsf{\&}\, {J}_{2}\, {{\rhd}}\, \textsf{[}{J}_3\textsf{]}\ \textsf{\&}\, {J}_{4}\ \textsf{in}\ {M}~\text{and}~{l}\in{dn}({J}_{1}) \text{{A}ssumption}\\ &&{\Gamma}_{1} \vdash {l}~\text{and}~{\Gamma}_{2} \vdash {\textsf{def}}\ \textsf{[}{J}_1\textsf{]}\ \textsf{\&}\, {J}_{2} \,{{\rhd}}\, \textsf{[}{J}_3\textsf{]}\ \textsf{\&}\ {J}_{4}\ \textsf{in}\ {M}\\ &&\text{where}~{\Gamma} = {\Gamma}_{1} \uplus {\Gamma}_{2}~\text{is defined}\text{{B}y inversion}\\ &&{\Gamma}_{1} = {l}: {l}_{p}\text{{B}y Lemma 1(1)}\\ &&{\Gamma}_{3} \vdash \textsf{[}{J}_1\textsf{]}\ \textsf{\&}~{J}_{2}\, {{\rhd}}\,\textsf{[}{J}_3\textsf{]}\ \textsf{\&}~ {J}_{4}~\text{and}~{\Gamma}_{4} \vdash {M}, \text{where}~{\Gamma}_{2} = {\Gamma}_{3} \uplus_{S} {\Gamma}_{4}~\text{is defined} \text{{B}y inversion}\\ &&{\Gamma}_{4} = \{{l}_{i}:{l}_{p}^{i \in N}\}\text{{B}y Lemma 1(1)}\\ &&{\Gamma}_{4} \uplus {l}:{l}_{p}~\text{is defined} \text{{B}y Prop 3}\\ &&{\Gamma}_{4} \uplus {l}:{l}_{p} \vdash {M}\ \textsf{\&}~ {l} \text{By rule}~\lfloor{\textsc{T-Par}}\rfloor\\ &&{\Gamma}_{3} \uplus_{S} ({\Gamma}_{4} \uplus {l}:{l}_{p})~\text{is defined}\text{{B}y Prop 3}\\ &&{\Gamma}_{3} \uplus_{S} ({\Gamma}_{4} \uplus {l}:{l}_{p}) \vdash {\textsf{def}}\ \textsf{[}{J}_1{]} ~\textsf{\&}\, {J}_{2}\, {{\rhd}}\, \textsf{[}{J}_3{]}\ \textsf{\&}\, {J}_{4}\ \textup{\textsf{in}}\ {l}\ \textsf{\&}\, {M}\text{{B}y rule}~{\lfloor{\textsc{T-Def}}\rfloor} \end{array} $$

One can easily observe that ${\Gamma } = {\Gamma }^{\prime }$.

Case(Rule R-DisO)

$$\textup{\textsf{def}}\ {D}\ \textup{\textsf{or}}\ {E}\ \textup{\textsf{in}}\ {M}\ \longrightarrow\ \textup{\textsf{def}}\ {D}\ \textup{\textsf{or}}\ {E}\ \textup{\textsf{in}}\ {M}^{\prime} \text{ if}~ \textup{\textsf{def}}\ {D}\ \textup{\textsf{in}}\ {M}\ \longrightarrow\ \textup{\textsf{def}}\ {D}\ \textup{\textsf{in}}\ {M}^{\prime} $$

$$\begin{array}{@{}rcl@{}} &&{\Gamma} \vdash \textup{\textsf{def}}\ {D}\ \textup{\textsf{or}}\ {E}\ \textup{\textsf{in}}\ {M} \text{{A}ssumption}\\ &&{\Gamma}_{1} \vdash {D}\ \textup{\textsf{or}}\ {E}~\text{and}~{\Gamma}_{2} \vdash {M}~\text{where}~{\Gamma} = {\Gamma}_{1} \uplus_{S} {\Gamma}_{2}~\text{is defined} \text{{B}y inversion}\\ &&{\Gamma}_{3} \vdash {D}~\text{and}~{\Gamma}_{4} \vdash {E}~\text{where}~{\Gamma}_{1} = {\Gamma}_{3} \uplus_{D} {\Gamma}_{4}~\text{is defined}\text{{B}y inversion}\\ &&{\Gamma}_{2} \uplus_{S} {\Gamma}_{3}~\text{is defined} \text{{B}y Prop 6}\\ &&{\Gamma}_{2} \uplus_{S} {\Gamma}_{3} \vdash \textup{\textsf{def}}\ {D}\ \textup{\textsf{in}}\ {M}\text{{B}y rule}~{\lfloor\textsc{{T-Def}}\rfloor}\\ &&{\Gamma}_{5}^{\prime} \vdash \textup{\textsf{def}}\ {D}\ \textup{\textsf{in}}\ {M}^{\prime}~\text{for}~{\Gamma}_{5} = {\Gamma}_{2} \uplus_{S} {\Gamma}_{3} \text{By induction}\\ &&{\Gamma}_{6} \vdash {D}~\text{and}~{\Gamma}_{7} \vdash {M}^{\prime} \text{By inversion}\\ &&\text{where}~{\Gamma}_{5} = {\Gamma}_{6} \uplus_{S} {\Gamma}_{7}~\text{and}~{\Gamma}_{6} = {\Gamma}_{3}~\text{so}~{\Gamma}_{2} \uplus_{S} {\Gamma}_{3} = {\Gamma}_{3} \uplus_{S} {\Gamma}_{7}\\ &&({\Gamma}_{3} \uplus_{D} {\Gamma}_{4}) \uplus_{S} {\Gamma}_{7}~\text{is defined}~\text{{B}y Prop 5}\\ &&({\Gamma}_{3} \uplus_{D} {\Gamma}_{4}) \uplus_{S} {\Gamma}_{7} \vdash \textup{\textsf{def}}\ {D}\ \textup{\textsf{or}}\ {E}\ \textup{\textsf{in}}\ {M}^{\prime} \text{By rule}~{\lfloor{\textsc{T-Def}}\rfloor} \end{array} $$

One can easily observe that by having Γ₂ ⊎ _S Γ₃ =Γ₇ ⊎ _S Γ₃, once can conclude that by extending Γ₃ with other handlers Γ₄ that are compatible by assumption then Γ₂ ⊎ _S (Γ₃ ⊎ _D Γ₄) =Γ₇ ⊎ _S (Γ₃ ⊎ _D Γ₄).

Case(Rule R-Par)

$${P}\ \textsf{\&}\, {Q}\ \longrightarrow\ {P}^{\prime}\ \textsf{\&}\, {Q} \text{ if}~ {P} \longrightarrow {P}^{\prime} $$

$$\begin{array}{@{}rcl@{}} &&{\Gamma} \vdash {P}\ \textsf{\&}\, {Q}\text{{A}ssumption}\\ &&{\Gamma}_{1} \vdash {P} \; \; {\Gamma}_{2} \vdash {Q}~\text{for}~{\Gamma} = {\Gamma}_{1} \uplus {\Gamma}_{2} \text{{B}y inversion}\\ &&{\Gamma}_{1} \vdash {P}^{\prime} \text{{B}y induction}\\ &&{\Gamma}_{1} \uplus {\Gamma}_{2} \vdash {P}^{\prime}\ \textsf{\&} {Q} \text{By rule}~{\lfloor{\textsc{T-Par}}\rfloor} \end{array} $$

Case(Rule R-Struct)

$${P}\ \longrightarrow\ {P}^{\prime} \text{ if } {P} \equiv {Q} \text{ and } {Q} \longrightarrow {Q}^{\prime}~and~ {Q}^{\prime} \equiv {P}^{\prime} $$

$$\begin{array}{@{}rcl@{}} &&{\Gamma} \vdash {P} \text{{A}ssumption}\\ &&{\Gamma} \vdash {Q} \text{{B}y Lemma 2}\\ &&{\Gamma} \vdash {Q}^{\prime} \text{{B}y induction}\\ &&{\Gamma} \vdash {P}^{\prime} \text{By Lemma 2} \end{array} $$

Theorem 5 (Subject reduction for programs)

If $\emptyset {\vdash _{flows}} {P}$ and P → Q then $\emptyset {\vdash _{flows}} {Q}$

Proof

Follows as a corollary from Subject reduction Theorem 4. □

Theorem 6 (Migration safety)

Suppose ${\Gamma } \vdash {P}$ then for adding l to ${\mathcal {E}}$ where P $\equiv {\mathcal {E}}[{l}]$ such that either $\mathcal {E}$ contains:

• 1. exactly one ${\mathcal {E}}_{pre}\langle {l} \rangle$ and l = i n i t

• 2. exactly one pair of $\mathcal {E}_{post}\langle {l} \rangle$ and $\mathcal {E}_{pre}\langle {l} \rangle$

• 3. exactly one $\mathcal {E}_{post}\langle {l} \rangle$ and many $\mathcal {E}_{pre}\langle {l} \rangle$ in only one site

• 4. many $\mathcal {E}_{r}\langle {l} \rangle$ of the same flow

• 5. many $\mathcal {E}_{r}\langle {l} \rangle$ and many $\mathcal {E}_{p}\langle {l} \rangle$ of the same flow

• 6. exactly one $\mathcal {E}_{r}\langle {l} \rangle$ and many $\mathcal {E}_{p}\langle {l} \rangle$ of different flows

Proof

Let P ≡ l & P ₀ & Q where P ₀does not containglobal events and Q contains global events. By rule induction, we prove that P ₀ has aname l as a reactant at a reaction of a site or a precondition or a pair of a precondition and postcondition orpairs of a reactant and products.

Case:

(⌊T-GName⌋, ⌊T-RGName⌋, ⌊T-Site⌋, ⌊T-Handler⌋, ⌊T-Dis⌋, ⌊T-GPar⌋, ⌊T-PPar⌋, ⌊T-RPar⌋):Vacuous since the terms do not reduce at l.

Case:

(⌊T-Par⌋): Suppose ${\Gamma } \vdash {P}$ and ${\Gamma }^{\prime } \vdash {Q}$suchthat ${\Gamma } \uplus {\Gamma }^{\prime }$is defined. By induction hypothesis, we can assume that P and Q satisfy the required condition.

• 1. If only one party reduces at l then we conclude.

• 2. If both processes reduce at l,hence Γand ${\Gamma }^{\prime }$,respectively, have a precondition or reactant at l and P and Q are not of the same flow. Then, ${\Gamma } \uplus {\Gamma }^{\prime }$cannot not be defined by combination rules of ⊎.

□

Theorem 7 (Progress)

If $\emptyset \vdash _{flows} {P}$ and P is simple then P $\longrightarrow {P}^{\prime }$ or inactive.

Proof

By induction on the derivation of the typing judgment.

Case

$$\frac{\Gamma \vdash {P} \quad {\Gamma} = \{{l}_{i}:{{l}_{r}{l}_{p}}/rp/{l}_{p}/p @{\Delta}_{i}\}^{i \in I}}{\emptyset \vdash_{flows} {P}}\;\;{{\lfloor\textsc{{T-flows}}\rfloor}} $$

$${\Gamma} \vdash {P} \quad {\Gamma} = \{{l}_{i}:{{l}_{r}{l}_{p}}/rp/{l}_{p}/p @{\Delta}_{i}\}^{i \in I} \text{By inversion} $$

By induction on the derivation of the typing judgment, analyzing all possible cases, we prove thatgiven ${\Gamma } \vdash {P}$ and ${\Gamma } = \{{l}_{i}:{{l}_{r}{l}_{p}}/rp/{l}_{p}/p @{\Delta }_{i}\}^{i \in I}$ and P is simple then $P \longrightarrow {P}^{\prime }$or inactive.

Cases ⌊T-Dis⌋, ⌊T-Hand⌋, ⌊TInact⌋, ⌊T-PrePar⌋, ⌊T-RPar⌋, ⌊T-PostPar⌋, ⌊T-PPar⌋, ⌊T-PreName⌋, ⌊T-RName⌋, ⌊T-PostName⌋ and ⌊T-PName⌋ are vacuous.

Case

$$ \frac{\Gamma \vdash {P} \quad {\Gamma}^{\prime} \vdash {Q}}{\Gamma \uplus {\Gamma}^{\prime} \vdash {P}\ \textsf{\&}\ {Q}}\;\;{\lfloor\textsc{{T-Par}}\rfloor} $$

$$\begin{array}{@{}rcl@{}} &&{\Gamma} \uplus {\Gamma}^{\prime} \vdash {P}\ \textsf{\&}\, {Q} \text{By assumption}\\ &&{P}\ \textsf{\&}\, {Q} = {l}\ \textsf{\&}\, (\textup{\textsf{def}}\ {D}_{1}\ \textup{\textsf{in}}\ {M}_{1})\textsf{\&} ...\ \textsf{\&} ...\ (\textup{\textsf{def}}\ {D}_{n}\ \textup{\textsf{in}}\ {M}_{n})\text{First subcase}\\ &&{P} \textsf{\&} {Q} \rightarrow {P} \textsf{\&} {Q} \text{By Theorem 6}\\ &&{\Gamma} \vdash {P} \quad {\Gamma}^{\prime} \vdash {Q} \text{{B}y inversion}\\ &&{P} \rightarrow {P}^{\prime} \text{First subcase}\\ &&{{{P}\ \textsf{\&}\, {Q}\ \longrightarrow\ {P}^{\prime}\ \textsf{\&}\, {Q}} \ \ \text{if}\ \ {{P}\ \longrightarrow\ {P}^{\prime}}} \text{{B}y rule}~{\lfloor\textsc{R-Par}\rfloor}\\ &&{P}\ \text{is\ inactive} \text{Second subcase}\\ &&{Q} \rightarrow {Q}^{\prime} \text{First subsubcase}\\ &&{P}\ \textsf{\&}\, {Q} \rightarrow {P}\ \textsf{\&}\, {Q}^{\prime} \text{By rule}~{\lfloor\textsc{R-Par}\rfloor}\\ &&{Q}\ \text{is\ inactive} \text{Second subsubcase}\\ &&{P}\ \textsf{\&} {Q} \text{ is\ inactive} \end{array} $$

Case

$$\frac{\Gamma \vdash {D} \quad {\Gamma}^{\prime} \vdash {M}}{\Gamma \uplus_{S} {\Gamma}^{\prime} \vdash \textup{\textsf{def}}\ {D}\ \textup{\textsf{in}}\ {M}}\;\; {\lfloor\textsc{{T-Site}}\rfloor} $$

$$\begin{array}{@{}rcl@{}} &&{\Gamma} \uplus_{S} {\Gamma}^{\prime} \vdash \textup{\textsf{def}}\ {D}\ \textup{\textsf{in}}\ {M}\text{By assumption}\\ &&{{\textup{\textsf{def}}\ {D}\ \textup{\textsf{in}}\ {M}\ {\longrightarrow}\ \textup{\textsf{def}}\ {D}\ \textup{\textsf{in}}\ {M}^{\prime}}} \text{By rule}~{\lfloor\textsc{{R-Occ}}\rfloor}\\ &&\textup{\textsf{def}}\ {D}\ \textup{\textsf{in}}\ {M}~\text{is inactive} \text{Second subcase} \end{array} $$

Case

$${{init}:{l}_{p}@[] \vdash {init}} \;\;{\lfloor\textsc{{T-Init}}\rfloor} $$

$$\begin{array}{@{}rcl@{}} &&{init}:{l}_{p}@[] \vdash {init} \text{By assumption}\\ &&\text{We have that}~{init}~\text{is}~\textit{inactive}. \end{array} $$

Similarly for rule ⌊T-GName⌋.

□