# Polymorphic Types for Leak Detection in a Session-Oriented Functional Language

Viviana Bono, Luca Padovani, Andrea Tosatto

► To cite this version:

Viviana Bono, Luca Padovani, Andrea Tosatto. Polymorphic Types for Leak Detection in a Session-Oriented Functional Language. 15th International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOOODS) / 33th International Conference on Formal Techniques for Networked and Distributed Systems (FORTE), Jun 2013, Florence, Italy. pp.83-98, 10.1007/978-3-642-38592-6_7. hal-01515251

HAL Id: hal-01515251

https://inria.hal.science/hal-01515251

Submitted on 27 Apr 2017

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

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

<figure><img src="image_1.png" /></figure>
# Polymorphic Types for Leak Detection in a Session-Oriented Functional Language

Viviana Bono, Luca Padovani, and Andrea Tosatto

Dipartimento di Informatica, Università di Torino, Italy

**Abstract.** Copyless message passing is a communication paradigm in which only pointers are exchanged between sender and receiver processes. Because of its nature, this paradigm requires that messages are treated as *linear* resources. Yet, even linear type systems leave room for scenarios where apparently well-typed programs may leak memory. In this work we develop a polymorphic type system for leak-free copyless messaging in a functional setting, where first-class functions can be used as messages.

## 1 Introduction

When communicating processes can access a shared address space, it is sensible to consider a *copyless* form of communication whereby only pointers to messages (instead of the messages themselves) are copied from senders to receivers. The Singularity Operating System [9,10] is a notable example of system making pervasive use of copyless communication. In Singularity, messages live in a shared area called *exchange heap* that, for practical reasons, cannot be garbage collected: data in this area must be explicitly allocated and deallocated. Messages travel through channels that are represented as pairs of *peer endpoints*: a message sent over one endpoint is received from the corresponding peer. Because channel endpoints can be sent as messages, they are also allocated in the exchange heap and explicitly managed.

Explicit memory management is a well-known source of hard-to-trace bugs. For this reason, it calls for the development of static analysis techniques meant to spot dangerous code. In [1,2] we have developed a type system for a language of processes that interact through copyless messaging: well-typed processes are guaranteed to be free from memory faults, memory leaks, and communication errors. The type system associates channel endpoints with *endpoint types* reminiscent of session types [7,8]. The present work extends the results of [2] to a language with first-class functions. For example,

$$g \stackrel{\text{def}}{=} \lambda c.\lambda x.\text{let } f, c' = \text{receive } c \text{ in close } c'; (f x)$$

is a function that, when applied to a channel endpoint *c* and a value *x*, transforms *x* through a function received from *c*. The *receive* *c* application evaluates to a pair consisting of the message received from *c* and *c* itself, the *let* destructs such pair and binds its components to the local variables *f* and *c'*, and
close c' deallocates c'. The explicit re-binding of c enables the type system to keep track of resource allocation and to spot violations in the memory management. Indeed, endpoints are linear resources that are consumed when used in a function application (like c and c' in receive c and close c') and acquired when obtained as result of a function application (like for f and c' returned by receive). In addition, the re-binding allows to assign different types to the same channel endpoint according to how the code uses it: the above function can be typed with the assignments c : ?(Int → Int).end and c' : end where the type of c denotes the fact that it can be used for receiving a message of type Int → Int (a linear function from integers to integers) and the type end of c' is the residual of c's type after receiving this message; end indicates that c' can be deallocated.

In [2] it was observed that it is possible to write apparently correct code that yields memory leaks, whereby an allocated region of the heap becomes inaccessible. This phenomenon manifests itself in the program

$$let a, b = \text{open unit in close (send b a)}$$

which creates a new channel represented as the two peer endpoints a and b and sends b over its own peer a. This code fragment can be typed using the assignment {a : T₁, b : S₁} where T₁ = !S₁.end and S₁ is the recursive type satisfying the equation S₁ = ?S₁.end. Note that in this code fragment every resource that is acquired is also consumed. Yet, after the execution of this code only endpoint a is actually deallocated, while endpoint b has become inaccessible because stored within its own queue. In [2] we rule out code like this by restricting the values that can be sent as messages depending on their type. The idea consists in looking at types for estimating the length of the chains of pointers originating from values with that type – we call such measure type weight – and then restricting messages to values whose type has a bounded weight. For example, the queue of an endpoint of type S₁ may contain a message of type S₁, therefore the weight of S₁ is unbounded, whereas the weight of T₁ is zero because a can only be used for sending messages, so its queue will never contain a message.

It turns out that the same technique does not work “out of the box” in a language with first-class functions. The problem is that arrow types only tell us what a function accepts and produces, but not which other (heap-allocated) values the function may use, while this information is essential for determining the weight of an arrow type. To illustrate the issue, consider the code fragment

$$let a, b = \text{open unit in close (send (g b) a)}$$

which is a little twist from the previous one. According to the definition of g, (g b) is a message that contains b. This code fragment can be typed with the assignment {a : T₂, b : S₂}, where T₂ = !(Int → Int).end and S₂ = ?(Int → Int).end. As before, this closed code fragment yields a memory leak due to b not being deallocated, but in this case the type Int → Int of the message in S₂ does not provide much information: we only know that (g b) is a function that may make use of a linear value, but the type of such linear value, which is key in order to assess the weight of Int → Int, is unknown. The solution we put
forward consists in decorating linear arrow types with an explicit weight, as in `Int w-→ Int`, to keep track of this information. In the above example, the weight of `S₂` should be strictly greater than `w`, because endpoint `b` carries messages of type `Int w-→ Int`. At the same time, `w` should not be smaller than the weight of `S₂`, because `(g b)` contains `b`. From this train of thoughts, one infers that there is no finite bound for `w`, and consequently that `(g b)` cannot be safely sent over `a`.

Polymorphism adds another dimension to the problem and forces us to consider a more structured representation of type weights. For example, the function

$$ forward \stackrel{\text{def}}{=} \lambda x.\lambda y.\text{let } m, x' = \text{receive } x \text{ in } (x', \text{send } m y) $$

which forwards a message from an endpoint `x` to another endpoint `y`, can be given the polymorphic type `?a.A → !a.B w-→ A ⊗ B`. The issue is how to determine the weight `w`, given that `x` occurs free in the function `λy...` and that it has the partially specified type `?a.A`. The actual weight of `?a.A` depends on the weight of the types with which `a` and `A` are instantiated. In particular, it is the maximum between the weight of `A` and the weight of `a` plus 1 (because the queue for `x` may contain a value of type `a`). We keep track of this dependency by letting `w = {a, A} + 1`.

In the rest of the paper we formalize all the notions sketched so far. We begin by defining syntax and reduction semantics of a core functional language equipped with session-oriented communication primitives (Section 2). We also provide a precise definition of “correct” programs as those that are free from memory faults, memory leaks, and communication errors. We proceed by presenting the type language (Section 3), the type system and its soundness results (Section 4). Related work (Section 5) and a few concluding remarks (Section 6) end the main body of the paper. Proofs of the results can be found in the long version of the paper [3].

## 2 Language

