A Polymorphic Type and Effect System for Detecting Mobile Functions

Z. Dilsun Kırlı^{∗}

Laboratory for Foundations of Computer Science, The University of Edinburgh, King’s Buildings, Mayfield Road, Edinburgh, EH9 3JZ, Scotland, UK.

Abstract

We define a language with a functional core and constructs for transmitting and receiving values across remote sites in which mobile agents have a natural representation as function closures. We present the dynamic semantics of this language in relational style. We develop a static type and effect system where the types are annotated so that the effects expose potentially mobile functions and channels. Finally, we prove the consistency of this system with respect to the dynamic semantics. Key words Functional languages, mobile computation, program analysis, type and effect systems, Facile

1 Introduction

Functional computation has some characteristics which make it promising to adopt a functional language as the core of a mobile computation language. One such characteristic is that functions are first-class values. They can flow as arguments to other functions or they can be returned as results. In a setting where their communication between different sites is facilitated, functions become a natural candidate for representing mobile agents since they are code containing objects capable of enhancing the dynamic behaviour of a system. It is also the case that expressive and well understood type systems have been defined for functional languages. In a setting where functions can be viewed as mobile agents, this fact implies that one can express a wide range of agents and yet be able to reason about their behaviour by exploiting the type system of the language in which they are written.

∗e-mail: zdk@dcs.ed.ac.uk. tel:+44 131 650 48 89

Facile [28, 6] is a language which encompasses the above mentioned characteristics. It is based on a well defined computational model which combines Standard ML [16] with a model of concurrency based on CCS [14] and its higher-order mobile extensions such as CHOCS [26] and the π-calculus [15]. It facilitates the transmission of first-class values including channels and functions over typed channels. Therefore, it is an apt choice to consider a Facile-like language when focusing on a particular problem relevant to mobile computation with mobile functions. In this paper, we focus on the static estimation of potentially mobile functions and channels. We investigate this problem within the framework of a Facile-like language.

Estimation of mobile entities can be useful for compiler-optimisations. We can provide supporting evidence for this argument by considering the implementation of the Facile language by Knabe [11] which facilitates the transmission of mobile agents across a network of heterogeneous nodes. In this language, users are required to provide annotations to identify potentially mobile functions so that the compiler generates a standard transmissible representation for these functions. The code for the functions which are immobile can be optimised for the local machine and the compiler need not generate and store a standard transmissible representation for them. A static analysis which estimates potentially mobile functions would make it possible to generate annotations automatically relieving the programmer from having to provide annotations and reducing the risks of errors due to omitted annotations.

Another area where information with respect to mobile entities can be put to use is providing a profile of a program so that programmers can statically reason about the transmission overhead their programs are likely to incur. In Facile and most higher-order languages, a function is compiled into a function closure which contains the code of the function together with the bindings from the definition environment of the function. According to the data space management policy employed by the implementation of Facile, transmission of a function occurs by copying of its closure to the destination site. Channels in Facile reside on the node where they were created. Their transmission requires that a network reference to them be established and maintained. Therefore, a profiler which estimates mobile functions and channels can be considered to estimate the cost of copying closures and network references. The latter can be particularly useful in that minimising network references is a key motivation for adopting mobile computation.

The problem of detecting mobile functions and channels is closely related to detecting the flow of control from one program point to another. So far we have considered the higher-order features in a positive light due to their expressive power. However, their presence poses challenges in detecting the flow of control. The literature contains a wide range of analyses which have been devised to approximate the functions which can be called from a particular point in a program [23, 5, 17, 8]. Some authors have pointed out the intuitive connection between reasoning about types and control flow in higher-order languages in the sense that they both derive invariants about the potential bindings of variables in a program. Research has been carried out in extending control flow systems to perform type analyses [21] and in extending type systems to perform control flow analyses [32]. Another direction of research has focused on systematic comparisons of type systems and control flow systems by establishing correspondences between certain type systems and control flow analyses [7, 20]. Drawing inspiration from these, we develop a type and effect system which conservatively estimates the set of functions and channels which may be transmitted by an expression in our Facile-like language.

Section 2 motivates the problem by an informal discussion and examples. Section 3 introduces the language on which our discussion is based. The type and effect system is defined in Section 4. Section 5 shows our approach to proving the soundness of our type and effect system. The following sections discuss the contributions of our work by referring to related work in the literature along with possible future directions.

2 Potential Mobility

In this section we define informally what is meant by potential mobility of functions and channels throughout the paper. We follow closely the criteria determined by Knabe to guide programmers in annotating potentially mobile functions in his implementation of Facile. The examples are also inspired by the discussion in his dissertation [11]. In the following section we will define a formal language which is suggestive of an intermediate language for Facilelike languages. For the purposes of this section, it is sufficient to note that the language has operators ! and ? corresponding to sending and receiving a value.

2.1 Mobile Functions

It should be relatively clear that any function which is passed directly to a send operator is potentially mobile. Whenever a function f moves, it takes with it the functions contained in its closure. Therefore, we can argue that a function which is referred to by a mobile function and which is not defined within it is also mobile. The functions which are defined within function f are mobile only by virtue of being a part of its code. Detecting the mobility of f implies the mobility of functions nested within its body. Therefore, we need not consider these as mobile functions individually.

If the above criteria were sufficient, all the information needed for automatic detection of mobile functions would be available in the definition environment component of the function closure which contains the bindings of free identifiers referred to by the code. However, in the presence of higherorder functions, one needs to go beyond the information provided by the function closure. The following examples illustrate this point.

Example 1

Let us consider a function f defined as follows.

fun f h = let fun g x = ... h x ...

in

chan ! g end

Obviously, g is potentially mobile. We can also deduce that h stands for a function referred to by g. The difficulty arises from the fact that h is a bound variable. In such a situation, all the functions which h can be bound to, in other words all the functions which f can be applied to, are potentially mobile. Detecting these functions is not straightforward since one needs to consider cases such as the following.

fun k x = ... f a ...  (∗ a will be mobile ∗)
fun k x = ... f x ...  (∗ any possible binding of x will be mobile ∗)

fun k x = ... x a ...

... k f ...  (∗ a will be mobile ∗)

fun k h y = ... h y ...

... k f ...  (∗ any possible binding of y will be mobile ∗)

Example 2

A similar difficulty arises when a higher-order function is transmitted. Let us consider an expression which transmits a function f defined as follows. let

fun f x = let fun g y = ... x ... y ...

in g end

in

chan ! f end

The function f is potentially mobile and the function g is defined within f. According to our discussion at the beginning of this section, there is no immediate reason for g to be taken as potentially mobile. However, it should be noted that the function g escapes the definition of f because it is returned as a result. It may be the case that the computation arrives at a point where it is transmitted by some other code. Therefore, it appears to be a safer option to consider functions such as g as potentially mobile.

2.2 Mobile Channels

As we have noted in Section 1 data structures implementing channels in Facile reside on the node where they were created and do not move. By channel mobility we mean the extrusion of the scope of a channel by sending its name. When a channel c is sent along a channel c’, the scope of c expands to include the expression receiving it.

