Ferruccio Damiani
email: ferruccio.damiani@unito.it

Mirko Viroli
email: mirko.viroli@unibo.it

Danilo Pianini
email: danilo.pianini@unibo.it

Jacob Beal
email: jakebeal@bbn.com

Code Mobility Meets Self-organisation: a Higher-order Calculus of Computational Fields

Self-organisation mechanisms, in which simple local interactions result in robust collective behaviors, are a useful approach to managing the coordination of large-scale adaptive systems. Emerging pervasive application scenarios, however, pose an openness challenge for this approach, as they often require flexible and dynamic deployment of new code to the pertinent devices in the network, and safe and predictable integration of that new code into the existing system of distributed self-organisation mechanisms. We approach this problem of combining self-organisation and code mobility by extending "computational field calculus", a universal calculus for specification of self-organising systems, with a semantics for distributed first-class functions. Practically, this allows selforganisation code to be naturally handled like any other data, e.g., dynamically constructed, compared, spread across devices, and executed in safely encapsulated distributed scopes. Programmers may thus be provided with the novel firstclass abstraction of a "distributed function field", a dynamically evolving map from a network of devices to a set of executing distributed processes.

Introduction

In many different ways, our environment is becoming ever more saturated with computing devices. Programming and managing such complex distributed systems is a difficult challenge and the subject of much ongoing investigation in contexts such as cyberphysical systems, pervasive computing, robotic systems, and large-scale wireless sensor networks. A common theme in these investigations is aggregate programming, which aims to take advantage of the fact that the goal of many such systems are best described in terms of the aggregate operations and behaviours, e.g., "distribute the new version of the application to all subscribers", or "gather profile information from everybody in the festival area", or "switch on safety lights on fast and safe paths towards the emergency exit". Aggregate programming languages provide mechanisms for building systems in terms of such aggregate-level operations and behaviours, and a global-to-local mapping that translates such specifications into an implementation in terms of the actions and interactions of individual devices. In this mapping, self-organisation techniques provide an effective source of building blocks for making such systems robust to device faults, network topology changes, and other contingencies. A wide range of such aggregate programming approaches have been proposed [START_REF] Beal | Organizing the aggregate: Languages for spatial computing[END_REF]: most of them share the same core idea of viewing the aggregate in terms of dynamically evolving fields, where a field is a function that maps each device in some domain to a computational value. Fields then become first-class elements of computation, used for tasks such as modelling input from sensors, output to actuators, program state, and the (evolving) results of computation.

Many emerging pervasive application scenarios, however, pose a challenge to these approaches due to their openness. In these scenarios, there is need to flexibly and dynamically deploy new or revised code to pertinent devices in the network, to adaptively shift which devices are running such code, and to safely and predictably integrate it into the existing system of distributed processes. Prior aggregate programming approaches, however, have either assumed that no such dynamic changes of code exist (e.g., [START_REF] Beal | Infrastructure for engineered emergence in sensor/actuator networks[END_REF][START_REF] Viroli | A calculus of computational fields[END_REF]), or else provide no safety guarantees ensuring that dynamically composed code will execute as designed (e.g., [START_REF] Mamei | Programming pervasive and mobile computing applications: The tota approach[END_REF][START_REF] Viroli | Linda in space-time: an adaptive coordination model for mobile ad-hoc environments[END_REF]). Accordingly, our goal in this paper is develop a foundational model that supports both code mobility and the predictable composition of self-organisation mechanisms. Moreover, we aim to support this combination such that these same self-organisation mechanisms can also be applied to manage and direct the deployment of mobile code.

To address the problem in a general and tractable way, we start from the field calculus [START_REF] Viroli | A calculus of computational fields[END_REF], a recently developed minimal and universal [START_REF] Beal | Towards a unified model of spatial computing[END_REF] computational model that provides a formal mathematical grounding for the many languages for aggregate programming. In field calculus, all values are fields, so a natural approach to code mobility is to support fields of first-class functions, just as with first-class functions in most modern programming languages and in common software design patterns such as MapReduce [START_REF] Dean | Mapreduce: simplified data processing on large clusters[END_REF]. By this mechanism, functions (and hence, code) can be dynamically consumed as input, passed around by device-to-device communication, and operated upon just like any other type of program value. Formally, expressions of the field calculus are enriched with function names, anonymous functions, and application of function-valued expressions to arguments, and the operational semantics properly accommodates them with the same core field calculus mechanisms of neighbourhood filtering and alignment [START_REF] Viroli | A calculus of computational fields[END_REF]. This produces a unified model supporting both code mobility and self-organisation, greatly improving over the independent and generally incompatible mechanisms which have typically been employed in previous aggregate programming approaches. Programmers are thus provided with a new first-class abstraction of a "distributed function field": a dynamically evolving map from the network to a set of executing distributed processes.

Section 2 introduces the concepts of higher-order field calculus; Section 3 formalises their semantics; Section 4 illustrates the approach with an example; and Section 5 concludes with a discussion of related and future work.

Fields and First-Class Functions

The defining property of fields is that they allow us to see computation from two different viewpoints. On the one hand, by the standard "local" viewpoint, computation is seen as occurring in a single device, and it hence manipulates data values (e.g., numbers) and communicates such data values with other devices to enable coordination. On the other hand, by the "aggregate" (or "global") viewpoint [START_REF] Viroli | A calculus of computational fields[END_REF], computation is seen as occurring on the overall network of interconnected devices: the data abstraction manipulated is hence a whole distributed field, a dynamically evolving data structure having extent over a subset of the network. This latter viewpoint is very useful when reasoning about aggregates of devices, and will be used throughout this document. Put more precisely, a field value φ may be viewed as a function φ : D → L that maps each device δ in the domain D to an associated data value in range L . Field computations then take fields as input (e.g., from sensors) and produce new fields as outputs, whose values may change over time (e.g., as inputs change or the computation progresses). For example, the input of a computation might be a field of temperatures, as perceived by sensors at each device in the network, and its output might be a Boolean field that maps to true where temperature is greater than 25 • C, and to false elsewhere.

Field Calculus

The field calculus [START_REF] Viroli | A calculus of computational fields[END_REF] is a tiny functional calculus capturing the essential elements of field computations, much as λ -calculus [START_REF] Church | A set of postulates for the foundation of logic[END_REF] captures the essence of functional computation and FJ [START_REF] Igarashi | Featherweight Java: A minimal core calculus for Java and GJ[END_REF] the essence of object-oriented programming. The primitive expressions of field calculus are data values denoted (Boolean, numbers, and pairs), representing constant fields holding the value everywhere, and variables x, which are either function parameters or state variables (see the rep construct below). These are composed into programs using a Lisp-like syntax with five constructs: (1) Built-in function call (o e 1 • • • e n ): A built-in operator o is a means to uniformly model a variety of "point-wise" operations, i.e. involving neither state nor communication. Examples include simple mathematical functions (e.g., addition, comparison, sine) and context-dependent operators whose result depends on the environment (e.g., the 0-ary operator uid returns the unique numerical identifier δ of the device, and the 0-ary nbr-range operator yields a field where each device maps to a subfield mapping its neighbours to estimates of their current distance from the device). The expression

(o e 1 • • • e n ) thus
a) (if x (f (sns)) (g (sns))) f" f" f" f" f" f" f" g" g" g" g" (b) ((if x f g) (sns))
Fig. 1: Field calculus functions are evaluated over a domain of devices. E.g., in (a) the if operation partitions the network into two subdomains, evaluating f where field x is true and g where it is false (both applied to the output of sensor sns). With first-class functions, however, domains must be constructed dynamically based on the identity of the functions stored in the field, as in (b), which implements an equivalent computation.

(3) Time evolution (rep x e 0 e): The "repeat" construct supports dynamically evolving fields, assuming that each device computes its program repeatedly in asynchronous rounds. It initialises state variable x to the result of initialisation expression e 0 (a value or a variable), then updates it at each step by computing e against the prior value of x. For instance, (rep x 0 (+ x 1)) is the (evolving) field counting in each device how many rounds that device has computed. (4) Neighbourhood field construction (nbr e): Device-to-device interaction is encapsulated in nbr, which returns a field φ mapping each neighbouring device to its most recent available value of e (i.e., the information available if devices broadcast the value of e to their neighbours upon computing it). Such "neighbouring" fields can then be manipulated and summarised with built-in operators, e.g., (min-hood (nbr e)) outputs a field mapping each device to the minimum value of e amongst its neighbours.

(5) Domain restriction (if e 0 e 1 e 2 ): Branching is implemented by this construct, which computes e 1 in the restricted domain where e 0 is true, and e 2 in the restricted domain where e 0 is false.

Any field calculus computation may be thus be viewed as a function f taking zero or more input fields and returning one output field, i.e., having the signature f : (D → L ) k → (D → L ). Figure 1a illustrates this concept, showing an example with complementary domains on which two functions are evaluated. This aggregatelevel model of computation over fields can then be "compiled" into an equivalent system of local operations and message passing actually implementing the field calculus program on a distributed system [START_REF] Viroli | A calculus of computational fields[END_REF].