The syntax of our language is described in Table 1, where we use the following syntactic categories: `x`, `y` range over an infinite set of variables; `p`, `q` range over an infinite set of Pointers of pointers; `u` ranges over names, which are either variables or pointers, and `U`, `V` over sets of names; `E` ranges over expressions and `v` over values; we write `~v` to denote queues, namely finite sequences of values; `k` ranges over constants from the set `{unit, fix, fork, open, close, send, receive}`; `P`, `Q` range over processes; `μ` ranges over heaps. The sub-language of expressions is almost standard, except for the `let` construct which deconstructs pairs and binds their components to two variables. As usual, `λx.E` binds `x` in `E` and `let x, y = E₁ in E₂` binds `x` and `y` in `E₂`, therefore, bound and free names are defined in the usual way. We will sometimes write `let x = E₁ in E₂` in place of `let x, y = (E₁, unit) in E₂` where `y` is some fresh variable. Processes are parallel compositions of expressions, each expression representing a thread of execution. We identify processes modulo commutativity and associativity of
<table><caption>**Table 1.** Syntax of expressions, processes, values, and heaps.</caption><thead><tr><th></th><th>Expression</th><th>v</th><th>Value</th></tr></thead><tbody><tr><td>E</td><td>(value)</td><td>v</td><td>(pointer)</td></tr><tr><td>v</td><td>(variable)</td><td>p</td><td>(constant)</td></tr><tr><td>x</td><td>(pair)</td><td>k</td><td>(abstraction)</td></tr><tr><td>(E, E)</td><td>(application)</td><td>λx.E</td><td>(abstraction)</td></tr><tr><td>EE</td><td>(pattern match)</td><td>(v, v)</td><td>(pair)</td></tr><tr><td>let x, y = E in E</td><td></td><td></td><td></td></tr><tr><td>P</td><td>(thread)</td><td>μ</td><td>(empty heap)</td></tr><tr><td>⟨E⟩</td><td>(composition)</td><td>∅</td><td>(endpoint)</td></tr><tr><td>P || P</td><td></td><td>p ↦→ [q; v]</td><td>(composition)</td></tr><tr><td></td><td></td><td>μ, μ</td><td></td></tr></tbody></table>

||. We write $fn(E)$ and $fn(P)$ for denoting the set of free names occurring in $E$ and $P$.

In order to express the operational semantics of processes, we need an explicit representation of heaps as finite maps from pointers to endpoint structures $[p, \tilde{v}]$, which, in turn, are a pair containing a pointer and a queue of values, representing the messages received at that endpoint. The set of pointers to allocated endpoint structures is $dom(\mu)$, and we assume that the composition $\mu_1, \mu_2$ is defined only when $dom(\mu_1) \cap dom(\mu_2) = \emptyset$. A system is a pair $\mu \otimes P$ of a heap $\mu$ and a process $P$.

Table 2 defines the reduction semantics of expressions and of systems. Expressions reduce according to a conventional call-by-value semantics extended with pattern matching over pairs. Systems reduce as a consequence of expressions that are evaluated in threads and of primitive functions forking new threads and implementing the communication operations. Rule (R-THREAD) performs a step of computation within a thread. The evaluation context $\mathcal{E}$ [12,6] is an expression with a hole, denoted by $[]$, where computation in a thread happens next. Evaluation contexts are defined by

$$ \mathcal{E} ::= [] | (\mathcal{E}, E) | (v, \mathcal{E}) | \mathcal{E}E | v\mathcal{E} | \text{let } x, y = \mathcal{E} \text{ in } E | \text{let } x, y = v \text{ in } \mathcal{E} $$

and $\mathcal{E}[E]$ denotes the result of filling the hole in $\mathcal{E}$ with the expression $E$.

Rule (R-PAR) singles out threads running in parallel. Rule (R-FORK) spawns a new thread. Rule (R-OPEN) creates a channel as a pair of peer endpoints, by allocating two endpoint structures in the heap which point to each other and initially have an empty queue ($\varepsilon$ denotes the empty sequence of values). Rule (R-SEND) inserts a value $v$ on the queue of the peer endpoint of $p$. Rule (R-RECEIVE) extracts the head value from the queue associated with the endpoint pointed to by $p$. In both `send` and `receive`, the operation evaluates to the endpoint being used for communication, which is thus available for further operations. In the following we write $\implies$ for the reflexive, transitive closure of $\to$ and we write $\mu \otimes P \to$ if there exist no $\mu'$ and $P'$ such that $\mu \otimes P \to \mu' \otimes P'$.