The arguments for mobile functions above apply to mobile channels as well and our criteria for identifying mobile channels is the same as those for functions. This is easily justified as channels are also first-class values and all first-class values are treated uniformly in Facile-like languages.

3 A Language for Communicating Expressions

Our view of a system is a coupling of two sites each of which evaluates a single expression. Each expression possibly communicates with the expression on the remote site through synchronous channels. We believe that this simple setting embodies the core ingredients of a distributed system where the basic computational units are functions. It provides a sufficient level of generality to model the remote transmission of functions which is our main interest.

We introduce a language which includes all the constructs of a typical sequential functional language extended with constructs for creating channels and sending and receiving values over these channels.

3.1 Syntax

The unusual point about the syntax is that function abstractions, recursive expressions and channel allocation expressions are labelled. We assume two disjoint sets of labels L and R which include labels for functions and channels respectively. The purpose of function labels (l) drawn from (L) and the channel labels (r) drawn from (R) is to uniquely identify functions and channels. Therefore, all labels in a program are required to be distinct.

e  ::=  () | true | false | n | chan^{r}()
| x | fn^{l} x ⇒ e | e_{1} e_{2} | primop c e
| e_{1}; e_{2} | let x = e_{1} in e_{2}
| rec^{l} f(x) ⇒ e | if e_{1} then e_{2} else e_{3}
| e_{1}? | e_{1}!e_{2}

3.2 Dynamic Semantics

3.2.1 Semantic Objects

Values of the language are the unit value, the values of base types such as integers and booleans, channel identifiers (ci) and function closures. The dynamic semantics distinguishes a set of values (b) as basic values.

Since the system consists of two expressions each of which return a value, we define a top-level value as a tupling of the individual values of expressions.

We also use semantic objects which describe the communication behaviour of an expression; com stands for a communication event drawn from the set {ch ci, ci?val, ci!val} representing the allocation of a channel, receiving and sending values over a channel respectively. The name w stands for a sequence of communication events.

Other semantic objects include a channel identifier set CI and an evaluation environment E which is a mapping from identifiers to values.

val  ::=  val_{unit} | val_{true} | val_{false} | val_{n}
ci | ⟨E, fn^{l} x ⇒ e⟩
val_{top}  ::=  (val_{1}, val_{2})
com  ::=  ch ci | ci?val | ci!val
w  ::=  ϵ | com_{1} … com_{n}

3.2.2 Top-level Rule and Matching

Our language does not include a construct for parallel composition of expressions. The concurrent activity is revealed in the composition of two sites. The top-level evaluation decomposes into individual evaluations at each site.

CI, E_{1} ⊢_{loc_{1}}e_{1}⟹^{w_{1}}val_{1}, CI_{1} CI, E_{2} ⊢_{loc_{2}}e_{2}⟹^{w_{2}}val_{2}, CI_{2}

w_{1} || w_{2} ↪ w_{top} w_{top} = ch ci_{1}…. ch ci_{n} (CI_{1} ∪ CI_{2}) \ CI = {ci_{1}, … ci_{n}}

CI, (E_{1}, E_{2}), (loc_{1}[e_{1}] || loc_{2}[e_{2}])⟹^{w_{top}}(val_{1}, val_{2}), CI_{1} ∪ CI_{2}

The synchronisation is specified by the following matching rules between communication event sequences.

ϵ || ϵ ↪ ϵ
\frac{w_{1} || w_{2} ↪ w}{w_{1}.com || w_{2} ↪ w.com}  \frac{w_{1} || w_{2} ↪ w}{w_{1} || w_{2}.com ↪ w.com}
\frac{w_{1} || w_{2} ↪ w}{w_{1}.ci!val || w_{2}.ci?val ↪ w}  \frac{w_{1} || w_{2} ↪ w}{w_{1}.ci?val || w_{2}.ci!val ↪ w}

3.2.3 Sequential Evaluation Rules

A judgement of the form CI, E ⊢ e⟹^{w}val, CI′ states that expression e evaluates to value val against an environment E and a global channel identifier set CI updating it to CI′. The evaluation relation ⟹, which is defined in Figure 1, is annotated with the possible communication events which may occur during evaluation. Initially, E contains the ubiquitous values and other values that are provided as predefined at the site of evaluation. The evaluation rules are quite intuitive. Note that the only rule which updates the channel identifier set CI is the rule for channel creation. This rule generates a new channel identifier which is globally unique. We can assume that each evaluation site generates fresh channel identifiers prefixed with its name. APPLY serves as a semantic tool to define the application of a predefined operation to an argument.

4 Type System

The type system specified in this section is designed with the intention of exposing which functions and channels an expression can possibly transmit. It extends the earlier type and effect systems which we mention in Section

(unit)  CI, E ⊢ ()⟹^{ϵ}val_{unit}, CI
(true)  CI, E ⊢ true⟹^{ϵ}val_{true}, CI
(false)  CI, E ⊢ false⟹^{ϵ}val_{false}, CI
(int)  CI, E ⊢ n⟹^{ϵ}val_{n}, CI
(chan)  CI, E ⊢ chan^{r}()⟹^{ch ci}ci, CI ∪ {ci} ci globally new
(var)  CI, E ⊢ x⟹^{ϵ}E(x), CI
(fn)  CI, E ⊢ fn^{l} x ⇒ e ⟹^{ϵ}⟨E, fn^{l} x ⇒ e⟩, CI
(rec)  \frac{val = ⟨E[f ↦ val], fn^{l} x ⇒ e⟩}{CI, E ⊢ rec^{l} f(x) ⇒ e ⟹^{ϵ}val, CI}

(app)

CI, E ⊢ e_{1}⟹^{w_{1}}⟨E′, fn^{l} x ⇒ e⟩, CI′ CI′, E ⊢ e_{2}⟹^{w_{2}}val, CI′′

CI′′, E′[x ↦ val] ⊢ e⟹^{w_{3}}val′, CI′′′

CI, E ⊢ e_{1} e_{2} ⟹^{w_{1}.w_{2}.w_{3}}val′, CI′′′

(primop)  \frac{CI, E ⊢ primop c⟹^{w_{1}}b, CI′ CI′, E ⊢ e⟹^{w_{2}}val, CI′′ APPLY(b, val) = val_{1}}{CI, E ⊢ primop c e⟹^{w}val_{1}, CI′′}

(seq)  \frac{CI, E ⊢ e_{1}⟹^{w_{1}}val_{1}, CI′ CI′, E ⊢ e_{2}⟹^{w_{2}}val_{2}, CI′′}{CI, E ⊢ e_{1} ; e_{2} ⟹^{w_{1}.w_{2}}val_{2}, CI′′}

(if-t)  \frac{CI, E ⊢ e_{1}⟹^{w_{1}}val_{true}, CI′ CI′, E ⊢ e_{2}⟹^{w_{2}}val, CI′′}{CI, E ⊢ if e_{1} then e_{2} else e_{3} ⟹^{w_{1}.w_{2}}val, CI′′}