Higher-order Field Calculus The higher-order field calculus (HFC) is an extension of the field calculus with embedded first-class functions, with the primary goal of allowing it to handle functions just like any other value, so that code can be dynamically injected, moved, and executed in network (sub)domains. If functions are "first class" in the language, then: (i) functions can take functions as arguments and return a function as result (higher-order functions); (ii) functions can be created "on the fly" (anonymous The syntax of the calculus is reported in Fig. 2. Values in the calculus include fields φ , which are produced at run-time and may not occur in source programs; also, local values may be smoothly extended by adding other ground values (e.g., characters) and structured values (e.g., lists). Borrowing syntax from [START_REF] Igarashi | Featherweight Java: A minimal core calculus for Java and GJ[END_REF], the overbar notation denotes metavariables over sequences and the empty sequence is denoted by •. E.g., for expressions, we let e range over sequences of expressions, written e 1 , e 2 , . . . e n (n ≥ 0). The differences from the field calculus are as follows: function application expressions (e e) can take an arbitrary expression e instead of just an operator o or a user-defined function name f; anonymous functions can be defined (by syntax (fun (x) e)); and built-in operators, user-defined function names, and anonymous functions are values. This implies that the range of a field can be a function as well. To apply the functions mapped to by such a field, we have to be able to transform the field back into a single aggregatelevel function. Figure 1b illustrates this issue, with a simple example of a function call expression applied to a function-valued field with two different values.

How can we evaluate a function call with such a heterogeneous field of functions? It would seem excessive to run a separate copy of function f for every device that has f as its value in the field. At the opposite extreme, running f over the whole domain is problematic for implementation, because it would require devices that may not have a copy of f to help in evaluating f . Instead, we will take a more elegant approach, in which making a function call acts as a branch, with each function in the range applied only on the subspace of devices that hold that function. Formally, this may be expressed as transforming a function-valued field φ into a function f φ that is defined as:

f φ (ψ 1 , ψ 2 , . . . ) = f ∈φ (D) f (ψ 1 | φ -1 ( f ) , ψ 2 | φ -1 ( f ) , . . . ) (1)
where ψ i are the input fields, φ (D) is set of all functions held as data values by some devices in the domain D of φ , and

ψ i | φ -1 ( f )
is the restriction of ψ i to the subspace of only those devices that φ maps to function f . In fact, when the field of functions is constant, this reduces to be precisely equivalent to a standard function call. This means that we can view ordinary evaluation of function f as equivalent to creating a functionvalued field with a constant value f , then making a function call applying that field to its argument fields. This elegant transformation is the key insight of this paper, enabling first-class functions to be implemented with a minimal change to the existing semantics while also ensuring compatibility with the prior semantics as well, thus also inheriting its previously established desirable properties.

3 The Higher-order Field Calculus: Dynamic and Static Semantics Dynamic Semantics (Big-Step Operational Semantics) As for the field calculus [START_REF] Viroli | A calculus of computational fields[END_REF], devices undergo computation in rounds. In each round, a device sleeps for some time, wakes up, gathers information about messages received from neighbours while sleeping, performs an evaluation of the program, and finally emits a message to all neighbours with information about the outcome of computation before going back to sleep.

The scheduling of such rounds across the network is fair and non-synchronous. This section presents a formal semantics of device computation, which is aimed to represent a specification for any HFC-like programming language implementation. The syntax of the HFC calculus has been introduced in Section 2 (Fig. 2). In the following, we let meta-variable δ range over the denumerable set D of device identifiers (which are numbers). To simplify the notation, we shall assume a fixed program P. We say that "device δ fires", to mean that the main expression of P is evaluated on δ .

We model device computation by a big-step operational semantics where the result of evaluation is a value-tree θ , which is an ordered tree of values, tracking the result of any evaluated subexpression. Intuitively, the evaluation of an expression at a given time in a device δ is performed against the recently-received value-trees of neighbours, namely, its outcome depends on those value-trees. The result is a new value-tree that is conversely made available to δ 's neighbours (through a broadcast) for their firing; this includes δ itself, so as to support a form of state across computation rounds (note that any implementation might massively compress the value-tree, storing only enough information for expressions to be aligned). A value-tree environment Θ is a map from device identifiers to value-trees, collecting the outcome of the last evaluation on the neighbours. This is written δ → θ as short for δ 1 → θ 1 , . . . , δ n → θ n .

The syntax of field values, value-trees and value-tree environments is given in Fig. 3 (top). Figure 3 (middle) defines: the auxiliary functions ρ and π for extracting the root value and a subtree of a value-tree, respectively (further explanations about function π will be given later); the extension of functions ρ and π to value-tree environments; and the auxiliary functions args and body for extracting the formal parameters and the body of a (user-defined or anonymous) function, respectively. The computation that takes place on a single device is formalised by the big-step operational semantics rules given in Fig. 3 (bottom). The derived judgements are of the form δ ;Θ e ⇓ θ , to be read "expression e evaluates to value-tree θ on device δ with respect to the value-tree environment Θ ", where: (i) δ is the identifier of the current device; (ii) Θ is the field of the value-trees produced by the most recent evaluation of (an expression corresponding to) e on δ 's neighbours; (iii) e is a run-time expression (i.e., an expression that may contain field values); (iv) the value-tree θ represents the values computed for all the expressions encountered during the evaluation of e-in particular ρ(θ ) is the resulting value of expression e. The first firing of a device δ after activation or reset is performed with respect to the empty tree environment, while any other firing must consider the outcome of the most recent firing of δ (i.e., whenever Θ is not empty, it includes the value of the most recent evaluation of e on δ )-this is needed to support the stateful semantics of the rep construct.

The operational semantics rules are based on rather standard rules for functional languages, extended so as to be able to evaluate a subexpression e of e with respect to Field values, value-trees, and value-tree environments:

φ ::= δ → field value θ ::= v (θ )
value-tree Θ ::= δ → θ value-tree environment Auxiliary functions:

ρ(v (θ )) = v π i (v (θ 1 , . . . , θ n )) = θ i if 1 ≤ i ≤ n π ,n (v (θ 1 , . . . , θ n+2 )) = θ n+2 if ρ(θ n+1 ) = π i (θ ) = • otherwise π ,n (θ ) = • otherwise For aux ∈ ρ, π i , π ,n :    aux(δ → θ ) = aux(θ ) if aux(θ ) = • aux(δ → θ ) = • if aux(θ ) = • aux(Θ ,Θ ) = aux(Θ ), aux(Θ ) args(f) = x if (def f(x) e) body(f) = e if (def f(x) e) args((fun (x) e)) = x body((fun (x) e)) = e
Rules for expression evaluation:

δ ;Θ e ⇓ θ [E-LOC] δ ;Θ ⇓ () [E-FLD] φ = φ | dom(Θ )∪{δ } δ ;Θ φ ⇓ φ () [E-B-APP] δ ; π n+1 (Θ ) e n+1 ⇓ θ n+1 ρ(θ n+1 ) = o δ ; π 1 (Θ ) e 1 ⇓ θ 1 • • • δ ; π n (Θ ) e n ⇓ θ n v = ε o δ ;Θ (ρ(θ 1 ), . . . , ρ(θ n )) δ ;Θ e n+1 (e 1 , . . . , e n ) ⇓ v (θ 1 , . . . , θ n+1 ) [E-D-APP] δ ; π n+1 (Θ ) e n+1 ⇓ θ n+1 ρ(θ n+1 ) = args( ) = x 1 , . . . , x n δ ; π 1 (Θ ) e 1 ⇓ θ 1 • • • δ ; π n (Θ ) e n ⇓ θ n body( ) = e δ ; π ,n (Θ ) e[x 1 := ρ(θ 1 ) . . . x n := ρ(θ n )] ⇓ θ n+2 v = ρ(θ n+2 ) δ ;Θ e n+1 (e 1 , . . . , e n ) ⇓ v (θ 1 , . . . , θ n+2 ) [E-REP] 0 = ρ(Θ (δ )) if Θ = / 0 otherwise δ ; π 1 (Θ ) e[x := 0 ] ⇓ θ 1 1 = ρ(θ 1 ) δ ;Θ (rep x e) ⇓ 1 (θ 1 ) [E-NBR] Θ 1 = π 1 (Θ ) δ ;Θ 1 e ⇓ θ 1 φ = ρ(Θ 1 )[δ → ρ(θ 1 )] δ ;Θ (nbr e) ⇓ φ (θ 1 ) [E-THEN] δ ; π 1 (Θ ) e ⇓ θ 1 ρ(θ 1 ) = true δ ; π true,0 Θ e ⇓ θ 2 = ρ(θ 2 ) δ ;Θ (if e e e ) ⇓ (θ 1 , θ 2 ) [E-ELSE] δ ; π 1 (Θ ) e ⇓ θ 1 ρ(θ 1 ) = false δ ; π false,0 Θ e ⇓ θ 2 = ρ(θ 2 ) δ ;Θ (if e e e ) ⇓ (θ 1 , θ 2 )
Fig. 3: Big-step operational semantics for expression evaluation the value-tree environment Θ obtained from Θ by extracting the corresponding subtree (when present) in the value-trees in the range of Θ . This process, called alignment, is modelled by the auxiliary function π, defined in Fig. 3 (middle). The function π has two different behaviours (specified by its subscript or superscript): π i (θ ) extracts the i-th subtree of θ , if it is present; and π ,n (θ ) extracts the (n + 2)-th subtree of θ , if it is present and the root of the (n + 1)-th subtree of θ is equal to the local value .

Rules [E-LOC] and [E-FLD] model the evaluation of expressions that are either a local value or a field value, respectively. For instance, evaluating the expression 1 produces (by rule [E-LOC]) the value-tree 1 (), while evaluating the expression + produces the value-tree + (). Note that, in order to ensure that domain restriction is obeyed (cf.

Section 2), rule [E-FLD] restricts the domain of the value field φ to the domain of Θ augmented by δ .

Rule [E-B-APP] models the application of built-in functions. It is used to evaluate expressions of the form (e n+1 e 1 • • • e n ) such that the evaluation of e n+1 produces a value-tree θ n+1 whose root ρ(θ n+1 ) is a built-in function o. It produces the value-tree v (θ 1 , . . . , θ n , θ n+1 ), where θ 1 , . . . , θ n are the value-trees produced by the evaluation of the actual parameters e 1 , . . . , e n (n ≥ 0) and v is the value returned by the function.

Rule [E-B-APP] exploits the special auxiliary function ε, whose actual definition is abstracted away. This is such that ε o δ ;Θ (v) computes the result of applying built-in function o to values v in the current environment of the device δ . In particular, we assume that the built-in 0-ary function uid gets evaluated to the current device identifier (i.e., ε uid δ ;Θ () = δ ), and that mathematical operators have their standard meaning, which is independent from δ and Θ (e.g., ε + δ ;Θ (1, 2) = 3). The ε function also encapsulates measurement variables such as nbr-range and interactions with the external world via sensors and actuators. In order to ensure that domain restriction is obeyed, for each built-in function o we assume that:

ε o δ ;Θ (v 1 , • • • , v n ) is defined only if all the field values in v 1 , . . . , v n have domain dom(Θ ) ∪ {δ }; and if ε o δ ;Θ (v 1 , • • • , v n ) returns a field value φ , then dom(φ ) = dom(Θ ) ∪ {δ }.
For instance, evaluating the expression (+ 1 2) produces the value-tree 3 (1 (), 2 (), + ()). The value of the whole expression, 3, has been computed by using rule [E-B-APP] to evaluate the application of the sum operator + (the root of the third subtree of the value-tree) to the values 1 (the root of the first subtree of the value-tree) and 2 (the root of the second subtree of the value-tree). In the following, for sake of readability, we sometimes write the value v as short for the value-tree v (). Following this convention, the value-tree 3 (1 (), 2 (), + ()) is shortened to 3 (1, 2, +).

Rule [E-D-APP] models the application of user-defined or anonymous functions, i.e., it is used to evaluate expressions of the form (e n+1 e 1 • • • e n ) such that the evaluation of e n+1 produces a value-tree θ n+1 whose root = ρ(θ n+1 ) is a user-defined function name or an anonymous function. It is similar to rule [E-B-APP], however it produces a value-tree which has one more subtree, θ n+2 , which is produced by evaluating the body of the function with respect to the value-tree environment π ,n (Θ ) containing only the value-trees associated to the evaluation of the body of the same function .

To illustrate rule [E-REP] (rep construct), as well as computational rounds, we consider program (rep x 0 (+ x 1)) (cf. Section 2). The first firing of a device δ after activation or reset is performed againstthe empty tree environment. Therefore, according to rule [E-REP], to evaluate (rep x 0 (+ x 1)) means to evaluate the subexpression (+ 0 1), obtained from (+ x 1) by replacing x with 0. This produces the valuetree θ 1 = 1 (1 (0, 1, +)), where root 1 is the overall result as usual, while its sub-tree is the result of evaluating the third argument. Any subsequent firing of the device δ is performed with respect to a tree environment Θ that associates to δ the outcome of the most recent firing of δ . Therefore, evaluating (rep x 0 (+ x 1)) at the second firing means to evaluate the subexpression (+ 1 1), obtained from (+ x 1) by replacing x with 1, which is the root of θ 1 . Hence the results of computation are 1, 2, 3, and so on.

Value-trees also support modelling information exchange through the nbr construct, as of rule [E-NBR]. Consider the program e = (min-hood (nbr (sns-num))), where the 1-ary built-in function min-hood returns the lower limit of values in the range of its field argument, and the 0-ary built-in function sns-num returns the numeric value measured by a sensor. Suppose that the program runs on a network of three fully connected devices δ A , δ B , and δ C where sns-num returns 1 on δ A , 2 on δ B , and 3 on δ C . Considering an initial empty tree-environment / 0 on all devices, we have the following: the evaluation of (sns-num) on δ A yields 1 (sns-num) (by rules [E-LOC] and [E-B-APP], since ε sns-num δ A ; / 0 () = 1); the evaluation of (nbr (sns-num)) on δ A yields (δ A → 1) (1 (sns-num)) (by rule [E-NBR]); and the evaluation of e on δ A yields

θ A = 1 ((δ A → 1) (1 (sns-num)), min-hood) (by rule [E-B-APP], since ε min-hood δ A ; / 0 ((δ A → 1)) = 1)
. Therefore, after its first firing, device δ A produces the value-tree θ A . Similarly, after their first firing, devices δ B and δ C produce the value-trees

θ B = 2 ((δ B → 2) (2 (sns-num)), min-hood) θ C = 3 ((δ C → 3) (3 (sns-num)), min-hood)
respectively. Suppose that device δ B is the first device that fires a second time. Then the evaluation of e on δ B is now performed with respect to the value tree environment

Θ B = (δ A → θ A , δ B → θ B , δ C → θ C
) and the evaluation of its subexpressions (nbr(sns-num)) and (sns-num) is performed, respectively, with respect to the following value-tree environments obtained from Θ B by alignment:

Θ B = π 1 (Θ B ) = (δ A → (δ A → 1) (1 (sns-num)), δ B → • • • , δ C → • • • ) Θ B = π 1 (Θ B ) = (δ A → 1 (sns-num), δ B → 2 (sns-num), δ C → 3 (sns-num))
We have that ε sns-num δ B ;Θ B () = 2; the evaluation of (nbr (sns-num)) on δ B with respect to Θ B yields φ (2 (sns-num)) where φ = (δ A → 1, δ B → 2, δ C → 3); and ε min-hood δ B ;Θ B (φ ) = 1. Therefore the evaluation of e on δ B produces the value-tree 1 (φ (2 (sns-num)), min-hood). Namely, the computation at device δ B after the first round yields 1, which is the minimum of sns-num across neighbours-and similarly for δ A and δ C . We now present an example illustrating first-class functions. Consider the program ((pick-hood (nbr (sns-fun)))), where the 1-ary built-in function pick-hood returns at random a value in the range of its field argument, and the 0-ary built-in function sns-fun returns a 0-ary function returning a value of type num. Suppose that the program runs again on a network of three fully connected devices δ A , δ B , and δ C where sns-fun returns 0 = (fun () 0) on δ A and δ B , and returns 1 = (fun () e ) on δ C , where e = (min-hood (nbr (sns-num))) is the program illustrated in the previous example. Assume that sns-num returns 1 on δ A , 2 on δ B , and 3 on δ C . Then after its first firing, device δ A produces the value-tree

θ A = 0 ( 0 ((δ A → 0 ) ( 0 (sns-fun)), pick-hood), 0)
where the root of the first subtree of θ A is the anonymous function 0 (defined above), and the second subtree of θ A , 0, has been produced by the evaluation of the body 0 of 0 . After their first firing, devices δ B and δ C produce the value-trees

θ B = 0 ( 0 ((δ B → 0 ) ( 0 (sns-fun)), pick-hood), 0) θ C = 3 ( 1 ((δ C → 1 ) ( 1 (sns-fun)), pick-hood), θ C )
respectively, where θ C is the value-tree for e given in the previous example.

Suppose that device δ A is the first device that fires a second time. The computation is performed with respect to the value tree environment

Θ A = (δ A → θ A , δ B → θ B , δ C → θ C
) and produces the value-tree 1 ( 1 (φ ( 1 (sns-fun)), pick-hood), θ A ), where

φ = (δ A → 1 , δ C → 1 ) and θ A = 1 ((δ A → 1, δ C → 3) (1 (sns-num)), min-hood),
since, according to rule [E-D-APP], the evaluation of the body e of 1 (which produces the value-tree θ A ) is performed with respect to the value-tree environment π 1 ,0 (Θ A ) = (δ C → θ C ). Namely, device δ A executed the anonymous function 1 received from δ C , and this was able to correctly align with execution of 1 at δ C , gathering values perceived by sns-num of 1 at δ A and 3 at δ C .

Static Semantics (Type-Inference System) We have developed a variant of the Hindley-Milner type system [START_REF] Damas | Principal type-schemes for functional programs[END_REF] for the HFC calculus.This type system has two kinds of types, local types (the types for local values) and field types (the types for field values), and is aimed to guarantee the following two properties:

Type Preservation If a well-typed expression e has type T and e evaluates to a value tree θ , then ρ(θ ) also has type T. Domain Alignment The domain of every field value arising during the evaluation of a well-typed expression on a device δ consists of δ and of the aligned neighbours.

Alignment is key to guarantee that the semantics correctly relates the behaviour of if, nbr, rep and function application-namely, two fields with different domain are never allowed to be combined. Besides performing standard checks (i.e., in a function application expression (e n+1 e 1 • • • e n ) the arguments e 1 , . . . e n have the expected type; in an if-expression (if e 0 e 1 e 2 ) the condition e 0 has type bool and the branches e 1 and e 2 have the same type; etc.) the type system perform additional checks in order to ensure domain alignment. In particular, the type rules check that:

-In an anonymous function (fun (x) e) the free variables y of e that are not in x have local type. This prevents a device δ from creating a closure e = (fun (x) e)[y := φ ] containing field values φ (whose domain is by construction equal to the subset of the aligned neighbours of δ ). The closure e may lead to a domain alignment error since it may be shifted (via the nbr construct) to another device δ that may use it (i.e., apply e to some arguments); and the evaluation of the body of e may involve use of a field value φ in φ such that the set of aligned neighbours of δ is different from the domain of φ . -In a rep-expression (rep x w e) it holds that x, w and e have (the same) local type.

This prevents a device δ from storing in x a field value φ that may be reused in the next computation round of δ , when the set of the set of aligned neighbours may be different from the domain of φ . -In a nbr-expression (nbr e) the expression e has local type. This prevents the attempt to create a "field of fields" (i.e., a field that maps device identifiers to field values)-which is pragmatically often overly costly to maintain and communicate. -In an if-expression (if e 0 e 1 e 2 ) the branches e 1 and e 2 have (the same) local type.

This prevents the if-expression from evaluating to a field value whose domain is different from the subset of the aligned neighbours of δ .

We now illustrate the application of first-class functions using a pervasive computing example. In this scenario, people wandering a large environment (like an outdoor festival, an airport, or a museum) each carry a personal device with short-range pointto-point ad-hoc capabilities (e.g. a smartphone sending messages to others nearby via Bluetooth or Wi-Fi). All devices run a minimal "virtual machine" that allows runtime injection of new programs: any device can initiate a new distributed process (in the form of a 0-ary anonymous function), which the virtual machine spreads to all other devices within a specified range (e.g., 30 meters). For example, a person might inject a process that estimates crowd density by counting the number of nearby devices or a process that helps people to rendezvous with their friends, with such processes likely implemented via various self-organisation mechanisms. The virtual machine then executes these using the first-class function semantics above, providing predictable deployment and execution of an open class of runtime-determined processes.

Virtual Machine Implementation The complete code for our example is listed in Figure 4, with syntax coloring to increase readability: grey for comments, red for field calculus keywords, blue for user-defined functions, and green for built-in operators. In this code, we use the following naming conventions for built-ins: functions sns-* embed sensors that return a value perceived from the environment (e.g., sns-injection-point returns a Boolean indicating whether a device's user wants to inject a function); functions *-hood yield a local value obtained by aggregating over the field value φ in input (e.g., sum-hood sums all values in each neighbourhood); functions *-hood+ behave the same but exclude the value associated with the current device; and built-in functions pair, fst, and snd respectively create a pair of locals and access a pair's first and second component. Additionally, given a built-in o that takes n ≥ 1 locals an returns a local, the built-ins o[*,...,*] are variants of o where one or more inputs are fields (as indicated in the bracket, l for local or f for field), and the return value is a field, obtained by applying operator o in a point-wise manner. For instance, as = compares two locals returning a Boolean, =[f,f] is the operator taking two field inputs and returns a Boolean field where each element is the comparison of the corresponding elements in the inputs, and similarly =[f,l] takes a field and a local and returns a Boolean field where each element is the comparison of the corresponding element of the field in input with the local. The first two functions in Figure 4 implement frequently used self-organisation mechanisms. Function distance-to, also known as gradient [START_REF] Clement | Self-assembly and self-repairing topologies[END_REF][START_REF] Lin | The gradient model load balancing method[END_REF], computes a field of minimal distances from each device to the nearest "source" device (those mapping to true in the Boolean input field). This is computed by repeated application of the triangle inequality (via rep): at every round, source devices take distance zero, while all others update their distance estimates d to the minimum distance estimate through their neighbours (min-hood+ of each neighbour's distance estimate (nbr d) plus the distance to that neighbour nbr-range); source and non-source are discriminated by mux, a builtin "multiplexer" that operates like an if but differently from it always evaluates both branches on every device. Repeated application of this update procedure self-stabilises into the desired field of distances, regardless of any transient perturbations or faults [START_REF] Kutten | Time-adaptive self stabilization[END_REF]. The second self-organisation mechanism, gradcast, is a directed broadcast, achieved by a computation identical to that of distance-to, except that the values are pairs (note that pair[f,f] produces a field of pairs, not a pair of fields), with the second element set to the value of v at the source: min-hood operates on pairs by applying lexicographic ordering, so the second value of the pair is automatically carried along shortest paths from the source. The result is a field of pairs of distance and most recent value of v at the nearest source, of which only the value is returned.

The latter two functions in Figure 4 use these self-organisation methods to implement our simple virtual machine. Code mobility is implemented by function deploy, which spreads a 0-ary function g via gradcast, keeping it bounded within distance range from sources, and holding 0-ary function no-op elsewhere. The corresponding field of functions is then executed (note the double parenthesis). The virtual-machine then simply calls deploy, linking its arguments to sensors configuring deployment range and detecting who wants to inject which functions (and using (fun () 0) as no-op function).

In essence, this virtual machine implements a code-injection model much like those used in a number of other pervasive computing approaches (e.g., [START_REF] Mamei | Programming pervasive and mobile computing applications: The tota approach[END_REF][START_REF] Gelernter | Generative communication in linda[END_REF][START_REF] Butera | Programming a Paintable Computer[END_REF])-though of course it has much more limited features, since it is only an illustrative example. With these previous approaches, however, code shares lexical scope and cannot have its network domain externally controlled. Thus, injected code may spread through the network unpredictably and may interact unpredictably with other injected code that it encounters. The extended field calculus semantics that we have presented, however, ensures that injected code moves only within the range specified to the virtual machine and remains lexically isolated from different injected code, so that no variable can be unexpectedly affected by interactions with neighbours.

Simulated Example Application

We further illustrate the application of first-class functions with an example in a simulated scenario. Consider a museum, whose docents monitor their efficacy in part by tracking the number of patrons nearby while they are working. To monitor the number of nearby patrons, each docent's device injects the following anonymous function (of type: () → num):

(fun () (low-pass 0.5 (converge-sum (distance-to (sns-injection-point))

(sns-patron))))

This counts patrons using the function converge-sum defined in Figure 4(bottom), a simple version of another standard self-organisation mechanism [START_REF] Beal | Building blocks for aggregate programming of self-organising applications[END_REF] which operates like an inverse broadcast, summing the values sensed by sns-patron (1 for a patron, 0 for a docent) down the distance gradient back to its source-in this case the docent at the injection point. In particular, each device's local value is summed with those identifying it as their parent (their closest neighbour to the source, breaking ties with device unique identifiers from built-in function uid), resulting in a relatively balanced spanning tree of summations with the source at its root. This very simple version of summation is somewhat noisy on a moving network of devices, so its output is passed through a simple low-pass filter, the function low-pass, also defined in Figure 4(bottom), in order to smooth its output and improve the quality of estimate. Figure 5a shows a simulation of a docent and 250 patrons in a large 100x30 meter museum gallery. Of the patrons, 100 are a large group of school-children moving together past the stationary docent from one side of the gallery to the other, while the rest are wandering randomly. In this simulation, people move at an average 1 m/s, the docent and all patrons carry personal devices running the virtual machine, executing asynchronously at 10Hz, and communicating via low-power Bluetooth to a range of 10 meters. The simulation was implemented using the ALCHEMIST [START_REF] Pianini | Chemical-oriented simulation of computational systems with Alchemist[END_REF] simulation framework and the Protelis [START_REF] Pianini | Practical aggregate programming with PROTELIS[END_REF] incarnation of field calculus, updated to the extended version of the calculus presented in this paper.

In this simulation, at time 10 seconds, the docent injects the patron-counting function with a range of 25 meters, and at time 70 seconds removes it. Figure 5a shows two snapshots of the simulation, at times 11 (top) and 35 (bottom) seconds, while Figure 5b compares the estimated value returned by the injected process with the true value. Note that upon injection, the process rapidly disseminates and begins producing good estimates of the number of nearby patrons, then cleanly terminates upon removal.

Conclusion, Related and Future Work

Conceiving emerging distributed systems in terms of computations involving aggregates of devices, and hence adopting higher-level abstractions for system development, is a thread that has recently received a good deal of attention. A wide range of aggregate programming approaches have been proposed, including Proto [START_REF] Beal | Infrastructure for engineered emergence in sensor/actuator networks[END_REF], TOTA [START_REF] Mamei | Programming pervasive and mobile computing applications: The tota approach[END_REF], the (bio)chemical tuple-space model [START_REF] Viroli | Spatial coordination of pervasive services through chemical-inspired tuple spaces[END_REF], Regiment [START_REF] Newton | Region streams: Functional macroprogramming for sensor networks[END_REF], the σ τ-Linda model [START_REF] Viroli | Linda in space-time: an adaptive coordination model for mobile ad-hoc environments[END_REF], Paintable Computing [START_REF] Butera | Programming a Paintable Computer[END_REF], and many others included in the extensive survey of aggregate programming languages given in [START_REF] Beal | Organizing the aggregate: Languages for spatial computing[END_REF]. Those that best support self-organisation approaches to robust and environment-independent computations have generally lacked well-engineered mechanisms to support openness and code mobility (injection, update, etc.). Our contribution has been to develop a core calculus, building on the work presented in [START_REF] Viroli | A calculus of computational fields[END_REF], that smoothly combines for the first time self-organisation and code mobility, by means of the abstraction of "distributed function field". This combination of first-class functions with the domain-restriction mechanisms of field calculus allows the predictable and safe composition of distributed self-organisation mechanisms at runtime, thereby enabling robust operation of open pervasive systems. Furthermore, the simplicity of the calculus enables it to easily serve as both an analytical framework and a programming framework, and we have already incorporated this into Protelis [START_REF] Pianini | Practical aggregate programming with PROTELIS[END_REF], thereby allowing these mechanisms to be deployed both in simulation and in actual distributed systems.

Future plans include consolidation of this work, by extending the calculus and its conceptual framework, to support an analytical methodology and a practical toolchain for system development, as outlined in [START_REF] Beal | Building blocks for aggregate programming of self-organising applications[END_REF]. First, we aim to apply our approach to support various application needs for dynamic management of distributed processes [START_REF] Beal | Dynamically defined processes for spatial computers[END_REF], which may also impact the methods of alignment for anonymous functions. Second, we plan to isolate fragments of the calculus that satisfy behavioural properties such as self-stabilisation, quasi-stabilisation to a dynamically evolving field, or density independence, following the approach of [START_REF] Viroli | A calculus of self-stabilising computational fields[END_REF]. Finally, these foundations can be applied in developing APIs enabling the simple construction of complex distributed applications, building on the work in [START_REF] Beal | Building blocks for aggregate programming of self-organising applications[END_REF] to define a layered library of self-organisation patterns, and applying these APIs to support a wide range of practical distributed applications.

2 )

 2 produces a field mapping each device identifier δ to the result of applying o to the values at δ of its n ≥ 0 arguments e 1 , . . . , e n . (Function call (f e 1 . . . e n ): Abstraction and recursion are supported by function definition: functions are declared as (def f(x 1 . . . x n ) e) (where elements x i are formal parameters and e is the body), and expressions of the form (f e 1 . . . e n ) are the way of calling function f passing n arguments.

(

eFig. 2 :

 2 Fig.2: Syntax of HFC (differences from field calculus are highlighted in grey).

Fig. 4 :

 4 Fig. 4: Virtual machine code (top) and application-specific code (bottom).

  Estimated vs. True Count

Fig. 5 :

 5 Fig. 5: (a) Two snapshots of museum simulation: patrons (grey) are counted (black) within 25 meters of the docent (green). (b) Estimated number of nearby patrons (grey) vs. actual number (black) in the simulation.

This work has been partially supported by HyVar (www.hyvar-project.eu, this project has received funding from the European Unions Horizon 2020 research and innovation programme under grant agreement No 644298 -Damiani), by EU FP7 project SAPERE (www.sapere-project.eu, under contract No 256873 -Viroli), by ICT COST Action IC1402 ARVI (www.cost-arvi.eu -Damiani), by ICT COST Action IC1201 BETTY (www.behavioural-types.eu -Damiani), by the Italian PRIN 2010/2011 project CINA (sysma.imtlucca.it/cina -Damiani & Viroli), by Ateneo/CSP project SALT (salt.di.unito.it -Damiani), and by the United States Air Force and the Defense Advanced Research Projects Agency under Contract No. FA8750-10-C-0242 (Beal). The U.S. Government is authorized to reproduce and distribute reprints for Governmental purposes notwithstanding any copyright notation thereon. The views, opinions, and/or findings


Luca Padovani

Luca Novara

Types for Deadlock-Free Higher-Order Programs

Type systems for communicating processes are typically studied using abstract models -e.g., process algebras -that distill the communication behavior of programs but overlook their structure in terms of functions, methods, objects, modules. It is not always obvious how to apply these type systems to structured programming languages. In this work we port a recently developed type system that ensures deadlock freedom in the π-calculus to a higher-order language.

Introduction

In this article we develop a type system that guarantees well-typed programs that communicate over channels to be free from deadlocks. Type systems ensuring this property already exist [START_REF] Kobayashi | A type system for lock-free processes[END_REF][START_REF] Kobayashi | A new type system for deadlock-free processes[END_REF][START_REF] Padovani | Deadlock and Lock Freedom in the Linear π-Calculus[END_REF], but they all use the π-calculus as the reference language. This choice overlooks some aspects of concrete programming languages, like the fact that programs are structured into compartmentalized blocks (e.g., functions) within which only the local structure of the program (the body of a function) is visible to the type system, and little if anything is know about the exterior of the block (the callers of the function). The structure of programs may hinder some kinds of analysis: for example, the type systems in [START_REF] Kobayashi | A type system for lock-free processes[END_REF][START_REF] Kobayashi | A new type system for deadlock-free processes[END_REF][START_REF] Padovani | Deadlock and Lock Freedom in the Linear π-Calculus[END_REF] enforce an ordering of communication events and to do so they take advantage of the nature of π-calculus processes, where programs are flat sequences of communication actions. How do we reason on such ordering when the execution order is dictated by the reduction strategy of the language rather than by the syntax of programs, or when events occur within a function, and nothing is known about the events that are supposed to occur after the function terminates? We answer these questions by porting the type system in [START_REF] Padovani | Deadlock and Lock Freedom in the Linear π-Calculus[END_REF] to a higher-order functional language.

To illustrate the key ideas of the approach, let us consider the program send a (recv b) | send b (recv a) (1.1) consisting of two parallel threads. The thread on the left is trying to send the message received from channel b on channel a; the thread on the right is trying to do the opposite. The communications on a and b are mutually dependent, and the program is a deadlock. The basic idea used in [START_REF] Padovani | Deadlock and Lock Freedom in the Linear π-Calculus[END_REF] and derived from [START_REF] Kobayashi | A type system for lock-free processes[END_REF][START_REF] Kobayashi | A new type system for deadlock-free processes[END_REF] for detecting deadlocks is to assign each channel a number -which we call level -and to verify that channels are used in order according to their levels. In (1.1) this mechanism requires b to have smaller level than a in the leftmost thread, and a to have a smaller level than b in the rightmost thread. No level assignment can simultaneously satisfy both constraints. In order to perform these checks with a type system, the first step is to attach levels to channel types. We therefore assign the types ![int] m and ?[int] n respectively to a and b in the leftmost thread of (1.1), and ?[int] m and ![int] n to the same channels in the rightmost thread of (1.1). Crucially, distinct occurrences of the same channel have types with opposite polarities (input ? and output !) and equal level. We can also think of the assignments send : ∀ı.![int] ı → int → unit and recv : ∀ı.?[int] ı → int for the communication primitives, where we allow polymorphism on channel levels. In this case, the application send a (recv b) consists of two subexpressions, the partial application send a having type int → unit and its argument recv b having type int. Neither of these types hints at the I/O operations performed in these expressions, let alone at the levels of the channels involved. To recover this information we pair types with effects [START_REF] Amtoft | Type and Effect Systems: Behaviours for Concurrency[END_REF]: the effect of an expression is an abstract description of the operations performed during its evaluation. In our case, we take as effect the level of channels used for I/O operations, or ⊥ in the case of pure expressions that perform no I/O. So, the judgment

b : ?[int] n recv b : int & n
states that recv b is an expression of type int whose evaluation performs an I/O operation on a channel with level n. As usual, function types are decorated with a latent effect saying what happens when the function is applied to its argument. So,

a : ![int] m send a : int → m unit & ⊥
states that send a is a function that, applied to an argument of type int, produces a result of type unit and, in doing so, performs an I/O operation on a channel with level m. By itself, send a is a pure expression whose evaluation performs no I/O operations, hence the effect ⊥. Effects help us detecting dangerous expressions: in a call-by-value language an application e 1 e 2 evaluates e 1 first, then e 2 , and finally the body of the function resulting from e 1 . Therefore, the channels used in e 1 must have smaller level than those occurring in e 2 and the channels used in e 2 must have smaller level than those occurring in the body of e 1 . In the specific case of send a (recv b) we have ⊥ < n for the first condition, which is trivially satisfied, and n < m for the second one. Since the same reasoning on send b (recv a) also requires the symmetric condition (m < n), we detect that the parallel composition of the two threads in (1.1) is ill typed, as desired.

It turns out that the information given by latent effects in function types is not sufficient for spotting some deadlocks. To see why, consider the function

f def = λ x.(send a x; send b x)
which sends its argument x on both a and b and where ; denotes sequential composition. The level of a (say m) should be smaller than the level of b (say n), for a is used before b (we assume that communication is synchronous and that send is a potentially blocking operation). The question is, what is the latent effect that decorates the type of f , of the form int → h unit? Consider the two obvious possibilities: if we take h = m, then

recv a | f 3; recv b (1.2)
is well typed because the effect m of f 3 is smaller than the level of b in recv b, which agrees with the fact that f 3 is evaluated before recv b; if we take h = n, then

recv a; f 3 | recv b (1.3)
is well typed for similar reasons. This is unfortunate because both (1.3) and (1.2) reduce to a deadlock. To flag both of them as ill typed, we must refine the type of f to int → m,n unit where we distinguish the smallest level of the channels that occur in the body of f (that is m) from the greatest level of the channels that are used by f when f is applied to an argument (that is n). The first annotation gives information on the channels in the function's closure, while the second annotation is the function's latent effect, as before. So (1.2) is ill typed because the effect of f 3 is the same as the level of b in recv b and (1.3) is ill typed because the effect of recv a is the same as the level of f in f 3.

In the following, we define a core multithreaded functional language with communication primitives (Section 2), we present a basic type and effect system, extend it to address recursive programs, and state its properties (Section 3). Finally, we briefly discuss closely related work and a few extensions (Section 4). Proofs and additional material can be found in long version of the paper, on the first author's home page.

Language syntax and semantics

In defining our language, we assume a synchronous communication model based on linear channels. This assumption limits the range of systems that we can model. However, asynchronous and structured communications can be encoded using linear channels: this has been shown to be the case for binary sessions [START_REF] Dardha | Session types revisited[END_REF] and for multiparty sessions to a large extent [10, technical report].

We use a countable set of variables x, y, . . . , a countable set of channels a, b, . . . , and a set of constants k. Names u, . . . are either variables or channels. We consider a language of expressions and processes as defined below: We write _ for unused/fresh variables. Constants include the unitary value (), the integer numbers m, n, . . . , as well as the primitives fix, fork, new, send, recv whose semantics will be explained shortly. Processes are either threads e , or the restriction (νa)P of a channel a with scope P, or the parallel composition P | Q of processes. The notions of free and bound names are as expected, given that the only binders are λ 's and ν's. We identify terms modulo renaming of bound names and we write fn(e) (respectively, fn(P)) for the set of names occurring free in e (respectively, in P).

The reduction semantics of the language is given by two relations, one for expressions, another for processes. We adopt a call-by-value reduction strategy, for which we need to define reduction contexts E , . . . and values v, w, . . . respectively as:

E ::= [ ] E e vE v, w ::= k a λ x.e send v
The reduction relation -→ for expressions is defined by standard rules

(λ x.e)v -→ e{v/x} fix λ x.e -→ e{fix λ x.e/x}
and closed under reduction contexts. As usual, e{e /x} denotes the capture-avoiding substitution of e for the free occurrences of x in e.

Table 1. Reduction semantics of expressions and processes.

E [send a v] | E [recv a] a - -→ E [()] | E [v] E [fork v] τ - -→ E [()] | v() E [new()] τ - -→ (νa) E [a] a ∈ fn(E ) e -→ e e τ - -→ e P - -→ P P | Q - -→ P | Q P - -→ Q (νa)P - -→ (νa)Q = a P a - -→ Q (νa)P τ - -→ Q P ≡ - -→≡ Q P - -→ Q
The reduction relation of processes (Table 1) has labels , . . . that are either a channel name a, signalling that a communication has occurred on a, or the special symbol τ denoting any other reduction. There are four base reductions for processes: a communication occurs between two threads when one is willing to send a message v on a channel a and the other is waiting for a message from the same channel; a thread that contains a subexpression fork v spawns a new thread that evaluates v(); a thread that contains a subexpression new() creates a new channel; the reduction of an expression causes a corresponding τ-labeled reduction of the thread in which it occurs. Reduction for processes is then closed under parallel compositions, restrictions, and structural congruence. The restriction of a disappears as soon as a communication on a occurs: in our model channels are linear and can be used for one communication only; structured forms of communication can be encoded on top of this simple model (see Example 2 and [5]). Structural congruence is defined by the standard rules rearranging parallel compositions and channel restrictions, where () plays the role of the inert process.

We conclude this section with two programs written using a slightly richer language equipped with let bindings, conditionals, and a few additional operators. All these constructs either have well-known encodings or can be easily accommodated. The fresh channels a and b are used to collect the results from the recursive, parallel invocations of fibo. Note that expressions are intertwined with I/O operations. It is relevant to ask whether this version of fibo is deadlock free, namely if it is able to reduce until a result is computed without blocking indefinitely on an I/O operation.

Example 2 (signal pipe). In this example we implement a function pipe that forwards signals received from an input stream x to an output stream y: let cont = λx.let c = new() in (fork λ_.send x c); c in let pipe = fix λpipe.λx.λy.pipe (recv x) (cont y)

Note that this pipe is only capable of forwarding handshaking signals. A more interesting pipe transmitting actual data can be realized by considering data types such as records and sums [START_REF] Dardha | Session types revisited[END_REF]. The simplified realization we consider here suffices to illustrate a relevant family of recursive functions that interleave actions on different channels.

Since linear channels are consumed after communication, each signal includes a continuation channel on which the subsequent signals in the stream will be sent/received. In particular, cont x sends a fresh continuation c on x and returns c, so that c can be used for subsequent communications, while pipe x y sends a fresh continuation on y after it has received a continuation from x, and then repeats this behavior on the continuations. The program below connects two pipes: Even if the two pipes realize a cyclic network, we will see in Section 3 that this program is well typed and therefore deadlock free. Forgetting cont on line 4 or not forking the send on line 1, however, produces a deadlock.

Type and effect system

We present the features of the type system gradually, in three steps: we start with a monomorphic system (Section 3.1), then we introduce level polymorphism required by Examples 1 and 2 (Section 3.2), and finally recursive types required by Example 2 (Section 3.3). We end the section studying the properties of the type system (Section 3.4).

Core types

Let L def = Z ∪ {⊥, } be the set of channel levels ordered in the obvious way (⊥ < n < for every n ∈ Z); we use ρ, σ , . . . to range over L and we write ρ σ (respectively, ρ σ ) for the minimum (respectively, the maximum) of ρ and σ . Polarities p, q, . . . are non-empty subsets of {?, !}; we abbreviate {?} and {!} with ? and ! respectively, and {?, !} with #. Types t, s, . . . are defined by t, s ::= B p[t] n t → ρ,σ s where basic types B, . . . include unit and int. The type p[t] n denotes a channel with polarity p and level n. The polarity describes the operations allowed on the channel: ? means input, ! means output, and # means both input and output. Channels are linear resources: they can be used once according to each element in their polarity. The type t → ρ,σ s denotes a function with domain t and range s. The function has level ρ (its closure contains channels with level ρ or greater) and, when applied, it uses channels with level σ or smaller. If ρ = , the function has no channels in its closure; if σ = ⊥, the function uses no channels when applied. We write → as an abbreviation for → ,⊥ , so → denotes pure functions not containing and not using any channel.

Recall from Section 1 that levels are meant to impose an order on the use of channels: roughly, the lower the level of a channel, the sooner the channel must be used. We extend the notion of level from channel types to arbitrary types: basic types have level because there is no need to use them as far as deadlock freedom is concerned; the level of functions is written in their type. Formally, the level of t, written |t|, is defined as:

|B| def = |p[t] n | def = n |t → ρ,σ s| def = ρ (3.1)
Levels can be used to distinguish linear types, denoting values (such as channels) that must be used to guarantee deadlock freedom, from unlimited types, denoting values that have no effect on deadlock freedom and may be disregarded. We say that t is linear if |t| ∈ Z; we say that t is unlimited, written un(t), if |t| = .

Below are the type schemes of the constants that we consider. Some constants have many types (constraints are on the right); we write types(k) for the set of types of k.

() : unit n : int fix : (t → t) → t fork : (unit → ρ,σ unit) → unit new : unit → #[t] n n < |t| recv : ?[t] n → ,n t n < |t| send : ![t] n → t → n,n unit n < |t|
The type of (), of the numbers, and of fix are ordinary. The primitive new creates a fresh channel with the full set # of polarities and arbitrary level n. The primitive recv takes a channel of type ?[t] n , blocks until a message is received, and returns the message. The primitive itself contains no free channels in its closure (hence the level ) because the only channel it manipulates is its argument. The latent effect is the level of the channel, as expected. The primitive send takes a channel of type ![t] n , a message of type t, and sends the message on the channel. Note that the partial application send a is a function whose level and latent effect are both the level of a. Note also that in new, recv, and send the level of the message must be greater than the level of the channel: since levels are used to enforce an order on the use of channels, this condition follows from the observation that a message cannot be used until after it has been received, namely after the channel on which it travels has been used. Finally, fork accepts a thunk with arbitrary level ρ and latent effect σ and spawns the thunk into an independent thread (see Table 1). Note that fork is a pure function with no latent effect, regardless of the level and latent effect of the thunk. This phenomenon is called effect masking [START_REF] Amtoft | Type and Effect Systems: Behaviours for Concurrency[END_REF], whereby the effect of evaluating an expression becomes unobservable: in our case, fork discharges effects because the thunk runs in parallel with the code executing the fork.

We now turn to the typing rules. A type environment Γ is a finite map u 1 : t 1 , . . . , u n : t n from names to types. We write / 0 for the empty type environment, dom(Γ ) for the domain of Γ , and Γ (u) for the type associated with u in Γ ; we write Γ 1 , Γ 2 for the union of Γ 1 and Γ 2 when dom(Γ 1 )∩dom(Γ 2 ) = / 0. We also need a more flexible way of combining type environments. In particular, we make sure that every channel is used linearly by distributing different polarities of a channel to different parts of the program. To this aim, following [START_REF] Kobayashi | Linearity and the pi-calculus[END_REF], we define a partial combination operator + between types:

t + t def = t if un(t) p[t] n + q[t] n def = (p ∪ q)[t] n if p ∩ q = / 0 (3.2)
that we extend to type environments, thus:

Γ + Γ def = Γ , Γ if dom(Γ ) ∩ dom(Γ ) = / 0 (Γ , u : t) + (Γ , u : s) def = (Γ + Γ ), u : t + s (3.3)
For example, we have

(x : int, a : ![int] n ) + (a : ?[int] n ) = x : int, a : #[int] n
, so we might have some part of the program that (possibly) uses a variable x of type int along with channel a for sending an integer and another part of the program that uses the same channel a but this time for receiving an integer. The first part of the program would be typed in the environment x : int, a : ![int] n and the second one in the environment a : ?[int] n . Overall, the two parts would be typed in the environment x : int, a : #[int] n indicating that a is used for both sending and receiving an integer.

We Table 2. Core typing rules for expressions and processes.

Typing of expressions

[T-NAME] Γ , u : t u : t & ⊥ un(Γ ) Γ 1 + Γ 2 P | Q [T-NEW] Γ , a : #[t] n P Γ (νa)P
We are now ready to discuss the core typing rules, shown in Table 2. Judgments of the form Γ e : t & ρ denote that e is well typed in Γ , it has type t and effect ρ; judgments of the form Γ P simply denote that P is well typed in Γ .

Axioms [T-NAME] and [T-CONST] are unremarkable: as in all substructural type systems the unused part of the type environment must be unlimited. Names and constants have no effect (⊥); they are evaluated expressions that do not use (but may contain) channels.

In rule [T-FUN], the effect ρ caused by evaluating the body of the function becomes the latent effect in the arrow type of the function and the function itself has no effect. The level of the function is determined by that of the environment Γ in which the function is typed. Intuitively, the names in Γ are stored in the closure of the function; if any of these names is a channel, then we must be sure that the function is eventually used (i.e., applied) to guarantee deadlock freedom. In fact, |Γ | gives a slightly more precise information, since it records the smallest level of all channels that occur in the body of the function. We have seen in Section 1 why this information is useful. A few examples:

the identity function λ x.x has type int → ,⊥ int in any unlimited environment; the function λ _.a has type unit→ n,⊥ ![int] n in the environment a : ![int] n ; it contains channel a with level n in its closure (whence the level n in the arrow), but it does not use a for input/output (whence the latent effect ⊥); it is nonetheless well typed because a, which is a linear value, is returned as result; the function λ x.send x 3 has type ![int] n → ,n unit; it has no channels in its closure but it performs an output on the channel it receives as argument; the function λ x.(recv a + x) has type int → n,n int in the environment a : ?[int] n ; note that neither the domain nor the codomain of the function mention any channel, so the fact that the function has a channel in its closure (and that it performs some I/O) can only be inferred from the annotations on the arrow; the function λ x.send x (recv a) has type ![int] n+1 → n,n+1 unit in the environment a : ![int] n ; it contains channel a with level n in its closure and performs input/output operations on channels with level n + 1 (or smaller) when applied.

Rule [T-APP] deals with applications e 1 e 2 . The first thing to notice is the type environments in the premises for e 1 and e 2 . Normally, these are exactly the same as the type environment used for the whole application. In our setting, however, we want to distribute polarities in such a way that each channel is used for exactly one communication. For this reason, the type environment Γ 1 + Γ 2 in the conclusion is the combination of the type environments in the premises. Regarding effects, τ i is the effect caused by the evaluation of e i . As expected, e 1 must result in a function of type t → ρ,σ s and e 2 in a value of type t. The evaluation of e 1 and e 2 may however involve blocking I/O operations on channels, and the two side conditions make sure that no deadlock can arise. To better understand them, recall that reduction is call-by-value and applications e 1 e 2 are evaluated sequentially from left to right. Now, the condition τ 1 < |Γ 2 | makes sure that any I/O operation performed during the evaluation of e 1 involves only channels whose level is smaller than that of the channels occurring free in e 2 (the free channels of e 2 must necessarily be in Γ 2 ). This is enough to guarantee that the functional part of the application can be fully evaluated without blocking on operations concerning channels that occur later in the program. In principle, this condition should be paired with the symmetric one τ 2 < |Γ 1 | making sure that any I/O operation performed during the evaluation of the argument does not involve channels that occur in the functional part. However, when the argument is being evaluated, we know that the functional part has already been reduced a value (see the definition of reduction contexts in Section 2). Therefore, the only really critical condition to check is that no channels involved in I/O operations during the evaluation of e 2 occur in the value of e 1 . This is expressed by the condition τ 2 < ρ, where ρ is the level of the functional part. Note that, when e 1 is an abstraction, by rule [T-FUN] ρ coincides with |Γ 1 |, but in general ρ may be greater than |Γ 1 |, so the condition τ 2 < ρ gives better accuracy. The effect of the whole application e 1 e 2 is, as expected, the combination of the effects of evaluating e 1 , e 2 , and the latent effect of the function being applied. In our case the "combination" is the greatest level of any channel involved in the application. Below are some examples:

-(λ x.x) a is well typed, because both λ x.x and a are pure expressions whose effect is ⊥, hence the two side conditions of [T-APP] are trivially satisfied; -(λ x.x) (recv a) is well typed in the environment a : ?[int] n : the effect of recv a is n (the level of a) which is smaller than the level of the function; send a (recv a) is ill typed in the environment a : #[int] n because the effect of evaluating recv a, namely n, is the same as the level of send a;

-(recv a) (recv b) is well typed in the environment a : ?[int → int] 0 , b : ?[int] 1 . The effect of the argument is 1, which is not smaller than the level of the environment a : ?[int → int] 0 used for typing the function. However, 1 is smaller than , which is the level of the result of the evaluation of the functional part of the application. This application would be illegal had we used the side condition

τ 2 < |Γ 1 | in [T-APP].
The typing rules for processes are standard: [T-PAR] splits contexts for typing the processes in parallel, [T-NEW] introduces a new channel in the environment, and [T-THREAD] types threads. The effect of threads is ignored: effects are used to prevent circular dependencies between channels used within the sequential parts of the program (i.e., within expressions); circular dependencies that arise between parallel threads are indirectly detected by the fact that each occurrence of a channel is typed with the same level (see the discussion of (1.1) in Section 1).

Level polymorphism

Looking back at Example 1, we notice that fibo n c may generate two recursive calls with two corresponding fresh channels a and b. Since the send operation on c is blocked by recv operations on a and b (line 5), the level of a and b must be smaller than that of c. Also, since expressions are evaluated left-to-right and recv a + recv b is syntactic sugar for the application (+) (recv a) (recv b), the level of a must be smaller than that of b. Thus, to declare fibo well typed, we must allow different occurrences of fibo to be applied to channels with different levels. Even more critically, this form of level polymorphism of fibo is necessary within the definition of fibo itself, so it is an instance of polymorphic recursion [START_REF] Amtoft | Type and Effect Systems: Behaviours for Concurrency[END_REF].

The core typing rules in Table 2 do not support level polymorphism. Following the previous discussion on fibo, the idea is to realize level polymorphism by shifting levels in types. We define level shifting as a type operator ⇑ n , thus:

⇑ n B def = B ⇑ n p[t] m def = p[⇑ n t] n+m ⇑ n (t → ρ,σ s) def = ⇑ n t → n+ρ,n+σ ⇑ n s (3.4)
where + is extended from integers to levels so that n+ = and n+⊥ = ⊥. The effect of ⇑ n t is to shift all the finite level annotations in t by n, leaving and ⊥ unchanged. Now, we have to understand in which cases we can use a value of type ⇑ n t where one of type t is expected. More specifically, when a value of type ⇑ n t can be passed to a function expecting an argument of type t. This is possible if the function has level . We express this form of level polymorphism with an additional typing rule for applications:

[T-APP-POLY] Γ 1 e 1 : t → ,σ s & τ 1 Γ 2 e 2 : ⇑ n t & τ 2 Γ 1 + Γ 2 e 1 e 2 : ⇑ n s & (n + σ ) τ 1 τ 2 τ 1 < |Γ 2 | τ 2 <
This rule admits an arbitrary mismatch n between the level the argument expected by the function and that of the argument supplied to the function. The type of the application and the latent effect are consequently shifted by the same amount n.

Soundness of [T-APP-POLY

] can be intuitively explained as follows: a function with level has no channels in its closure. Therefore, the only channels possibly manipulated by the function are those contained in the argument to which the function is applied or channels created within the function itself. Then, the fact that the argument has level n + k rather than level k is completely irrelevant. Conversely, if the function has channels in its closure, then the absolute level of the argument might have to satisfy specific ordering constraints with respect to these channels (recall the two side conditions in [T-APP]). Since level polymorphism is a key distinguishing feature of our type system, and one that accounts for much of its expressiveness, we elaborate more on this intuition using an example. Consider the term fwd def = λ x.λ y.send y (recv x) which forwards on y the message received from x. The derivation . . .

[T-APP] y : ![int] 1 send y : int → 1,1 unit & ⊥ . . . [T-APP] x : ?[int] 0 recv x : int & 0 [T-APP] x : ?[int] 0 , y : ![int] 1 send y (recv x) : unit & 1 [T-FUN] x : ?[int] 0 λ y.send y (recv x) : ![int] 1 → 0,1 unit & ⊥ [T-FUN] fwd : ?[int] 0 → ![int] 1 → 0,1 unit & ⊥
does not depend on the absolute values 0 and 1, but only on the level of x being smaller than that of y, as required by the fact that the send operation on y is blocked by the recv operation on x. Now, consider an application fwd a, where a has type ?[int] 2 . The mismatch between the level of x (0) and that of a (2) is not critical, because all the levels in the derivation above can be uniformly shifted up by 2, yielding a derivation for

fwd : ?[int] 2 → ![int] 3 → 2,3 unit & ⊥
This shifting is possible because fwd has no free channels in its body (indeed, it is typed in the empty environment). Therefore, using [T-APP-POLY], we can derive

a : ?[int] 2 fwd a : ![int] 3 → 2,3 unit & ⊥
Note that (fwd a) is a function having level 2. This means that (fwd a) is not level polymorphic and can only be applied, through [T-APP], to channels with level 3. If we allowed (fwd a) to be applied to a channel with level 2 using [T-APP-POLY] we could derive

a : #[int] 2 fwd a a : unit & 2
which reduces to a deadlock. Example 3. To show that the term in Example 1 is well typed, consider the environment

Γ def = fibo : int → ![int] 0 → ,0 unit, n : int, c : ![int] 0
In the proof derivation for the body of fibo, this environment is eventually enriched with the assignments a : #[int] -2 and b : #[int] -1 . Now we can derive . . .

[T-APP] Γ fibo (n -2) : ![int] 0 → ,0 unit & ⊥ [T-NAME] a : ![int] -2 a : ![int] -2 & ⊥ [T-APP-POLY] Γ , a : ![int] -2 fibo (n -2) a : unit & -2
where the application fibo (n -2) a is well typed despite the fact that fibo (n -2) expects an argument of type ![int] 0 , while a has type ![int] -2 . A similar derivation can be obtained for fibo (n -1) b, and the proof derivation can now be completed.

Recursive types

Looking back at Example 2, we see that in a call pipe x y the channel recv x is used in the same position as x. Therefore, according to [T-APP-POLY], recv x must have the same type as x, up to some shifting of its level. Similarly, channel c is both sent on y and then used in the same position as y, suggesting that c must have the same type as y, again up to some shifting of its level. This means that we need recursive types in order to properly describe x and y. Instead of adding explicit syntax for recursive types, we just consider the possibly infinite trees generated by the productions for t shown earlier. In light of this broader notion of types, the inductive definition of type level (3.1) is still well founded, but type shift (3.4) must be reinterpreted coinductively, because it has to operate on possibly infinite trees. The formalities, nonetheless, are well understood.

It is folklore that, whenever infinite types are regular (that is, when they are made of finitely many distinct subtrees), they admit finite representations either using type variables and the familiar µ notation, or using systems of type equations [START_REF] Courcelle | Fundamental properties of infinite trees[END_REF]. Unfortunately, a careful analysis of Example 2 suggests that -at least in principle -we also need non-regular types. To see why, let a and c be the channels to which (recv x) and (cont y) respectively evaluate on line 2 of the example. Now:

x must have smaller level than a since a is received from x (cf. the types of recv).

y must have smaller level than c since c is sent on y (cf. the types of send).

x must have smaller level than y since x is used in the functional part of an application in which y occurs in the argument (cf. line 2 and [T-APP-POLY]).

Overall, in order to type pipe in Example 2 we should assign x and y the types t n and s n that respectively satisfy the equations

t n = ?[t n+2 ] n s n = ![t n+3 ] n+1 (3.5)
Unfortunately, these equations do not admit regular types as solutions. We recover typeability of pipe with regular types by introducing a new type constructor

t ::= • • • t n
that wraps types with a pending shift: intuitively t n and ⇑ n t denote the same type, except that in t n the shift ⇑ n on t is pending. For example, ?[int] 0 1 and ?[int] 2 -1 are both possible wrappings of ?

[int] 1 , while int → 0,⊥ ![int] 0 is the unwrapping of int → 1,⊥ ![int] 1 -1 .
To exclude meaningless infinite types such as • • • n n n we impose a contractiveness condition requiring every infinite branch of a type to contain infinite occurrences of channel or arrow constructors. To see why wraps help finding regular representations for otherwise non-regular types, observe that the equations

t n = ?[ t n 2 ] n s n = ![ t n+1 2 ] n+1 (3.6)
denote -up to pending shifts -the same types as the ones in (3.5), with the key difference that (3.6) admit regular solutions and therefore finite representations. For example, t n could be finitely represented as a familiar-looking µα.?[ α 2 ] n term. We should remark that t n and ⇑ n t are different types, even though the former is morally equivalent to the latter: wrapping is a type constructor, whereas shift is a type operator. Having introduced a new constructor, we must suitably extend the notions of type level (3.1) and type shift (3.4) we have defined earlier. We postulate

| t n | def = n + |t| ⇑ n t m def = ⇑ n t m
in accordance with the fact that • n denotes a pending shift by n (note that | • | extended to wrappings is well defined thanks to the contractiveness condition).

We also have to define introduction and elimination rules for wrappings. To this aim, we conceive two constants, wrap and unwrap, having the following type schemes:

wrap : ⇑ n t → t n unwrap : t n → ⇑ n t
We add wrap v to the value forms. Operationally, we want wrap and unwrap to annihilate each other. This is done by enriching reduction for expressions with the axiom and we are now able to find a typing derivation for it that uses regular types. In particular, we assign cont the type s n → s n+2 and pipe the type t n → s n → n, unit where t n and s n are the types defined in (3.6). Note that cont is a pure function because its effects are masked by fork and that pipe has latent effect since it loops performing recv operations on channels with increasing level. Because of the side conditions in [T-APP] and [T-APP-POLY], this means that pipe can only be used in tail position, which is precisely what happens above and in Example 2.

unwrap (wrap v) -→ v

Properties

To formulate subject reduction, we must take into account that linear channels are consumed after communication (last but one reduction in Table 1). This means that when a process P communicates on some channel a, a must be removed from the type environment used for typing the residual of P. To this aim, we define a partial operation Γthat removes from Γ , when is a channel. Formally:

Theorem 1 (subject reduction). If Γ P and P - -→ Q, then Γ - Q where Γ -τ def = Γ and (Γ , a : #[t] n ) -a def = Γ .
Note that Γa is undefined if a ∈ dom(Γ ). This means that well-typed programs never attempt at using the same channel twice, namely that channels in well-typed programs are indeed linear channels. This property has important practical consequences, since it allows the efficient implementation (and deallocation) of channels [START_REF] Kobayashi | Linearity and the pi-calculus[END_REF].

Deadlock freedom means that if the program halts, then there must be no pending I/O operations. In our language, the only halted program without pending operations is (structurally equivalent to) () . We can therefore define deadlock freedom thus: Definition 1. We say that P is deadlock free

if P τ - -→ * Q -→ implies Q ≡ () .
As usual, τ --→ * is the reflexive, transitive closure of τ --→ and Q -→ means that Q is unable to reduce further. Now, every well-typed, closed process is free from deadlocks: Theorem 2 (soundness). If / 0 P, then P is deadlock free.

Theorem 2 may look weaker than desirable, considering that every process P (even an ill-typed one) can be "fixed" and become part of a deadlock-free system if composed in parallel with the diverging thread fix λ x.x . It is not easy to state an interesting property of well-typed partial programs -programs that are well typed in uneven environments -or of partial computations -computations that have not reached a stable (i.e., irreducible) state. One might think that well-typed programs eventually use all of their channels. This property is false in general, for two reasons. First, our type system does not ensure termination of well-typed expressions, so a thread like send a (fix λ x.x) never uses channel a, because the evaluation of the message diverges. Second, there are threads that continuously generate (or receive) new channels, so that the set of channels they own is never empty; this happens in Example 2. What we can prove is that, assuming that a well-typed program does not internally diverge, then each channel it owns is eventually used for a communication or is sent to the environment in a message. To formalize this property, we need a labeled transition system describing the interaction of programs with their environment. Labels π, . . . We formalize the assumption concerning the absence of internal divergences as a property that we call interactivity. Interactivity is a property of typed processes, which we write as pairs Γ P, since the messages exchanged between a process and the environment in which it executes are not arbitrary in general.

Definition 2 (interactivity). Interactivity is the largest predicate on well-typed processes such that Γ P interactive implies Γ P and:

1. P has no infinite reduction P Clause [START_REF] Amtoft | Type and Effect Systems: Behaviours for Concurrency[END_REF] says that an interactive process does not internally diverge: it will eventually halt either because it terminates or because it needs interaction with the environment in which it executes. Clause (2) states that internal reductions preserve interactivity. Clause (3) states that a process with a pending output on a channel a must reduce to an interactive process after the output is performed. Finally, clause (4) states that a process with a pending input on a channel a may reduce to an interactive process after the input of a particular message v is performed. The definition looks demanding, but many conditions are direct consequences of Theorem 1. The really new requirements besides well typedness are convergence of P (1) and the existence of v (4). It is now possible to prove that well-typed, interactive processes eventually use their channels.

1 -→ P 1 2 -→ P 2 3 -→ • • • , and 2. if P -→ Q, then Γ -Q is interactive, and 3. if P a!v -→ Q and Γ = Γ , a : ![t] n , then Γ Q is interactive for some Γ ⊆ Γ ,
Theorem 3 (interactivity). Let Γ P be an interactive process such that a ∈ fn(P). Then P

π 1 -→ P 1 π 2 -→ • • • π n
-→ P n for some π 1 , . . . , π n such that a ∈ fn(P n ).

Concluding remarks

We have demonstrated the portability of a type system for deadlock freedom of πcalculus processes [START_REF] Padovani | Deadlock and Lock Freedom in the Linear π-Calculus[END_REF] to a higher-order language using an effect system [START_REF] Amtoft | Type and Effect Systems: Behaviours for Concurrency[END_REF]. We have shown that effect masking and polymorphic recursion are key ingredients of the type system (Examples 1 and 2), and also that latent effects must be paired with one more annotation -the function level. The approach may seem to hinder program modularity, since it requires storing levels in types and levels have global scope. In this respect, level polymorphism (Section 3.2) alleviates this shortcoming of levels by granting them a relative -rather than absolute -meaning at least for non-linear functions.

Other type systems for higher-order languages with session-based communication primitives have been recently investigated [START_REF] Gay | Linear type theory for asynchronous session types[END_REF][START_REF] Wadler | Propositions as sessions[END_REF][START_REF] Bono | Polymorphic Types for Leak Detection in a Session-Oriented Functional Language[END_REF]. In addition to safety, types are used for estimating bounds in the size of message queues [START_REF] Gay | Linear type theory for asynchronous session types[END_REF] and for detecting memory leaks [START_REF] Bono | Polymorphic Types for Leak Detection in a Session-Oriented Functional Language[END_REF]. Since binary sessions can be encoded using linear channels [START_REF] Dardha | Session types revisited[END_REF], our type system can address the same family of programs considered in these works with the advantage that, in our case, well-typed programs are guaranteed to be deadlock free also in presence of session interleaving. For instance, the pipe function in Example 2 interleaves communications on two different channels. The type system described by Wadler [START_REF] Wadler | Propositions as sessions[END_REF] is interesting because it guarantees deadlock freedom without resorting to any type annotation dedicated to this purpose. In his case the syntax of (well-typed) programs prevents the modeling of cyclic network topologies, which is a necessary condition for deadlocks. However, this also means that some useful program patterns cannot be modeled. For instance, the program in Example 2 is ill typed in [START_REF] Wadler | Propositions as sessions[END_REF].

The type system discussed in this paper lacks compelling features. Structured data types (records, sums) have been omitted for lack of space; an extended technical report [START_REF] Padovani | Types for Deadlock-Free Higher-Order Concurrent Programs[END_REF] and previous works [START_REF] Padovani | Type Reconstruction for the Linear π-Calculus with Composite and Equi-Recursive Types[END_REF][START_REF] Padovani | Deadlock and Lock Freedom in the Linear π-Calculus[END_REF] show that they can be added without issues. The same goes for non-linear channels [START_REF] Padovani | Deadlock and Lock Freedom in the Linear π-Calculus[END_REF], possibly with the help of dedicated accept and request primitives as in [START_REF] Gay | Linear type theory for asynchronous session types[END_REF]. True polymorphism (with level and type variables) has also been studied in the technical report [START_REF] Padovani | Types for Deadlock-Free Higher-Order Concurrent Programs[END_REF]. Its impact on the overall type system is significant, especially because level and type constraints (those appearing as side conditions in the type schemes of constants, Section 3.1) must be promoted from the metatheory to the type system. The realization of level polymorphism as type shifting that we have adopted in this paper is an interesting compromise between impact and flexibility. Our type system can also be relaxed with subtyping: arrow types are contravariant in the level and covariant in the latent effect, whereas channel types are invariant in the level. Invariance of channel levels can be relaxed refining levels to pairs of numbers as done in [START_REF] Kobayashi | A type system for lock-free processes[END_REF][START_REF] Kobayashi | A new type system for deadlock-free processes[END_REF]. This can also improve the accuracy of the type system in some cases, as discussed in [START_REF] Padovani | Deadlock and Lock Freedom in the Linear π-Calculus[END_REF] and [START_REF] Carbone | Progress as compositional lock-freedom[END_REF]. It would be interesting to investigate which of these features are actually necessary for typing concrete functional programs using threads and communication/synchronization primitives.

Type reconstruction algorithms for similar type systems have been defined [START_REF] Padovani | Type Reconstruction for the Linear π-Calculus with Composite and Equi-Recursive Types[END_REF][START_REF] Padovani | Type Reconstruction Algorithms for Deadlock-Free and Lock-Free Linear π-Calculi[END_REF]. We are confident to say that they scale to type systems with arrow types and effects.

e

  ::= k u λ x.e ee P, Q ::= e (νa)P P | Q Expressions comprise constants k, names u, abstractions λ x.e, and applications e 1 e 2 .

Example 1 (

 1 parallel Fibonacci function). The fibo function below computes the n-th number in the Fibonacci sequence and sends the result on a channel c: fix λfibo.λn.λc.if n ≤ 1 then send c n else let a = new() and b = new() in (fork λ_.fibo (n -1) a); (fork λ_.fibo (n -2) b); send c (recv a + recv b)

3 4 (

 4 let a = new() and b = new() in fork λ_.pipe a b); (fork λ_.pipe b (cont a))

  extend the function | • | to type environments so that |Γ | def = u∈dom(Γ ) |Γ (u)| with the convention that | / 0| = ; we write un(Γ ) if |Γ | = .

Example 4 .

 4 We suitably dress the code in Example 2 using wrap and unwrap: 1 let cont = λx.let c = new() in (fork λ_.send x (wrap c)); c in 2 let pipe = fix λpipe.λx.λy.pipe (unwrap (recv x)) (cont y)

  of transitions are defined by π ::= a?e a!v and the transition relation π -→ extends reduction with the rules a ∈ bn(C ) C [send a v] a!v -→ C [()] a ∈ bn(C ) fn(e) ∩ bn(C ) = / 0 C [recv a] a?e -→ C [e] where C ranges over process contexts C ::= E | (C | P) | (P | C ) | (νa)C . Messages of input transitions have the form a?e where e is an arbitrary expression instead of a value. This is just to allow a technically convenient formulation of Definition 2 below.

  and Γ = Γ , a : ?[t] n , then Γ Q{v/x} is interactive for some v and Γ ⊇ Γ such that n < |Γ \ Γ |.

[T-CONST] Γ k : t & ⊥ un(Γ ) t ∈ types(k) [T-FUN] Γ , x : t e : s & ρ Γ λ x.e : t → |Γ |,ρ s & ⊥ [T-APP] Γ 1 e 1 : t → ρ,σ s & τ 1 Γ 2 e 2 : t & τ 2 Γ 1 + Γ 2 e 1 e 2 : s & σ τ 1 τ 2 τ 1 < |Γ 2 | τ 2 < ρTyping of processes[T-THREAD] Γ e : unit & ρ Γ e [T-PAR] Γ 1 P Γ 2 Q

Acknowledgments. The authors are grateful to the reviewers for their detailed comments and useful suggestions. The first author has been supported by Ateneo/CSP project SALT, ICT COST Action IC1201 BETTY, and MIUR project CINA.