In this work, as in [2], we focus on three properties of systems: we wish every system to be fault free, where a fault is an attempt to use a pointer not
<table><caption>**Table 2.** Reduction semantics of expressions and systems.</caption><thead><tr><th colspan="4">Reduction of expressions</th></tr></thead><tbody><tr><td>(λx.E)v &rarr; v E{v/x}</td><td>fix(λx.E) &rarr; v E{fix(λx.E)/x}</td><td></td><td></td></tr><tr><td>let x, y = (v, w) in E &rarr; v E{v, w/x, y}</td><td></td><td></td><td></td></tr><tr><th colspan="4">Reduction of systems</th></tr><tr><td>(R-THREAD)<br>E &rarr; v E'<br>μ; &lang;E[E]&rang; &rarr; μ; &lang;E[E]&rang;</td><td>(R-FORK)<br>μ; &lang;E[fork E]&rang; &rarr; μ; &lang;E[unit]&rang; || &lang;E&rang;</td><td></td><td></td></tr><tr><td>(R-PAR)<br>μ; P<sub>1</sub> &rarr; μ'; P'<sub>1</sub><br>μ; P<sub>1</sub> || P<sub>2</sub> &rarr; μ'; P'<sub>1</sub> || P<sub>2</sub></td><td>(R-OPEN)<br>μ; &lang;E[open unit]&rang; &rarr; μ, p &mapsto; [q; ε], q &mapsto; [p; ε]; &lang;E[(p, q)]&rang;</td><td></td><td></td></tr><tr><td>(R-SEND)<br>μ, p &mapsto; [q; Q], q &mapsto; [p; Q']; &lang;E[send (v, p)]&rang; &rarr; μ, p &mapsto; [q; Q], q &mapsto; [p; Q'; v]; &lang;E[p]&rang;</td><td></td><td></td><td></td></tr><tr><td>(R-RECEIVE)<br>μ, p &mapsto; [q; vQ]; &lang;E[receive p]&rang; &rarr; μ, p &mapsto; [q; Q]; &lang;E[(v, p)]&rang;</td><td></td><td></td><td></td></tr></tbody></table>

corresponding to an allocated endpoint; we wish every system to be *leak free*, where a leak is an endpoint that becomes unreachable because no reference to it is directly or indirectly available to the processes in the system; finally, we wish every system to avoid *communication errors*, by enjoying (a limited form of) progress, meaning that no process in the system should get stuck while reading messages from a non-empty queue. We conclude this section by making these properties precise. In order to do so, we need to formalize the reachability of a heap object with respect to a set of *root pointers*. Intuitively, a process *P* may directly reach any object located at some pointer in the set *fn*(*P*) (we can think of the pointers in *fn*(*P*) as of the local variables of the process stored in its stack); from these pointers, the process may reach transitively other heap objects by reading messages from the queue of the endpoints it can reach.

**Definition 2.1 (reachable pointers).** We say that *p* is reachable from *q* in μ (written *p* ≺<sub>μ</sub> *q*) if *q* ↦→ [*r*; *ŵvŵ*'] ∈ μ and *p* ∈ *fn*(*v*). We write $\leqqquad$ for the reflexive and transitive closure of $\prec_{\mu}$. The pointers reachable from $\mathbb{U}$ in μ are defined as $\mu$-reach($\mathbb{U}$) = {$p \in \text{Pointers} \mid \exists q \in \mathbb{U} : p \leqq q$}.

We are now ready to define formally well-behaved processes.

**Definition 2.2 (well-behaved process).** We say that *P* is well behaved if for every possible reduction $\emptyset; P \Rightarrow \mu; Q$ the following properties hold:

$$1. \ dom(\mu) = \mu\text{-reach}(\mathrm{fn}(Q)).$$
<table><caption>**Table 3.** Syntax of types.</caption><thead><tr><th>σ ::=</th><th>Type Scheme</th><th>T ::=</th><th>Endpoint Type</th></tr></thead><tbody><tr><td>t</td><td>(monomorphic type)</td><td>end</td><td>(termination)</td></tr><tr><td>| ∀α :: ρ.σ</td><td>(polymorphic type)</td><td>| A<br>| A&#773;</td><td>(variable)<br>(dualized variable)</td></tr><tr><td>t ::=</td><td>Type</td><td>| ?t.T<br>| !t.T</td><td>(input)<br>(output)</td></tr><tr><td>| Unit</td><td>(unit type)</td><td>| rec A.T</td><td>(recursion)</td></tr><tr><td>| a</td><td>(variable)</td><td></td><td></td></tr><tr><td>| T</td><td>(endpoint type)</td><td></td><td></td></tr><tr><td>| t ⊗ t</td><td>(linear pair)</td><td>w ::=</td><td>Weight</td></tr><tr><td>| t → t</td><td>(function)</td><td>| ∞</td><td>(unbounded weight)</td></tr><tr><td>| t w-→ t</td><td>(linear function)</td><td>| X + n</td><td>(bounded weight)</td></tr></tbody></table>

2. if $Q = P_1 \parallel P_2$, then $\mu$-reach(fn($P_1$)) $\cap$ $\mu$-reach(fn($P_2$)) = $\emptyset$.

3. if $Q = \langle E \rangle \parallel Q'$ and $\mu_\beta \langle E \rangle \to$, then either $E = \text{unit}$, or $E = \mathcal{E}[\text{receive p}]$ and $q \mapsto [p; \varepsilon] \in \mu$, or $E = \mathcal{E}[\text{close p}]$ and $p \mapsto [q; \varepsilon] \in \mu$.

Conditions (1) and (2) ask for the absence of faults and leaks. In detail, condition (1) states that every allocated pointer in the heap is reachable by one process, and that every reachable pointer corresponds to an object allocated in the heap. Condition (2) states that processes are isolated, namely that no pointer is reachable from two or more processes. Since expressions of the form `close p` are persistent (they do not reduce), this condition rules out memory faults whereby the same endpoint is deallocated multiple times. Condition (3) requires the absence of communication errors, namely that if $\mu_\beta \nleq Q$ is stuck (no reduction is possible), then it is because every non-terminated process in $Q$ is waiting for a message on an endpoint having an empty queue. This configuration corresponds to a genuine deadlock where every process in some set is waiting for a message that is to be sent by another process in the same set. Condition (3) also ensures the absence of so-called *orphan messages*: no message accumulates in the queue of closed endpoints.

## 3 Types

Table 3 gives the syntax of types using the following syntactic categories: $m$, $n$ range over natural numbers; $A, B, \dots$ range over an infinite set of *endpoint type variables*; $a, b, \dots$ range over an infinite set of *value type variables*; $\alpha, \beta$ range over *type variables*, which are either *endpoint type variables* or *value type variables* without distinction; $X, Y$ range over finite sets of *type variables*; $\rho$ ranges over *qualifiers*, which are elements of $\{\text{any}, \text{fin}\}$; $w$ ranges over *weights*; $t, s$ range over *types*; $\sigma$ range over *type schemes*; $T, S$ range over *endpoint types*.

*Endpoint types* denote pointers to channel endpoints; they are fairly standard session types with input/output prefixes ?t/!t, recursion, and a terminal state end. Endpoint type variables $A$ can occur in dualized form $A\bar{A}$, as in [4]. This is
necessary for typing some functions, beside simplifying the definition of duality. For simplicity we omit choices and branches; they can be added without posing substantial problems. Types include the conventional constructs of functional languages à la ML, comprising a Unit type (other data types can be added as needed), linear functions, and linear pairs. The linear types are necessary to denote objects (functions, pairs) that contain channel endpoints and that, for this reason, must be owned and used linearly. In particular, the linear arrow type $t w \dashv s$ denotes a function whose body may contain pointers and has an explicit decoration $w$ determining its weight. A weight is a term representing the length of a chain of pointers in the program heap. It can be either $\infty$, denoting an unbound length, or $X + n$ denoting a length that is bound by the weight of the types that will instantiate the type variables in $X$ plus the value of the constant $n$. We will often write $X$ instead of $X + 0$ and $n$ instead of $\emptyset + n$. Type schemes are almost standard, except that polymorphic type variables are associated with a qualifier $\rho$: if the qualifier is any, then there is no constrain as to which types may instantiate the type variable; if the qualifier is fin, then only finite-weight types may instantiate the type variable. We will write $\tilde{t}$ for denoting sequences $t_1, \dots, t_n$ of types and we will often write $\forall \tilde{\alpha} :: \tilde{\rho}.t$ in place of $\forall \alpha_1 :: \rho_1 \dots \forall \alpha_n :: \rho_n.t$ for some $n$.

A type is *well formed* if none of its endpoint type variables bound by a *rec* occurs in a weight. For example, both $Unit\{A\} \dashv Unit$ and $\forall A :: any(Unit\{A\} \dashv Unit)$ are well formed, but $rec A.!(Unit\{A\} \dashv Unit).end$ is not. From now on we implicitly assume to work with well-formed types.

The predicate $\text{lin}(\sigma)$ identifies *linear types*:

$$ \text{lin}(\alpha) \quad \text{lin}(T) \quad \text{lin}(t_1 \otimes t_2) \quad \text{lin}(t_1 w \dashv t_2) \quad \frac{\text{lin}(t)}{\text{lin}(\forall \tilde{\alpha} :: \tilde{\rho}.t)} $$

We say that $\sigma$ is *unlimited*, notation $\text{un}(\sigma)$, if not $\text{lin}(\sigma)$. Note that a type variable is always considered linear because it may be instantiated by a linear type. A full-fledged type system might distinguish between linear and unlimited type variables for better precision; we leave this as a straightforward extension for the sake of simplicity.

There are three crucial notions regarding types that we need to define next, namely *duality*, *type weight*, *substitution*. It turns out that these notions are mutually dependent on one another and their formal definition requires a carefully ordered sequence of intermediate steps that relies on type well formedness. Here we only present the “final” definitions and highlight peculiarities and pitfalls of each, while the detailed development can be found in [3].

**Duality.** Communication errors are prevented by associating peer endpoints with dual endpoint types, so that when one endpoint type allows sending a message of type $t$, the dual endpoint type allows receiving messages of type $t$ and when one endpoint should be closed the other endpoint should be closed as well. Roughly, the dual of an endpoint type $T$, denoted by $\bar{T}$, is obtained from $T$ by swapping ?'s with !'s so that, for example, the dual of $?t.!?s.end$ is $!t.?!s.end$. In practice,
things are a little more complicated because of recursive behaviors. For example, the dual of $T = \text{rec } A.!A.end$ is not $S = \text{rec } A.?!A.end$. Indeed, in $T$ the recursion variable occurs within a prefix, denoting the fact that an endpoint of type $T$ carries messages which have themselves type $T$. That is, $T = !T.end$. By contrast, we have $S = ?S.end$, hence from an endpoint of type $S$ we can receive another endpoint having type $S$. In fact, we have $\overline{T} = ?T.end \neq S$.

The dual of an endpoint type is inductively defined by the equations:

$$ \begin{array}{lclcl} \overline{\text{end}} & = & \text{end} & & \overline{A} & = & \overline{A} \\ \overline{\text{rec } A.T} & = & \overline{\text{rec } A.T\{\overline{A}/A\}} & & \overline{A} & = & A \\ & & & & \overline{?t.T} & = & !t.\overline{T} \\ & & & & \overline{!t.T} & = & ?t.\overline{T} \end{array} $$

where $T\{\overline{A}/A\}$ denotes the endpoint type $T$ where free occurrences of $A$ have been replaced by its dualized form and free occurrences of $\overline{A}$ by $A$. For example, we have $\overline{\text{rec } A.?!A.end} = \overline{\text{rec } A.?!\overline{A}.end} = \overline{\text{rec } A.?!\overline{A}.end}$.

**Weight.** The weight of a type (scheme) gives information about the length of the chains of pointers originating from values having that type (scheme). For example, the weight of end is 0, because the queue of an endpoint of type end will never contain any message, hence no chains of pointers can originate from an endpoint of this type. On the contrary, an endpoint of type ?end.end may contain a pointer to another endpoint of type end, therefore its weight is 1. Because types may contain type variables, in general the weight of a type depends on how these type variables are instantiated. In order to compute the weight of a type, we must be able to compare weights:

**Definition 3.1 (weight order).** We define the relation $\leq$ over weights as the least partial order such that $w \leq \infty$ and $X + m \leq Y + n$ if $X \subseteq Y$ and $m \leq n$.

Observe that, if $W$ is the set of all weights, then $(W, \leq)$ is a complete lattice with least element $\emptyset + 0$ and greatest element $\infty$. In what follows we will use the operators $\vee$ and $\wedge$ to respectively compute the join and meet of possibly infinite sets of weights.

**Definition 3.2 (weight).** Let $\downarrow$ be the largest relation such that $t \downarrow w$ implies either

- $w = \infty$, or

- $t = \text{Unit}$ or $t = t_1 \to t_2$ or $t = \text{end}$ or $t = !s.T$, or

- $t = \alpha$ and $w = (X \cup \{\alpha\}) + n$, or

- $t = t_1 \otimes t_2$ and $t_1 \downarrow w$ and $t_2 \downarrow w$, or

- $t = ?s.T$ and $w = X + (n + 1)$ and $s \downarrow (X + n)$ and $T \downarrow w$, or

- $t = t_1 w' \to t_2$ and $w' \leq w$.

The weight of a type $t$, denoted $\|t\|$, is defined as $\|t\| \stackrel{\text{def}}{=} \bigwedge_{t \downarrow w} w$.

Intuitively, the relation $t \downarrow w$ says that $w$ is an upper bound for the length of the chains of pointers originating from values of type $t$, and $\|t\|$ is the least of such upper bounds. It is easy to see that every unlimited type has a null weight
(a value with unlimited type cannot contain any pointer) and that, for instance, $\|\alpha\| = \{\alpha\}$ and $\|t \otimes s\| = \|t\| \lor \|s\|$. Also, endpoints with type `end` or `!t.T` have null weight because their queues must be empty (this property will be enforced by the type system in Section 4). However, we have that $\|?a.end\| = \{a\} + 1$ because an endpoint of such type may contain a value of type `a`, so the length of the longest chain of pointers originating from such an endpoint is 1 plus the length of longest chain of pointers originating from a value with type that instantiates `a`. In general, we have $\|?t.T\| = (\|t\| + 1) \lor \|T\|$. If we take the endpoint type $S_1 = \text{rec } A. ?A. end$ from Section 1 we have $\|S_1\| = \infty$ because $S_1$ has no finite upperbound. Finally, note that $\|\bar{A}\| = \infty$. This is because, in general, there is no relationship between the weight of an endpoint type and that of its dual. For instance, we have $\|!S_1. end\| = 0$ but $\|!S_1. end\| = \|?S_1. end\| = \infty$. It would be possible to allow dualized type variables in the syntax of weights, but since such variables occur seldom in types we leave this extension out of our formal treatment and conservatively approximate their weight to $\infty$.

**Substitution.** Intuitively, a substitution $t\{s/\alpha\}$ represents the type obtained by replacing the occurrences of $\alpha$ in $t$ with $s$. This notion is standard, except for two features that are specific of our type language. The first feature is the presence of dualized endpoint type variables $\bar{A}$. The idea is that, when $A$ is replaced by an endpoint type $T$, $\bar{A}$ is replaced by $\bar{T}$, namely by the dual endpoint type of $T$ that we have just introduced. The second feature is the presence of type variables in weights which decorate linear function types. In particular, a substitution $(t_1 w \stackrel{\cdot}{\to} t_2)\{s/\alpha\}$ may need to update $w = X + n$ if $\alpha \in X$. Formally, we define a weight substitution operation $w\{w'/\alpha\}$ such that

$$ w\{w'/\alpha\} \stackrel{\text{def}}{=} \begin{cases} ((X \setminus \{\alpha\}) \lor w') + n & \text{if } w = X + n \text{ and } \alpha \in X \\ w & \text{otherwise} \end{cases} $$

where we define a meta operator $w+n$ such that $\infty+n = \infty$ and $(X+m)+n = X+(m+n)$. Then $t\{s/\alpha\}$ is defined in the standard way except that

$$ \bar{A}\{T/A\} = \bar{T} \quad \text{and} \quad (t_1 w \stackrel{\cdot}{\to} t_2)\{s/\alpha\} = t_1\{s/\alpha\} w\{\|s\|/\alpha\} \stackrel{\cdot}{\to} t_2\{s/\alpha\} $$

Finally, we generalize the notion of weight to type schemes so that $\|\forall \tilde{\alpha} :: \tilde{\rho}.t\| \stackrel{\text{def}}{=} \bigvee \|t\{\tilde{s}/\tilde{\alpha}\}\|$. Note that we do not worry about instantiating `fin-qualified` type variables with infinite-weight types, since such type variables can be instantiated with types having arbitrarily large weight anyway. Therefore, if the weight of $t$ depends in any way from one of the $\alpha_i$, the overall weight of the type scheme will be $\infty$, no matter what.

We identify types modulo folding/unfolding of recursions. That is, $\text{rec } A.T = T\{\text{rec } A.T/A\}$ (we have already used this property in Definition 3.2).

# 4 Type System

We give the types of the constants in Table 4. The types in the l.h.s. of the table are unremarkable. The `open` primitive returns a pair of peer channel endpoints
<table><caption>**Table 4.** Type of constants.</caption><tr><td>unit: Unit</td><td>open: ∀A :: any(Unit → (A ⊗ A))</td></tr><tr><td>fix: ∀a :: any.(a → a) → a</td><td>close: end → Unit</td></tr><tr><td>fork: Unit → Unit</td><td>send: ∀a :: fin.∀A :: any.(a ⊗ !a.A) → A<br>receive: ∀a :: fin.∀A :: any.?a.A → (a ⊗ A)</td></tr></table>

when applied to the `unit` value. For this reason, the resulting type is a pair of dual endpoint types. Because `open` is polymorphic, this can only be expressed using a dualized endpoint type variable. Note how `open` is an example of resource-producing function, accepting an unlimited value `unit` and returning a linear pair. The `close` primitive accepts an endpoint provided that it has type `end` and deallocates it. Being the converse of `open`, `close` is an example of resource-consuming function, accepting a linear value and not returning it. The `send` and `receive` constants implement the communication primitives: `send` accepts a message of type `a`, an endpoint of type `!a.A` that allows sending such a message, and returns the same endpoint with the residual type `A`; `receive` accepts an endpoint of type `?a.A`, reads a message of type `a` from such an endpoint, and returns the pair consisting of the received message and the endpoint with the residual type `A`. Observe that, in both `send` and `receive`, the value type variable `a` is qualified by `fin`, meaning that only values with finite-weight type can be sent and received. On the contrary, no constraint is imposed on `A`. In the following we write `TypeOf(k)` for the type scheme associated with `k` according to Table 4.

Judgments of the type system depend on two finite maps: the *type variable environment* $\Sigma = \{\alpha_i :: \rho_i\}_{i \in I}$ associates type variables with qualifiers, while the *name environment* $\Gamma = \{u_i :: \sigma_i\}_{i \in I}$ associates names with type schemes. In both cases we use $dom(\cdot)$ for denoting the set of type variables/names for which there is an association in the environment. We also write $\Sigma, \alpha :: \rho$ (respectively, $\Gamma, u :: \sigma$) to extend the environment whenever $\alpha \notin dom(\Sigma)$ (respectively, $u \notin dom(\Gamma)$). Finally, we write $\Gamma|_U$ for the restriction of $\Gamma$ to the names in $U$. Because name environments may contain linear entities (pointers) as well as unlimited ones, it is convenient to define also a more flexible (partial) operator $+$ for extending them. As in [5], we let

$$ \Gamma + u : \sigma = \begin{cases} \Gamma & \text{if } u : \sigma \in \Gamma \text{ and } \mathrm{un}(\sigma) \\ \Gamma, u : \sigma & \text{if } u \notin \mathrm{dom}(\Gamma) \\ \text{undefined} & \text{otherwise} \end{cases} $$

and we extend `+` to pairs of environments $\Gamma_1+\Gamma_2$ by induction on $\Gamma_2$ in the natural way. We write $\mathrm{lin}(\Gamma)$ if $\mathrm{lin}(\Gamma(u))$ for some $u \in dom(\Gamma)$ and $\mathrm{un}(\Gamma)$ otherwise.

Sometimes we will need to reason on the finiteness of a weight which contains type variables. In such cases, we use the information contained in a type variable environment for determining whether a weight is finite or not. More precisely, we write $\Sigma \vdash X + n < \infty$ whenever $\alpha :: \mathrm{fin} \in \Sigma$ for every $\alpha \in X$.
<table><caption>**Table 5.** Typing rules for processes and expressions.</caption><thead><tr><th>(T-THREAD)</th><th>(T-PAR)</th><th>(T-CONST)</th></tr></thead><tbody><tr><td>∅; Γ ⊢ E : Unit<br>Γ ⊢ &lt;E&gt;</td><td>Γ<sub>1</sub> ⊢ P<sub>1</sub> &nbsp;&nbsp;&nbsp;&nbsp; Γ<sub>2</sub> ⊢ P<sub>2</sub><br>Γ<sub>1</sub> + Γ<sub>2</sub> ⊢ P<sub>1</sub> || P<sub>2</sub></td><td>un(Γ) &nbsp;&nbsp;&nbsp;&nbsp; Σ ⊢ TypeOf(k) ≻ t<br>Σ; Γ ⊢ k : t</td></tr><tr><td>(T-NAME)<br>un(Γ) &nbsp;&nbsp;&nbsp;&nbsp; Σ ⊢ σ ≻ t<br>Σ; Γ, u : σ ⊢ u : t</td><td>(T-LET 1)<br>Σ, ˜α :: ˜ρ; Γ<sub>1</sub> ⊢ E<sub>1</sub> : t<sub>1</sub> &nbsp;&nbsp;&nbsp;&nbsp; Σ; Γ<sub>2</sub>, x : ∀α :: ˜ρ.t<sub>1</sub> ⊢ E<sub>2</sub> : t<sub>2</sub><br>Σ; Γ<sub>1</sub> + Γ<sub>2</sub> ⊢ let x = E<sub>1</sub> in E<sub>2</sub> : t<sub>2</sub></td><td></td></tr><tr><td>(T-PAIR)<br>∀i ∈ {1, 2} : Σ; Γ<sub>i</sub> ⊢ E<sub>i</sub> : t<sub>i</sub><br>Σ; Γ<sub>1</sub> + Γ<sub>2</sub> ⊢ (E<sub>1</sub>, E<sub>2</sub>) : t<sub>1</sub> ⊗ t<sub>2</sub></td><td>(T-LET 2)<br>Σ; Γ<sub>1</sub> ⊢ E<sub>1</sub> : t<sub>1</sub> ⊗ t<sub>2</sub> &nbsp;&nbsp;&nbsp;&nbsp; Σ; Γ<sub>2</sub>, x : t<sub>1</sub>, y : t<sub>2</sub> ⊢ E<sub>2</sub> : t<br>Σ; Γ<sub>1</sub> + Γ<sub>2</sub> ⊢ let x, y = E<sub>1</sub> in E<sub>2</sub> : t</td><td></td></tr><tr><td>(T-ARROW)<br>Σ; Γ, x : t ⊢ E : s &nbsp;&nbsp;&nbsp;&nbsp; un(Γ)<br>Σ; Γ ⊢ λx.E : t → s</td><td>(T-ARROW LIN)<br>Σ; Γ, x : t ⊢ E : s &nbsp;&nbsp;&nbsp;&nbsp; V<sub>u∈dom(Γ)</sub> ||Γ(u)|| ≤ w<br>Σ; Γ ⊢ λx.E : t w ↛ s</td><td></td></tr><tr><td>(T-APP)<br>Σ; Γ<sub>1</sub> ⊢ E<sub>1</sub> : t → s &nbsp;&nbsp;&nbsp;&nbsp; Σ; Γ<sub>2</sub> ⊢ E<sub>2</sub> : t<br>Σ; Γ<sub>1</sub> + Γ<sub>2</sub> ⊢ E<sub>1</sub>E<sub>2</sub> : s</td><td>(T-APP LIN)<br>Σ; Γ<sub>1</sub> ⊢ E<sub>1</sub> : t w ↛ s &nbsp;&nbsp;&nbsp;&nbsp; Σ; Γ<sub>2</sub> ⊢ E<sub>2</sub> : t<br>Σ; Γ<sub>1</sub> + Γ<sub>2</sub> ⊢ E<sub>1</sub>E<sub>2</sub> : s</td><td></td></tr></tbody></table>

A type scheme $\forall \tilde{\alpha} :: \tilde{\rho}.t$ denotes the family of types obtained from $t$ by instantiating each type variable $\alpha_i$ with a type whose weight respects the qualifier $\rho_i$. This is formally expressed by an *instantiation relation* $\Sigma \vdash \sigma \succ t$ defined by the rule

$$ \rho_i = \mathbf{fin} \Rightarrow \Sigma \vdash \|s_i\| < \infty \stackrel{(i=1..n)}{\Sigma \vdash \forall \tilde{\alpha} :: \tilde{\rho}.t \succ t\{\tilde{s}/\tilde{\alpha}\}} $$

For example, if we consider once again the endpoint types $T_1 = \text{rec } A. !S_1.\text{end}$ and $S_1 = \text{rec } A. ?A.\text{end}$ from Section 1 we have $\vdash$ TypeOf(send) $\succ$ $(T_1, !T_1.\text{end}) \to$ end because $T_1$ has finite weight so it can instantiate the type variable $a$ in TypeOf(send). On the contrary, $\vdash$ TypeOf(send) $\not\succ$ $(S_1, !S_1.\text{end}) \to$ end because $\|S_1\| = \infty$. Therefore, it is forbidden to send endpoints of type $S_1$.

The typing rules make use of two judgments, $\Gamma \vdash P$ stating that the process $P$ is well typed in the name environment $\Gamma$, and $\Sigma; \Gamma \vdash E : t$ stating that $E$ is well typed and has type $t$ in the type variable environment $\Sigma$ and name environment $\Gamma$. A judgment $\Gamma \vdash P$ is well formed if $dom(\Gamma) \subseteq$ Pointers and $\Gamma(p)$ is a closed type for every $p \in dom(\Gamma)$ and a judgment $\Sigma; \Gamma \vdash E$ is well formed if all type variables occurring free in $\Gamma$ are in $dom(\Sigma)$. Table 5 defines the typing rules for processes and expressions. Rule (T-THREAD) and (T-PAR) say that a process is well typed if so is each thread in it. Note that linear names are distributed linearly among threads by definition of $\Gamma_1 + \Gamma_2$. Rule (T-CONST) instantiates the type of a constant, while rule (T-NAME) retrieves and possibly instantiates the type of a name from the name environment. In both rules the unused part of the name environment must not contain linear resources. Rule (T-LET 1) is a linearity-aware
version of the rule to have let-polymorphism à la ML. The name environment is split between $E_1$ and $E_2$ knowing that, if $\ln(t_1)$, then $x$ must occur in $E_2$. Note that, by well formedness of $\Sigma$, $\tilde{\alpha} :: \tilde{\rho}$, none of the type variables in $\tilde{\alpha}$ can be in dom($\Sigma$) and hence can occur free in $\Gamma_2$. Therefore, they can be safely generalized when typing $E_2$. Overall, this treatment of universal polymorphism is borrowed from [12]: generalization and instantiation are embedded, respectively, in rule (T-LET 1), and in rules (T-CONST) and (T-NAME). Rules (T-PAIR) and (T-LET 2) are, respectively, the construction and the de-construction (via pattern matching) of linear pairs. Rules (T-ARROW) and (T-APP) are the standard ways of introducing and eliminating (unlimited) arrow types. The rule for arrow introduction requires the side condition $un(\Gamma)$, meaning that the body of the function does not make use of any pointer. Finally, rules (T-ARROW LIN) and (T-APP LIN) introduce and eliminate linear arrow types. In (T-ARROW LIN), the weight $w$ that annotates the linear arrow is chosen in such a way that it is an upper bound for the weights of the types of all names occurring in $E$.

**Example 4.1.** The following derivation, where we omit $\Sigma = a :: \text{fin}, A :: \text{any}, B :: \text{any}$ and we let $w = \|?a.A\| = \{a, A\}+1$, shows that the function *forward* defined at the end of Section 1 is well typed.

$$
\begin{array}{l@{\qquad}l}
x :: ?a.A \vdash \text{receive} x : a \otimes A & x' : A \vdash x' : A \qquad y :: !a.B, m : a \vdash \text{send} m y : B \\[2ex]
& y : !a.B, m : a, x' : A \vdash (x', \text{send} m y) : A \otimes B \\[2ex]
\cline{2-2}
x :: ?a.A, y :: !a.B \vdash \text{let } m, x' = \text{receive } x \text{ in } (x', \text{send } m y) : A \otimes B & x : ?a.A \vdash \lambda y. \text{let } m, x' = \text{receive } x \text{ in } (x', \text{send } m y) : !a.B w \dashv A \otimes B \\[2ex]
& \vdash \lambda x. \lambda y. \text{let } m, x' = \text{receive } x \text{ in } (x', \text{send } m y) : ?a.A \rightarrow !a.B w \dashv A \otimes B
\end{array}
$$