(if-f)  \frac{CI, E ⊢ e_{1}⟹^{w_{1}}val_{false}, CI′ CI′, E ⊢ e_{3}⟹^{w_{2}}val, CI′′}{CI, E ⊢ if e_{1} then e_{2} else e_{3} ⟹^{w_{1}.w_{2}}val, CI′′}

(let)  \frac{CI, E ⊢ e_{1}⟹^{w_{1}}val_{1}, CI′ CI′, E[x ↦ val_{1}] ⊢ e_{2}⟹^{w_{2}}val_{2}, CI′′}{CI, E ⊢ let x = e_{1} in e_{2} ⟹^{w_{1}.w_{2}}val_{2}, CI′′}

(receive)  \frac{CI, E ⊢ e⟹^{w}ci, CI′}{CI, E ⊢ e? ⟹^{w.ci?val}val, CI′}

(send)  \frac{CI, E ⊢ e_{1}⟹^{w_{1}}ci, CI′ CI′, E ⊢ e_{2}⟹^{w_{2}}val, CI′′}{CI, E ⊢ e_{1}!e_{2} ⟹^{w_{1}.w_{2}.ci!val}val_{unit}, CI′′}

Figure 1: Evaluation Rules 6 so that the types capture additional information in the form of abstract closure annotations.

4.1 Semantic Objects

We have abstract closures (v), channel regions (χ), communication effects (κ), raw types (τ̄) and closure annotated types (τ). A type scheme (σ) can be obtained from a type (τ) by universally quantifying zero or more abstract closure, region, behaviour and type variables.

\begin{aligned}v & ::= & ∅ | ⟨ε, l⟩ | γ | v ∪ v \\ χ & ::= & r | ρ | χ ∪ χ \\ κ & ::= & ∅ | ch(χ, τ) | send(χ, L) | remref(χ, R) | recv(χ, τ) | β | κ ∪ κ \\ τ̄ & ::= & Unit | Int | Bool | chan_{χ}(τ) | τ→^{κ}τ | α \\ τ & ::= & (τ̄, v) \\ σ & ::= & ∀γ⃗ρ⃗β⃗α⃗. τ \end{aligned}

The set v conservatively estimates the set of functions an expression can evaluate to. A function closure ⟨E, fn^{l} x ⇒ e⟩ is abstracted by ⟨ε, l⟩ where ε stands for the environment of the function and l stands for the function. The abstract environment ε contains static bindings of free variables of the function expression with function or channel types. The meta-variable γ ranges over abstract closures. The operator ∪ denotes set union.

The set χ estimates channel regions. A more detailed explanation of regions can be found in [4, 18]. Channel regions are to channels what abstract closures are to functions. They abstract channels and thus provide a means of keeping track of the identity of channels in the static semantics. A channel region is represented by a label r. The meta-variable ρ ranges over channel regions.

The set κ estimates the communication effects which may occur during the evaluation of an expression. An expression may have no effect, or its overall effect can be estimated by a set of possible effects; allocating a channel, sending a function closure approximated by the set L or creating a remote reference to a channel which is approximated by the set R through a channel and receiving a value on a channel. The meta-variable β ranges over communication effects.

Raw types (τ̄) consist of base types, channel types, function types and type variables (α). We pair raw types with abstract closure annotations to get the types of our language. An expression of type chan_{χ}(τ) denotes a channel which communicates values of type τ where χ estimates the channel. An expression of type (τ̄_{1}, v_{1})→^{κ}(τ̄_{2}, v_{2}) denotes a function whose argument is estimated by v_{1} and whose result is estimated by v_{2}. By injecting value annotations into types we keep track of functions flowing as arguments and results. The annotation κ stands for the latent effect which may occur when the function is applied.

4.1.1 Operations on Types

The operations defined below are familiar from polymorphic type systems for languages with a functional core.

Definition 1 (≻)

A type scheme σ generalises a type τ, written as σ≻τ, if τ can be obtained from the body of σ by substituting types (τ), behaviours (κ), regions (χ) and abstract closures (v) for the bound type, behaviour, region and abstract closure variables of σ respectively. A substitution θ denotes a mapping from type, behaviour, region and abstract closure variables to types, behaviours, regions and abstract closures.

Definition 2 (Generalisation)

Types are generalised to type schemes by the operation Gen.

Gen(κ, Γ)(τ) = let{α⃗, β⃗, ρ⃗, γ⃗} = fv(τ) \ (fv(κ) ∪ fv(Γ)) in ∀α⃗β⃗ρ⃗γ⃗. τ where fv computes the free type, behaviour, region and abstract closure variables in the expected way.

4.1.2 Analysis for Mobility

The following two definitions are related to forming and analysing abstract closures and therefore are characteristic operations of our type system.

Definition 3 (Abstract Closure)

AbsCl(Γ, e, S) = ε where ε is the environment Γ restricted to the bindings of free identifiers of e excluding the ones in set S, which have function or channel types.

The information with respect to function closures embodied in types through v annotations are analysed to extract the labels of potentially mobile functions and channels. The rules of this analysis are specified by an inference system. A judgement of the form ⊢_{mob} τ : R, L means that the transmission of a value of type τ may cause the transmission of channels with labels in R and functions with labels in L.

Definition 4 ( ⊢_{mob} )

(1)  ⊢_{mob} (τ̄, ∅) : ∅, ∅ τ̄ base type or variable
(2)  ⊢_{mob} (chan_{ρ}(τ), ∅) : ∅, ∅
(3)  ⊢_{mob} (chan_{r}(τ), ∅) : {r}, ∅

(4)  \frac{⊢_{mob} (chan_{χ_{1}}(τ), ∅) : R_{1}, L_{1} ⊢_{mob} (chan_{χ_{2}}(τ), ∅) : R_{2}, L_{2}}{⊢_{mob} (chan_{χ_{1}∪χ_{2}}(τ), ∅) : R_{1} ∪ R_{2}, L_{1} ∪ L_{2}}

(5)  \frac{⊢_{mob} τ_{2} : R_{2}, L_{2}}{⊢_{mob} (τ_{1}→^{κ}τ_{2}, γ) : R_{2}, L_{2}}

(6)  \begin{matrix}if ε(x) = (τ_{x}) ⊢_{mob} τ_{x} : R_{x}, L_{x} \\ R_{1} = ⋃R_{x}, L_{1} = ⋃ L_{x} \\ ⊢_{mob} τ_{2} : R_{2}, L_{2} \\ ⊢_{mob} (τ_{1}→^{κ}τ_{2}, ⟨ε, l⟩) : R_{1} ∪ R_{2}, \{l\} ∪ L_{1} ∪ L_{2} \end{matrix}

(7)  \frac{⊢_{mob} (τ̄, v_{1}) : R_{1}, L_{1} ⊢_{mob} (τ̄, v_{2}) : R_{2}, L_{2}}{⊢_{mob} (τ̄, v_{1} ∪ v_{2}) : R_{1} ∪ R_{2}, L_{1} ∪ L_{2}}