Note that $w$ is the smallest weight allowable in this derivation. Therefore, the obtained type is also the most precise and general one for *forward*. $\blacksquare$

**Example 4.2.** In a functional language, multi-argument functions are commonly represented in *curried form*, whereby such functions accept their arguments one at a time. On the contrary, the *send* constant is *uncurried*, because it accepts both its arguments at once in a pair. The *curry* combinator transforms an uncurried binary function into its curried form and is defined as *curry* = $\lambda f.\lambda x.\lambda y.f(x, y)$. Below is the derivation showing that *curry* is well typed, where we let $\Sigma = a :: \text{any}, b :: \text{any}, c :: \text{any}$.

$$
\begin{array}{c@{\quad}c@{\quad}c}
\begin{array}{l}
\Sigma; f : (a \otimes b) \rightarrow c \vdash f : (a \otimes b) \rightarrow c \\
\Sigma; f : (a \otimes b) \rightarrow c, x : a, y : b \vdash f (x, y) : c \\
\Sigma; f : (a \otimes b) \rightarrow c, x : a \vdash \lambda y.f (x, y) : b \{a\} \dashv c \\
\Sigma; f : (a \otimes b) \rightarrow c \vdash \lambda x.\lambda y.f (x, y) : a \rightarrow b \{a\} \dashv c \\
\emptyset \vdash \lambda f.\lambda x.\lambda y.f (x, y) : ((a \otimes b) \rightarrow c) \rightarrow a \rightarrow b \{a\} \dashv c
\end{array}
&
\begin{array}{l}
\Sigma; x : a \vdash x : a \qquad \Sigma; y : b \vdash y : b \\
\Sigma; x : a, y : b \vdash (x, y) : a \otimes b \\
\Sigma; x : a, y : b \vdash f (x, y) : c \\
\Sigma; x : a \vdash \lambda y.f (x, y) : b \{a\} \dashv c \\
\emptyset \vdash \lambda x.\lambda y.f (x, y) : a \rightarrow b \{a\} \dashv c
\end{array}
&
\begin{array}{l}
\Sigma; f : (a \otimes b) \rightarrow c \vdash f : (a \otimes b) \rightarrow c \\
\Sigma; f : (a \otimes b) \rightarrow c, x : a, y : b \vdash f (x, y) : c \\
\Sigma; f : (a \otimes b) \rightarrow c, x : a \vdash \lambda y.f (x, y) : b \{a\} \dashv c \\
\Sigma; f : (a \otimes b) \rightarrow c \vdash \lambda x.\lambda y.f (x, y) : a \rightarrow b \{a\} \dashv c \\
\emptyset \vdash \lambda f.\lambda x.\lambda y.f (x, y) : ((a \otimes b) \rightarrow c) \rightarrow a \rightarrow b \{a\} \dashv c
\end{array}
\end{array}
$$
Observe that the function returned by *curry* has type $a \to b\{a\} \to^c c$, where the linear arrow type has been decorated with the weight $\{a\}$. Indeed, the function $\lambda y.f(x, y)$ with this type has two free variables, $f$ having an unlimited type with null weight, and $x$ having type $a$. We can now obtain the curried form of *send* as *curry send* which can be given the polymorphic type $\forall a :: fin.\forall A :: any.a \to !a.A \{a\} \to^A A$.

**Example 4.3.** The *curry* function in Example 4.2 can only be applied to functions with unlimited type. It makes sense to consider also a linear variant *lcurry* of *curry* which has the same implementation of *curry* but can be used for currying linear functions (observe that the definition of *curry* uses its first argument $f$ exactly once). Using a derivation very similar to that shown in Example 4.2, *lcurry* could be given the type

$$ \forall a :: any.\forall b :: any.\forall c :: any.((a \otimes b) w \to^c c) \to a w \to^b (w \lor \{a\}) \to^c c $$

except that this type depends on the weight $w$ of the linear function being curried. This means that, in principle, we actually need a whole family $lcurry_w$ of combinators, one for each possible weight of the linear function to be curried. However, by combining polymorphism and explicit weight annotations in linear arrow types, we can provide *lcurry* with the most general type. The idea is to introduce another type variable, say $d$, which does not correspond to any actual argument of the function, but which represents an arbitrary weight, and to let $w = \{d\}$. This way we can give *lcurry* the type

$$ \forall a :: any.\forall b :: any.\forall c :: any.\forall d :: any.((a \otimes b) \{d\} \to^c c) \to a \{d\} \to^b a, d \to^c c $$

where we can instantiate $d$ with a type having exactly the weight of the linear function to be curried. For example, suppose we wish to apply *lcurry* to some function $f: (a \otimes b) n \to^c c$. Then it is enough to instantiate the $d$ variable in the type of *lcurry* with the type $T^{[n]}$ defined by