The Rule 1 applies when the raw type is a base type or a variable. Our type system does not keep track of values of base types.

The Rules 2,3,4 apply when the type is a channel type and the channel is estimated by a region variable, single region or a set of regions respectively. A variable includes no specific information, hence the empty R in Rule 2. In cases where labels are present in the set χ, Rules 3 and 4 collect these one by one and merge them in R.

The Rules 5,6,7 apply when the type is a function type. If an abstract closure is represented by a variable we have no information about the environment of the function or its label. However, the result type may include information about the escaping values, therefore it needs to be examined. Rule 5 handles this case. If the function is abstracted by a single abstract closure, Rule 6 extracts the label of the function and examines the bindings of the identifiers of the abstract environment to collect the labels of potentially mobile values. The return type is also examined to handle the escaping values. If the function is estimated by a non-singleton set Rule 7 ensures that each element of the set is examined and the results are merged into a single set.

(unit)  Γ ⊢ () : (Unit, ∅), ∅
(true)  Γ ⊢ true : (Bool, ∅), ∅
(false)  Γ ⊢ false : (Bool, ∅), ∅
(int)  Γ ⊢ n : (Int, ∅), ∅
(chan)  Γ ⊢ chan^{r}() : (chan_{χ}(τ), ∅), ch(χ, τ) τ = (α, γ) , α, γ new , r ⊆ χ
(var)  \frac{Γ(x) = σ σ ≻ τ}{Γ ⊢ x : τ}
(fn)  \frac{Γ[x ↦ τ_{1}] ⊢ e : τ_{2}, κ ε = AbsCl(Γ, e, \{x\})}{Γ ⊢ fn^{l} x ⇒ e : (τ_{1}→^{κ}τ_{2}, ⟨ε, l⟩), ∅}
(rec)  \frac{Γ[f ↦ (τ_{1}→^{κ}τ_{2}, ⟨ε, l⟩)][x ↦ τ_{1}] ⊢ e : τ_{2}, κ ε = AbsCl(Γ, e, \{x, f\})}{Γ ⊢ rec^{l} f (x) ⇒ e : (τ_{1}→^{κ}τ_{2}, ⟨ε, l⟩), ∅}
(app)  \frac{Γ ⊢ e_{1} : ((τ̄_{1}, v)→^{κ}(τ̄_{2}, v_{2}), v′), κ′ Γ ⊢ e_{2} : (τ̄_{1}, v_{1}), κ′′ v_{1} ⊆ v}{Γ ⊢ e_{1} e_{2} : (τ̄_{2}, v_{2}), κ ∪ κ′ ∪ κ′′}
(primop)  \frac{Γ ⊢ primop c : ((τ̄_{1}, v)→^{κ}(τ̄_{2}, v_{2}), v′), ∅ Γ ⊢ e : (τ̄_{1}, v_{1}), κ′ v_{1} ⊆ v}{Γ ⊢ primop c e : (τ̄_{2}, v_{2}), κ ∪ κ′}
(seq)  \frac{Γ ⊢ e_{1} : τ_{1}, κ Γ ⊢ e_{2} : τ_{2}, κ′}{Γ ⊢ e_{1} ; e_{2} : τ_{2}, κ ∪ κ′}
(if)  \frac{Γ ⊢ e_{1} : (Bool, ∅), κ, Γ ⊢ e_{2} : (τ̄, v), κ′ Γ ⊢ e_{3} : (τ̄, v′), κ′′}{Γ ⊢ if e_{1} then e_{2} else e_{3} : (τ̄, v ∪ v′), κ ∪ κ′ ∪ κ′′}
(let)  \frac{Γ ⊢ e_{1} : τ_{1}, κ Γ[x ↦ Gen(κ, Γ)(τ_{1})] ⊢ e_{2} : τ_{2}, κ′}{Γ ⊢ let x = e_{1} in e_{2} : τ_{2}, κ ∪ κ′}
(receive)  \frac{Γ ⊢ e : (chan_{χ}(τ), ∅), κ}{Γ ⊢ e? : τ, κ ∪ recv(χ, τ)}
(send)  \frac{Γ ⊢ e_{1} : (chan_{χ}(τ), ∅), κ Γ ⊢ e_{2} : τ, κ′ ⊢_{mob} τ : R, L}{Γ ⊢ e_{1}!e_{2} : Unit, κ ∪ κ′ ∪ send(χ, L) ∪ remref(χ, R)}
(subs)  \frac{Γ ⊢ e : (τ̄, v), κ κ ⊆ κ′ v ⊆ v′}{Γ ⊢ e : (τ̄, v′), κ′}

Figure 2: Typing Rules 4.1.3 Typing Rules

The static semantics for the language assigns a type, an effect (τ, κ) to each expression. This is represented by a judgement of the form Γ ⊢ e : τ, κ .

The context in which an expression is assigned a type, an effect and an abstract value is represented by a static environment Γ, which maps value identifiers to type schemes (σ). The notation Γ[x ↦ σ] is used for adding element x to the environment Γ, overriding the existing binding if x is already in the domain of Γ.

Regarding polymorphism, we adopt the standard discipline employed in languages with a functional core and allow type generalisation to be performed in the (let) rule only.

The rule (send) for the send expression reveals the essence of the type system. All the information with respect to the sent value captured by its type is analysed to extract the labels of the channels and the closures which are potentially mobile.

The side condition in the application rule (app) is used to ensure that the abstract closure annotation inferred for the argument is consistent with the abstract closure annotation which appears in the argument position of the function type. The operator ⊆ denotes the subset relation for sets.

The subsumption rule (subs) allows an expression to admit a larger communication effect and an abstract closure than seems to be necessary. We adopt the approach which is referred to as early subsumption in [18] and subeffecting in [32]. This is in contrast to the approach known as late subsumption or subtyping where coercion can happen at any time inside any type. The advantage of our approach is that the complex interplay between polymorphism and subtyping can be avoided.

5 Semantic Consistency

We define the following consistency judgements which relate objects of the dynamic semantics to objects of the static semantics with respect to a given channel environment CE where CE is defined as a mapping from channel identifiers to channel region and type pairs: [ci_{1} ↦ (χ_{1}, τ), …, ci_{n} ↦ (χ_{n}, τ)]. The rest of the objects we refer to are as defined in the previous sections.

CE ⊧ val : τ  the value val has the type τ
CE ⊧ E : Γ  the values of E respect the types of Γ
CE ⊧ com : κ the event com respects the effect κ
CE ⊧ w : κ  the event sequence w respects the effect κ

The definition of ⊧ makes use of an ordering relation ⪯ between abstract closures which is defined as follows.

Definition 5 (⪯)

ϵ ⪯ v  for any v
⟨ε_{1}, l⟩ ⪯ v if there exists ⟨ε_{2}, l⟩ ∈ v such that ε_{1} ⊆ ε_{2}