$$ T^{[0]} = \text{end} \qquad T^{[m+1]} = ?T^{[m]} \text{.end} $$

and obtain *lcurry* $f: a n \to^b (\{a\} + n) \to^c c$ as expected.

<figure><img src="image_2.png" /></figure>

**Properties.** In order to show that every well-typed process is well behaved (Definition 2.2) we need, as usual, a subject reduction result showing that well-typedness is preserved under reductions. Since in our language processes allocate and modify the heap, we need to define a concept of *well-typed heap* just as we have defined a concept of well-typed process. Intuitively, a heap $\mu$ is well typed with respect to an environment $\Gamma$ if the endpoints allocated in $\mu$ are consistent with their type in $\Gamma$. In particular, we want that whenever a message is inserted into the queue of an endpoint, the type of the message is consistent with the type of endpoint. To this aim, we define a function $\text{tail}(T, \tilde{t})$ that, given an endpoint type $T$ and a sequence of types $\tilde{t}$ of messages, computes the residual of $T$ after all the messages have been received:

$$ \text{tail}(T, \varepsilon) = T \qquad \frac{\text{tail}(T, \tilde{s}) = S}{\text{tail}(?t.T, t\tilde{s}) = S} $$
Note that tail(*T*, *s̃*) is undefined if *s̃* is not empty and *T* does not begin with input actions: only endpoints whose type begins with input actions can have messages in their queue. The weight of end and output endpoint types is zero because of this property (Definition 3.2).

The notion of well-typed heap is relative to a pair $\Gamma_0; \Gamma$ of disjoint name environments: the overall environment $\Gamma_0$, $\Gamma$ determines the type of all the objects allocated in the heap; the sub-environment $\Gamma$ distinguishes the *roots* of the heap (the pointers that are not reachable from any other pointer) from the sub-environment $\Gamma_0$ of the pointers that are stored within other structures in the heap and that are reachable from some root.

**Definition 4.1 (well-typed heap).** Let $\text{dom}(\Gamma) \cap \text{dom}(\Gamma_0) = \emptyset$. We say that $\mu$ is well typed in $\Gamma_0; \Gamma$, written $\Gamma_0; \Gamma \Vdash \mu$, if all of the following properties hold:

1. For every $\mathbf{p} \mapsto [\mathbf{q}; \tilde{\mathbf{v}}] \in \mu$ we have $\mathbf{p} \mapsto [\mathbf{q}; \tilde{\mathbf{w}}] \in \mu$ and either $\tilde{\mathbf{v}} = \varepsilon$ or $\tilde{\mathbf{w}} = \varepsilon$.

2. For every $\mathbf{p} \mapsto [\mathbf{q}; \tilde{\mathbf{v}}] \in \mu$ we have tail(*T*, *s̃*) = *S* where $\mathbf{p} : T \in \Gamma_0, \Gamma$ and $\Gamma_0|_{\text{fn}(v_i)} \vdash v_i : s_i$ and $\|s_i\| < \infty$ and $\mathbf{q} \mapsto [\mathbf{p}; \varepsilon] \in \mu$ then $\mathbf{q} : \bar{S} \in \Gamma_0, \Gamma$.

3. $\text{dom}(\mu) = \text{dom}(\Gamma_0, \Gamma) = \mu\text{-reach}(\text{dom}(\Gamma))$.

4. For every $U, V \subseteq \text{dom}(\Gamma)$ with $U \cap V = \emptyset$ we have $\mu\text{-reach}(U) \cap \mu\text{-reach}(V) = \emptyset$.