The consistency relation which establishes the correspondence between objects of the dynamic semantics and the static semantics satisfies the following properties:

Definition 6 (⊧)

CE ⊧ val_{unit} : (Unit, ϵ) CE ⊧ val_{true} : (Bool, ϵ) CE ⊧ val_{false} : (Bool, ϵ) CE ⊧ val_{n} : (Int, ϵ)

CE ⊧ ci : (chan_{χ}(τ), ϵ)

if ch(χ, τ) ∈ κ, CE(ci) = (χ, τ)

CE ⊧ ⟨E, fn^{l} x ⇒ e⟩ : (τ_{1}→^{κ′}τ_{2}, v)

if there exists Γ such that Γ ⊢ fn^{l} x ⇒ e : (τ_{1}→^{κ′}τ_{2}, v′), ∅

where v ⪯ v′ and CE ⊧ E : Γ

CE ⊧ E : Γ if Dom(E) = Dom(Γ) and for any x ∈ Dom(E) CE ⊧ E(x) : v such that v ⪯ Γ(x).

CE ⊧ ϵ : ∅ CE ⊧ ch ci : ch(χ, τ)

if CE(ci) = (χ, τ) CE ⊧ ci?val : recv(χ, τ)

if CE(ci) = (χ, τ) CE ⊧ ci!val : send(χ, L) ∪ remref(χ, R)

if CE(ci) = (χ, τ) and CE ⊧ val : τ

and ⊢_{mob} τ : R′, L′ such that R′ ⊆ R, L′ ⊆ L

CE ⊧ w : κ if there exists a κ_{i} ∈ κ such that CE ⊧ com : κ_{i} for any com ∈ w

We write Γ ⊧ val : ∀ι⃗.τ if and only if Γ ⊧ val : θτ for any substitution θ defined on ι⃗.

The typing consistency relation that we seek to define must be viewed as the maximal fixed point of the property defined above. We consider an appropriate function F and by verifying that F is monotonic conclude that the above definition is satisfied by its maximal fixed point. This part of the proof is omitted from our discussion.

Definition 7 (Extension)

(κ′, CE′) extends (κ, CE), written (κ, CE) ⊑ (κ′, CE′) if and only if κ ⊆ κ′, Dom(CE) ⊆ Dom(CE′) and for all ci ∈ Dom(CE), if CE(ci) ∈ Rng(κ) or CE′(ci) ∈ Rng(κ) then CE′(ci) = CE(ci).

Definition 8 (Equivalence)

(κ, CE) and (κ′, CE′) are equivalent, written (κ, CE) ≃ (κ′, CE′), if and only if (κ, CE) ⊑ (κ′, CE′) and (κ′, CE′) ⊑ (κ, CE).

Definition 9 (Succession)

(CI, w, κ, CE) ⊑ (CI′, w′, κ′, CE′) if and only if CI ⊆ CI′, w′ = w.w′′ for some w′′, (κ, CE) ⊑ (κ′, CE′),CE ⊧ val : τ and CE ⊧ w : κ implies CE′ ⊧ val : τ and CE′ ⊧ w′ : κ′.

Proposition 1 (Consistency)

Assume CI, (E_{1}, E_{2})(loc_{1}[e_{1}] || loc_{2}[e_{2}])⟹^{w_{top}}(val_{1}, val_{2}), CI_{top}.

For each e ∈ {e_{1}, e_{2}}, if CE ⊧ E : Γ and CE ⊧ w_{0} : κ_{0}, Γ ⊢ e : (τ̄, v), κ and CI, E ⊢ e⟹^{w}val, CI′ then there exists a CE′ and v′ such that CE′ ⊧ val : τ̄, v′ and (CI, w_{0}, κ_{0}, CE ⊑ CI′, w_{0}.w, κ_{0} ∪ κ, CE′) and v′ ⪯ v.

Proof (Consistency) The proof is given by a simultaneous induction on the depth of inference of CI, E_{i} ⊢_{loc_{i}} e_{i}⟹^{w_{i}}val_{i}, CI′ for i ∈ {0, 1}. □

Appendix A contains the major lemmas used in the proof of the consistency. Selected cases from the proof of Proposition 1 are given in Appendix B.

The method used in the proof of consistency depends on the approach used in the specification of the dynamic and static semantics. Relative merits of different methods in proving the two semantics consistent have been discussed in the related literature [12, 30, 22, 25]. Our formulation can be likened to that of [25] in the sense that we use the formalism of relational semantics in specifying the evaluation rules and the static semantics rules involve effect inference. It can also be likened to that of [12] in the sense that the formalism of relational semantics is enriched by labelling evaluation rules with event sequences to capture the communication behaviour.

6 Related Work

Initially, effect systems were proposed as a solution to the problem of safely integrating functional and imperative features [13]. The basic idea was to enhance the type systems so that the expressions were associated with their observable side effects as well as types. This approach was pursued by Talpin and Jouvelot to safely type references in ML-like languages [25] and by Tofte and Talpin to improve memory management techniques [29]. The same approach was later carried over to concurrent programming languages where effect information was used in safe generalisation of channel types. The work by Thomsen on the language Facile [27] and Bolignano and Debbabi on Concurrent ML [4] are examples of this.

Another line of research in the literature demonstrates that the exploitation of type and effect systems need not be confined to the enforcement of type safety in the above sense. Annotated with effects and other kinds of information, types can capture a significant amount of static information about a program’s potential dynamic behaviour. For a more detailed explanation the reader is referred to the work by Nielson and Nielson which includes an analysis of communication topology of programs [18] and an analysis developed for obtaining information to be used in static and dynamic processor allocation [19].

Our work bears a strong similarity to the earlier type and effect systems, in particular to those designed for Facile and Concurrent ML. A common point of these systems is that they rely on the concept of channel regions which are the static counterparts of channels created at run-time. Channels play the key role in the problems they focus on. In our case however, it is the functions which play the key role. Therefore, we introduce the concept of abstract closure which can be considered as an analogous concept to channel regions. We retain channel regions in our type system because of two reasons. Firstly, we would like our type system to be at least as expressive as the earlier ones. Secondly, we are interested in the potential mobility of the channels as well as that of functions.

7 Conclusions and Future Work

We have shown that the methodology of annotated type and effect systems can be exploited to provide a general profile of programs with respect to the potential mobility of values where the main computational units are functions. Such a profile could be put to use internally by a compiler to direct optimisations or could serve as a tool for programmers.

It is now becoming a common practice to use types in stipulating safety and security properties and to provide sound systems for reasoning about these properties. The type-based approach to security emphasises the significance of tracing the flow of information through computation [9]. The power of our type and effect system comes from its ability to trace the flow of values. In other words, the machinery to control secure information flow is already partially built into the type system. We can now look at ways of exploiting it for expressing, validating and enforcing certain safety and security properties.

Most of the work in the area of safety and security is in the framework of lower-level process calculi such as the π-calculus family and static analyses techniques developed for these [9, 24, 10, 31, 2, 3, 1]. Casting some of these in the framework of a type and effect system such as ours would make the underlying ideas more readily applicable using the type systems of languages such as CML and Facile as a basis.