In words, condition (1) states that in any pair of peer endpoints, one queue is always empty. This condition corresponds to *half-duplex communication*, whereby it is not possible to send messages over one endpoint before all pending messages from that endpoint have been read. Condition (2) states that the content of the queue associated with an endpoint is consistent with the type of the endpoint, that all messages in a queue have a type with finite weight, and that the residual type of an endpoint after all of the enqueued messages are received is dual of the type of its peer. Condition (3) states that all objects in the heap are reachable from the roots. Since the root pointers will be distributed linearly among the processes in the system, this means that there are no leaks. Finally, condition (4) says that every object in the heap is reachable from exactly one root, ensuring process isolation. Now we formalize the notion of well-typed system.

**Definition 4.2 (well-typed system).** We say that the system $\mu;_P \mathbf{U}$ is well
typed *under* $\Gamma_0; \Gamma$, *written* $\Gamma_0; \Gamma \vdash \mu;_P \mathbf{U}$, *if* $\Gamma_0; \Gamma \Vdash \mu$ and $\Gamma \vdash \mathbf{P}$.

We conclude this section by stating the two main results: well-typedness of
systems is preserved by reductions and well-typed processes are well behaved.
The proof of Theorem 4.1 relies on the finite-weight restriction on the type of
messages for ensuring that no cycles are generated in the heap.

**Theorem 4.1 (subject reduction).** Let $\Gamma_0; \Gamma \vdash \mu;_P \mathbf{U}$ and $\mu;_P \mathbf{U} \rightarrow \mu';_P \mathbf{U}'$. Then $\Gamma'_0; \Gamma' \vdash \mu';_P \mathbf{U}'$ for some $\Gamma'_0$ and $\Gamma'$.

**Theorem 4.2 (soundness).** If $\Gamma \vdash P$ then $P$ is well behaved.
# 5 Related Work

This work is the convergence point of several lines of research, including the study and development of Singularity OS [9,10], the formalization of copyless messaging as a communication paradigm [1,2], the development of type systems for session-oriented functional languages [6], and polymorphic session types [4]. The fact that a linear type system is insufficient for preventing memory leaks in copyless messaging was first pointed out in [1,11]. In particular, in [1] and later in [2] we have put forward the idea of *type weight* as the characteristic quantity that allows us to discriminate between safe and unsafe messages. The main limit of the notion of type weight in [1,2] is that it is defined for endpoint types only, for which the weight is entirely determined by the structure of types. In this work we have shown that this is not always the case. Our motivation for studying the extension of the technique developed in [1,2] to a functional language is twofold: first of all, [6] already presents an elegant type system for such a language, even though [6] does not consider explicit memory management. Second, the *Sing#* programming language used for the development of Singularity OS includes features such as first-class and anonymous functions, which are commonly found in functional languages. In this setting, the idea of having functions as messages turns out to be a natural one. Another major difference between the present work and [6] is that we develop a truly polymorphic type system in the style of [12], while [6] only considers monomorphic types except for communication primitives which benefit from a form of *ad hoc* polymorphism. In this sense, the present work constitutes also a smooth extension of the type system in [6] with ML-style polymorphism. Interestingly, the polymorphic type of the *open* primitive crucially relies on dualized endpoint type variables, which were introduced in [4] for totally different reasons. Note also that [6] introduces a notion of “size” for session types that may be easily confused with out notion of type weight. In [6], the size estimates the maximum number of enqueued messages in an endpoint and it is used for efficient, static allocation of endpoints with finite-size type. Our weights are unrelated to the size of queues and concern the length of chains of pointers involving queues.

# 6 Conclusions and Future Work

The type language we have developed is a relatively simple variant of that required for ML-style functional languages. Many features that are practically relevant can be added without posing substantial issues. For instance, it is feasible to devise a subtyping relation it in the style of [6] whereby unlimited functions can be used in place of linear ones ($t \to s \le t w \to s$). Subtyping can also take into account weights, in the sense that it is safe to use a “lighter” function where a “heavier” function is expected ($t w \to s \le t w' \to s$ if $w \le w'$). It is also easy to equip endpoint types with the dual constructs $T \oplus S$ and $T + S$ for denoting internal and external choices driven by boolean values.

The finite-weight restriction on the type of messages prevents the formation of cycles in the heap. In the context of Singularity OS, this restriction seems
to be reasonable since objects allocated in the exchange heap are managed by
means of reference counting which cannot handle cyclic structures.

The type system we have presented (Table 5) is not syntax-directed and therefore leaves room for a fair amount of “guessing”, in particular with respect to the introduction of type variables in types and weights. An open question is whether it is feasible to devise a fully automated type and weight inference algorithm that is capable of inferring the most general type of arbitrary expressions.

***Acknowledgments.*** This work has been partially supported by MIUR PRIN 2010-2011 CINA. The authors are grateful to the anonymous referees for their comments.

References

1. V. Bono, C. Messa, and L. Padovani. Typing Copyless Message Passing. In *Proceedings of ESOP'11*, LNCS 6602, pages 57-76. Springer, 2011.

2. V. Bono and L. Padovani. Typing Copyless Message Passing. *Logical Methods in Computer Science*, 8:1–50, 2012.

3. V. Bono, L. Padovani, and A. Tosatto. Polymorphic Types for Leak Detection in a Session-Oriented Functional Language, 2013. Available at http://www.di.unito.it/~padovani/Papers/BonoPadovaniTosatto13.pdf.

4. S. Gay. Bounded Polymorphism in Session Types. *Mathematical Structures in Computer Science*, 18(5):895–930, 2008.

5. S. Gay and M. Hole. Subtyping for Session Types in the π-calculus. *Acta Informatica*, 42(2-3):191–225, 2005.

6. S. Gay and V. T. Vasconcelos. Linear Type Theory for Asynchronous Session Types. *Journal of Functional Programming*, 20(01):19–50, 2010.

7. K. Honda. Types for Dyadic Interaction. In *Proceedings of CONCUR'93*, LNCS 715, pages 509–523. Springer, 1993.

8. K. Honda, V. T. Vasconcelos, and M. Kubo. Language Primitives and Type Disciplines for Structured Communication-based Programming. In *Proceedings of ESOP'98*, LNCS 1381, pages 122–138. Springer, 1998.

9. G. Hunt, J. Larus, M. Abadi, M. Aiken, P. Barham, M. Fähndrich, C. Hawblitzel, O. Hodson, S. Levi, N. Murphy, B. Steensgaard, D. Tarditi, T. Wobber, and B. Zill. An Overview of the Singularity Project. Technical Report MSR-TR-2005-135, Microsoft Research, 2005.

10. G. C. Hunt and J. R. Larus. Singularity: Rethinking the Software Stack. *SIGOPS Operating Systems Review*, 41:37–49, April 2007.

11. J. Villard. *Heaps and Hops*. PhD thesis, Laboratoire Spécification et Vérification, ENS Cachan, France, 2011.

12. A. K. Wright and M. Felleisen. A syntactic approach to type soundness. *Information and Computation*, 115(1):38–94, 1994.