Acknowledgements

I would like to thank Stephen Gilmore for the very helpful discussions and the comments on the drafts of this paper. I also would like to thank Jane Hillston for her support. My research is funded by the University of Edinburgh.

References

[1] M. Abadi. Secrecy by typing in security protocols. In Proceedings of Theoretical Aspects of Computer Software, volume 1281 of LNCS, pages 611–638. Springer, 1997.

[2] C. Bodei, P. Degano, F. Nielson, and H. R. Nielson. Control flow analysis for the π-calculus. In Proceedings of International Conference on Concurrency Theory (CONCUR), number 1466 in Lecture Notes in Computer Science, pages 84–98. Springer-Verlag, 1998.

[3] C. Bodei, P. Degano, F. Nielson, and H. R. Nielson. Static analysis of processes for no read-up and no write-down. In Proceedings of FOS-SACS’99, number 1578 in Lecture Notes in Computer Science, pages 120–134. Springer-Verlag, 1999.

[4] D. Boloignano and M. Debbabi. A semantic theory for ML higher order concurrency primitives. In F. Nielson, editor, ML with Concurrency, chapter 6, pages 145–183. Springer-Verlag New York, Inc, 1997.

[5] K.L. Gasser, F.Nielson, and H.R.Nielson. Systematic realisation of control flow analysis for CML. In Proceedings of International Conference on Functional Programming (ICFP). ACM Press, 1997.

[6] A. Giacalone, P. Mishra, and S. Prasad. Facile: A symmetric integration of concurrent and functional programming. International Journal of Parallel Programming, 18(2):121–160, April 1989.

[7] N. Heintze. Control-flow analysis and type systems. Technical Report CMU-CS-94-227, School of Computer Science, Carnegie Mellon Univeristy, 1994. Also appears as Fox Memorandum CMU-CS-FOX-94-09.

[8] N. Heintze. Set-based analysis of ML programs. In Proceedings of Lisp and Functional Programming. ACM Press, 1994.

[9] N. Heintze and J. G. Riecke. The slam calculus: Programming with secrecy and integrity. In Proceedings of ACM Conference on Principles of Programming Languages (POPL), pages 365–377, San Diego, CA, USA, 1998.

[10] M. Hennesy and J. Riely. Type-safe execution of mobile agents in anonymous networks. In Secure Internet Programming: Proceedings of 4th Workshop on Mobile Object Systems, volume 1603 of LNCS, pages 95– 117, Brussels, 1998. Springer-Verlag.

[11] F.C. Knabe. Language Support for Mobile Agents. PhD thesis, Carnegie Mellon University, Pittsburgh, PA, USA, Dec. 1995.

[12] X. Leroy. Polymorphic Typing of an Algorithmic Language. PhD thesis, Univerity of Paris VII, 1992.

[13] J. Lucassen and D.K. Gifford. Polymorphic effect systems. In Proceedings of ACM Conference on Principles of Programming Languages (POPL), New York, 1988. ACM.

[14] R. Milner. Communication and Concurrency. Prentice Hall, 1989.

[15] R. Milner, J.Parrow, and D. Walker. A calculus of mobile processes I and II. Information and Computation, 100:1–72, 1992.

[16] R. Milner, M. Tofte, R.Harper, and D.MacQueen. The Definition of Standard ML: Revised 1997. The MIT Press, 1997.

[17] F. Nielson and H.R.Nielson. Infinitary control flow analysis: A collecting semantics for closure analysis. In Proceedings of ACM Conference on Principles of Programming Languages (POPL). ACM Press, 1997.

[18] H. R. Nielson and F. Nielson. Higher-order concurrent programs with finite communication topology. In Proceedings of ACM Conference on Principles of Programming Languages (POPL), pages 84–97. ACM Press, 1994.

[19] H. R. Nielson and F. Nielson. Static and dynamic processor allocation for higher-order concurrent languages. In Proceedings of TAPSOFT, volume 915 of Lecture Notes in Computer Science, pages 590–604. Springer-Verlag, 1995.

[20] J. Palsberg and P. O’Keefe. A type system equivalent to flow analysis. In Proceedings of ACM Conference on Principles of Programming Languages (POPL), pages 367–378. ACM Press, 1995.

[21] J. Palsberg and M. I. Schwartzbach. Safety analysis versus type inference. Information and Computation, 118:128–141, 1995.

[22] R.Milner and M.Tofte. Co-induction in relational semantics. Theoretical Computer Science, 87(1):209–220, Sep 1991.

[23] O. Shivers. Control-Flow Analysis of Higher-order Languages or Taming Lambda. PhD thesis, School of Computer Science, Carnegie-Mellon University, 1991.

[24] G. Smith and D. Volpano. A type-based approach to program security. In Proceedings of TAPSOFT ’97, pages 607–621, Lille, France.

[25] J.P. Talpin and P. Jouvelot. The type and effect discipline. Information and Computation, 111:245–296, 1994.

[26] B. Thomsen. Calculi for Higher Order Communicating Systems. PhD thesis, Imperial College, London University, 1989.

[27] B. Thomsen. Polymorphic sorts and types for concurrent functional programs. In J. Glauert, editor, Proceedings of the 6th International Workshop on the Implementatin of Functional Languages, Norwich,UK, 1994.

[28] B. Thomsen, L. Leth, S. Prasad, T. M. Kuo, A. Kramer, and F.C. Knabe. Facile Antigua Release programming guide. Technical Report ECRC-93-20, Europian Computer Industry Research Centre, Munich, Germany, Dec. 1993.

[29] M. Tofte and J.P. Talpin. Implemantation of the types call-by-value λ-calculus using a stack of regions. In Proceedings of ACM Conference on Principles of Programming Languages (POPL), pages 188–201, Portland, Oregon, USA, 1994.

[30] A. Wright and M. Felleisen. A syntactic approach to type soundness. Technical report, Rice University, 1992.

[31] N. Yoshida and M. Hennessy. Subtyping and locality in distributed higher order processes. In Proceedings of International Conference on Concurrency Theory (CONCUR), LNCS. Springer-Verlag, 1999.

[32] Y.Tang and P.Jouvelot. Control-flow effects for escape analysis. In Proceedings of WSA’92, Bordeux, France, 1992.

A Lemmas

Lemma 1 (General Substitution)

If Γ ⊢ e : τ, κ then θΓ ⊢ e : θτ, θκ.

Proof (General Substitution) The proof is given by induction on the derivation of Γ ⊢ e : τ, κ.

case x The rule (var) of the the static semantics imposes that the typing is of the following form Γ ⊢ x : τ, ∅ Γ(x) = σ and σ ≻ τ.

Suppose σ = ∀ι⃗.τ_{0}. After renaming if necessary we define θ so that ι⃗ is out of reach of θ. Let θ′ be a substitution over ι⃗ such that θ′(τ_{0}) = τ. Now define a substitution θ′′ with domain ι⃗_{i} by θ′′(ι_{i}) = θ(θ′′(ι_{i})). We then have θ′′(θ(ι_{i})) = θ′′(ι_{i}) = θ(θ′(ι_{i})) for all i θ′′(θ(β)) = θ(β) = θ(θ′(β)) for all β not in ι⃗_{i} Hence, θ′′(θ(τ_{0})) = θ(θ′(τ_{0})) = θ(τ) which shows that θ(τ) is an instance of θ(Γ(x)). So, θ(Γ) ⊢ x : Γ(τ).

case let x = e_{1} in e_{2} The rule (var) of the the static semantics imposes that the typing is of the following form Γ ⊢ e_{1} : τ_{1}, κ Γ[x ↦ Gen(κ, Γ)(τ_{1})] ⊢ e_{2} : τ_{2}, κ′

Let ∀ι⃗.τ_{1} be Gen(κ, Γ)(τ_{1}). For any substitution θ, let us consider fresh ι⃗′ and define θ′ as the extension of θι⃗ with θ{ι ↦ ι′}. By the definition of Gen we have that θ(Γ) = θ′(Γ) and θ(κ) = θ′(κ′). By the definition of θ′, ι being out of reach, θ′(∀ι⃗.τ_{1}) = ∀ι⃗′.θ′τ_{1}. Thus, θ(Γ[x ↦ Gen(κ, Γ)(τ_{1})] = θ(Γ)[x ↦ Gen(θκ, θΓ)(θ′τ_{1})].

By using the induction hypothesis on e_{1} with θ′ we get θ′Γ ⊢ e : θ′τ, θ′κ. By definition of θ′, θ′Γ ⊢ e : θ′τ, θκ. By using the induction hypothesis on e_{2} we get θ(Γ[x ↦ Gen(κ, Γ)(τ_{1})]) ⊢ e_{2} : θ(τ_{2}), θ(κ′) which is equivalent to θ(Γ)[x ↦ Gen(θ(κ), θ(Γ))(θ′(τ_{1}))] ⊢ e_{2} : θ(τ_{2}), θ(κ′). Finally by definition of (let) we can conclude that θ(Γ) = let x = e_{1} in e_{2} : θ(τ), θ(κ). □

Lemma 2 (Extension)

If CE ⊧ val : τ and CE ⊧ w : κ and (κ, CE) ⊑ (κ′, CE′) then CE′ ⊧ val : τ and CE′ ⊧ w : κ.

Proof (Extension) We consider the set Z = {(w, κ′, CE′, val, τ) | CE ⊧ val : τ and CE ⊧ w : κ and (κ, CE) ⊑ (κ′, CE′)}. We show by case analysis on the structure of val that q = (w, κ′, CE′val, τ) ∈ F (Z). □

Lemma 3 (Equivalence)

If (κ, CE) ≃ (κ′, CE′) and CE ⊧ val : τ and CE ⊧ w : κ if and only if CE′ ⊧ val : τ and CE′ ⊧ w : κ′.

Proof (Equivalence) Since (κ, CE) ≃ (κ′, CE′), by Definition 7, (κ, CE) ⊑ (κ′, CE′) and (κ′, CE′) ⊑ (κ, CE). If CE ⊧ val : τ and CE ⊧ w : κ then by Lemma 2, CE′ ⊧ val : τ and CE′ ⊧ w : κ. If S : CE′ ⊧ val : τ and CE′ ⊧ w : κ then by Lemma 2, CE ⊧ val : τ and CE ⊧ w : κ. □

Lemma 4 (Semantic Substitution)

If CE ⊧ val : τ and CE ⊧ w : κ then θCE ⊧ val : θτ and CE ⊧ w : θκ for any substitution θ.

Proof (Semantic Substitution) We consider Z = {(w, θκ, θCE, val, θτ) | CE ⊧ val : τ and CE ⊧ w : κ} and show by case analysis on the structure of val that q = (w, θκ, θCE, val, θτ) is in F (Z). □

Lemma 5 (Instantiation)

If CE ⊧ val : τ and CE ⊧ w : κ and θ is defined on fv(τ) \ fv(κ) then CE ⊧ val : θτ and CE ⊧ w : κ.

Proof (Instantiation) By Lemma 4, θCE ⊧ val : θτ and CE ⊧ w : θκ. Since θκ = κ, by Definition 7, (κ, CE) ≃ (κ, θCE). By Lemma 3 we conclude that CE ⊧ val : θτ and CE ⊧ w : κ. □

Lemma 6 (Channel allocation)

Let κ′ = ch(χ, τ) , w′ = w.ch ci and CE′ = CE[ci ↦ (χ, τ)] where ci ∉ Dom(CE). If CE ⊧ val : τ′ and CE ⊧ w : κ then CE′ ⊧ val : τ′ and CE′ ⊧ w′ : κ ∪ κ′.

Proof (Channel Allocation) We consider the set Z = {(w′, κ∪κ′, CE′, val, τ′) | CE ⊧ val : τ, CE ⊧ w : κ}. We show by case analysis on the structure of val that q = (w′, κ ∪ κ′, CE′, val, τ′) is in F (Z). □

Lemma 7 (Send)

Let κ′ = send(χ, L) ∪ remref(χ, R), w′ = w.ci!val, CE ⊧ ci : (chan_{χ}(τ), ϵ), CE ⊧ w : κ, CE ⊧ val : τ and ⊢_{mob} τ : R′, L′ where R′ ⊆ R, L′ ⊆ L . If CE ⊧ val′ : τ′ and CE ⊧ w : κ then CE′ ⊧ val′ : τ′ and CE ⊧ w′ : κ ∪ κ′.

Proof (Send) We consider the set Z = {(w′, κ ∪ κ′, CE′, val, τ′) | CE ⊧ val : τ andCE ⊧ w : κ}. We show by case analysis on the structure of val that q = (w′, κ ∪ κ′, CE′, val, τ′) is in F (Z). □

B Proof of consistency

case chan^{r}() The rules (chan) of the dynamic and the static semantics impose that the evaluation and the typing are of the form

CI, E ⊢ chan^{r}()⟹^{ch ci}ci, CI ∪ {ci} ci ∉ CI

Γ ⊢ chan^{r}() : (chan_{χ}(τ), ∅), ch(χ, τ) where τ = (α, γ), α, γ are new, r ⊆ χ . By hypothesis CE ⊧ w_{0} : κ_{0}. We are required to show that there exits CE′ and v′ such that CE′ ⊧ val : τ̄, v′ and (CI, w_{0}, κ_{0}, CE ⊑ CI′, w.ch ci, κ_{0} ∪ ch(χ, τ), CE′) and v′ ⪯ v.

We provide a witness for CE′ by taking CE′ = CE[ci ↦ (χ, τ)] such that ci ∉ CI and ci ∉ Dom(CE). By Lemma 6 we know that if CE ⊧ val : τ′ then CE′ ⊧ val : τ′ and CE′ ⊧ w.chan ci : κ_{0} ∪ ch(χ, τ). Now, by Definition 5 we also have (CI, w, κ, CE ⊑ CI′, w.chan ci, κ∪ch(χ, τ), CE′). We provide a witness for v′ by taking v′ = ϵ.

case e_{1}e_{2} The rules (app) of the dynamic and the static semantics impose that the evaluation and the typing are of the form

CI, E ⊢ e_{1}⟹^{w_{1}}⟨E′, fn^{l} x ⇒ e⟩, CI′ CI′, E ⊢ e_{2}⟹^{w_{2}}val, CI′′

CI′′, E′[x ↦ val] ⊢ e⟹^{w_{3}}val′, CI′′′

CI, E ⊢ e_{1} e_{2} ⟹^{w_{1}.w_{2}.w_{3}}val′, CI′′′

\frac{Γ ⊢ e_{1} : ((τ̄_{1}, v)→^{κ}(τ̄_{2}, v_{2}), v′), κ′ Γ ⊢ e_{2} : (τ̄_{1}, v_{1}), κ′′ v_{1} ⊆ v}{Γ ⊢ e_{1} e_{2} : (τ̄_{2}, v_{2}), κ ∪ κ′ ∪ κ′′}

By the induction hypothesis on e_{1} and the assumption CE ⊧ E′ : Γ and CE ⊧ w_{0} : κ_{0}, there exists CE′ and v′′ such that

CE′ ⊧ ⟨E′, fn^{l} x ⇒ e⟩ : ((τ̄_{1}, v)→^{κ}(τ̄_{2}, v_{2}), v′′), v′′ ⪯ v′ and

(CI, w_{0}, κ_{0}, CE) ⊑ (CI′, w.w_{1}, κ_{0}∪κ′, CE′). By Definition 5 we can conclude that CE′ ⊧ E′ : Γ and CE′ ⊧ w_{0}.w_{1} : κ_{0} ∪ κ′. Now, by induction hypothesis on e_{2} there exists CE′′ and v′′′ such that CE′′ ⊧ val : (τ̄_{1}, v′′′) , v′′′ ⪯ v_{1} and (CI′, w_{0}, κ_{0} ∪ κ′, CE′) ⊑ (CI′′, κ_{0} ∪ κ′ ∪ κ′′, CE′′). By Definition

5, since CE′ ⊧ ⟨E′, fn^{l} x ⇒ e⟩ : ((τ̄_{1}, v)→^{κ}(τ̄_{2}, v_{2}), v′′), we have CE′′ ⊧

⟨E′, fn^{l} x ⇒ e⟩ : ((τ̄_{1}, v)→^{κ}(τ̄_{2}, v_{2}), v′′) and CE′′ ⊧ w_{0}.w_{1} : κ_{0} ∪ κ′ ∪ κ′′.

CE′′ ⊧ ⟨E′, fn^{l} x ⇒ e⟩ : ((τ̄_{1}, v)→^{κ}(τ̄_{2}, v_{2}), v′′) requires that there exists a

Γ′ such that Γ′ ⊢ fn^{l} x ⇒ e : ((τ̄_{1}, v)→^{κ}(τ̄_{2}, v_{2}), v′′′′), ∅ where v′′ ⪯ v′′′′ and

CE′′ ⊧ E′ : Γ′.

Let us take E′′ = E′[x ↦ val] and Γ′′ = Γ′[x ↦ (τ̄_{1}, v)]. By the side condition v_{1} ⊆ v and Definition (⪯) , it follows that v′′′ ⪯ v. By Definition (⊧) and Lemma 2 we have CE′′ ⊧ E′′ : Γ′′ and CE′′ ⊧ w_{0}.w_{1}.w_{2} : κ_{0} ∪ κ′ ∪ κ′′. Now, by induction hypothesis on e_{3}, we can conclude that there exists a CE′′′ and v′_{2} such that v′_{2} ⪯ v_{2} and (CI′′, w_{0}.w_{1}.w_{2}, κ_{0} ∪ κ′ ∪ κ′′, CE′′) ⊑ (CI′′′, , w_{0}.w_{1}.w_{2}.w_{3}, κ_{0} ∪ κ′ ∪ κ′′ ∪ κ, CE′′′). case e_{1}!e_{2} The rules (send) of the dynamic and the static semantics impose that the evaluation and the typing are of the form

\frac{CI, E ⊢ e_{1}⟹^{w_{1}}ci, CI′ CI′, E ⊢ e_{2}⟹^{w_{2}}val, CI′′}{CI, E ⊢ e_{1}!e_{2} ⟹^{w_{1}.w_{2}.ci!val}val_{unit}, CI′′}

\frac{Γ ⊢ e_{1} : (chan_{χ}(τ), ∅), κ Γ ⊢ e_{2} : τ, κ′ ⊢_{mob} τ : R, L}{Γ ⊢ e_{1}!e_{2} : Unit, κ ∪ κ′ ∪ send(χ, L) ∪ remref(χ, R)}

By the induction hypothesis on e_{1} and the assumption CE ⊧ E : Γ and CE ⊧ w_{0} : κ_{0} there exists CE′ and v′ such that CE′ ⊧ ci : chan_{χ}(τ̄, ϵ), (CI, w_{0}, κ_{0}, CE) ⊑ (CI′, w_{0}.w_{1}, κ_{0} ∪ κ, CE′) and ϵ ⪯ ∅.

By Definition 5 we have CE′ ⊧ E : Γ and CE′ ⊧ w_{0}.w_{1} : κ_{0} ∪ κ. We can now apply the induction hypothesis on e_{2}. It follows that there exists CE′′ and v′′ such that CE′′ ⊧ val : (τ̄, v′′) where τ = (τ̄, v) and (CI′, w_{0}.w_{1}, κ_{0} ∪ κ′, CE′) ⊑ (CI′′, w_{0}.w_{1}.w_{2}, κ_{0} ∪ κ ∪ κ′, CE′′) and v′′ ⪯ v. By Definition 5 we also have CE′ ⊧ ci : chan_{χ}(τ), v′.

The side condition imposes that ⊢_{mob} τ : R, L. We know that τ = (τ̄, v) and v′′ ⪯ v. Suppose ⊢_{mob} (τ̄, v′′) = R′, L′. By inspecting the definition of ⊢_{mob} it follows that R′ ⊆ R, L′ ⊆ L. By Lemma 7 we can conclude that (CI′′, w_{0}.w_{1}.w_{2}, κ_{0} ∪ κ ∪ κ′, CE′′ ⊑ (CI′′, w_{0}.w_{1}.w_{2}.ci!val, κ_{0} ∪ κ ∪ κ′ ∪ send(χ, L) ∪ remref(χ, R), CE′′), CE′′).

Finally, by Definition 5 and ⊧ we conclude that CE′′ ⊧ val_{unit} : (Unit, ϵ) and (CI, w_{0}, κ_{0}, CE) ⊑ (CE′′, κ_{0} ∪κ′ ∪κ′′ ∪send(χ, L)∪remref(χ, R), CE′′). □