# Type-Based Analysis for Session Inference (Extended Abstract)

Carlo Spaccasassi, Vasileios Koutavas

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

## To cite this version:

Carlo Spaccasassi, Vasileios Koutavas. Type-Based Analysis for Session Inference (Extended Abstract). 36th International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE), Jun 2016, Heraklion, Greece. pp.248-266, 10.1007/978-3-319-39570-8_17 hal-01432922

HAL Id: hal-01432922

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

Submitted on 12 Jan 2017

HAL is a multi-disciplinary open access archive for the deposit and dissemination of scientific research documents, whether they are published 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_2.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
Type-Based Analysis for Session Inference
(Extended Abstract)*

Carlo Spaccasassi and Vasileios Koutavas

Trinity College Dublin

**Abstract.** We propose a type-based analysis to infer the session protocols of channels in an ML-like concurrent functional language. Combining and extending well-known techniques, we develop a type-checking system that separates the underlying ML type system from the typing of sessions. Without using linearity, our system guarantees communication safety and partial lock freedom. It also supports provably complete session inference for finite sessions with no programmer annotations. We exhibit the usefulness of our system with interesting examples, including one which is not typable in substructural type systems.

# 1 Introduction

Concurrent programming often requires processes to communicate according to intricate protocols. In mainstream programming languages these protocols are encoded implicitly in the program's control flow, and no support is available for verifying their correctness.

Honda [6] first suggested the use of *binary session types* to explicitly describe and check protocols over communication channels with two endpoints. Fundamentally, session type systems guarantee that a program respects the order of communication events (session fidelity) and message types (communication safety) described in a channel's session type. A number of session type systems (e.g., [2, 3, 16]) also ensure that processes fully execute the protocols of their open endpoints, as long as they do not diverge or block on opening new sessions (partial lock freedom).

To date, binary session type disciplines have been developed for various process calculi and high-level programming languages (see [8] for an overview) by following one of two main programming language design approaches: using a single substructural type system for both session and traditional typing [5, 7, 18, 19], or using monads to separate the two [13, 16].

In this paper we propose a third design approach which uses *effects*. Similar to previous work, our approach enables the embedding of session types in programming languages with sophisticated type systems. Here we develop a high-level language where intricate protocols of communication can be programmed and checked statically (Sect. 2). Contrary to both monads and substructural type

<footnote>* This research was supported, in part, by Science Foundation Ireland grant 13/RC/2094. The first author was supported by MSR (MRL 2011-039).</footnote>
systems, our approach allows pure code to call library code with communication effects, without having to refactor the pure code (e.g., to embed it in a monad or pass continuation channels through it—see Ex. 2.3). We apply our approach to ML<sub>S</sub>, a core of ML with session communication (Sect. 3).

Our approach separates traditional typing from session typing in a two-level system, which follows the principles of *typed based analysis* [12]. The first level employs a type-and-effect system, which adapts and extends the one of Amtoft, Nielson and Nielson [1] to session communication (Sect. 4). At this level the program is typed against an ML type and a *behaviour* which abstractly describes program structure and communication. Session protocols are not considered here—they are entirely checked at the second level. Thus, each endpoint is given type *Ses*<sup>ρ</sup>, where ρ statically approximates its source. The benefit of extending [1] is that we obtain a complete behaviour inference algorithm, which extracts a behaviour for every program respecting ML types.

At the second level, our system checks that a behaviour, given an operational semantics, complies with the session types of channels and endpoints (Sect. 5). The session discipline realised here is inspired by the work of Castagna et al. [3]. This discipline guarantees that programs comply with session fidelity and communication safety, but also, due to stacked interleaving of sessions, partial lock freedom. However, one of the main appeals of our session typing discipline is that it enables a provably *complete session types inference* from behaviours which, with behaviour inference, gives us a complete method for session inference from ML<sub>S</sub>, without programmer annotations (Sect. 6). The two levels of our system only interact through behaviours, which we envisage will allow us to develop front-ends for different languages and back-ends for different session disciplines.

To simplify the technical development we consider only sessions of finite interactions. However, we allow recursion in the source language, as long as it is *confined*: recursive code may only open new sessions and completely consume them (see Sect. 2). In Sect. 7 we discuss an extension to recursive types. Related work and conclusions can be found in Sect. 8. Details missing from this extended abstract can be found in the appendix for the benefit of the reviewers.

## 2 Motivating Examples

*Example 2.1 (A Swap Service)*. A coordinator process uses the primitive *acc-swp* to accept two connections on a channel *swp* (we assume functions *acc-c* and *req-c* for every channel *c*), opening two concurrent sessions with processes that want to exchange values. It then coordinates the exchange and recurs.

```haskell
let fun coord(-) =
  let val p1 = acc-swp ()
    val x1 = recv p1
    val p2 = acc-swp ()
    val x2 = recv p2
  in send p2 x1; send p1 x2; coord ()
  in spawn coord;
```

```haskell
let fun swap(x) =
  let val p = req-swp ()
    in send p x; recv p
  in spawn (fn _ => swap 1);
    spawn (fn _ => swap 2);
```
Each endpoint the coordinator receives from calling `acc-swp` are used according to the session type `?T.!T.end`. This says that, on each endpoint, the coordinator will first read a value type `T` (`?T`), then output a value of the same type (`!T`) and close the endpoint (`end`). The interleaving of sends and receives on the two endpoints achieves the desired swap effect.

Function `swap`: `Int→T'` calls `req-swp` and receives and endpoint which is used according to the session type `!Int.?T'.end`. By comparing the two session types above we can see that the coordinator and the swap service can communicate without type errors, and indeed are typable, when `T = Int = T'`. Our type inference algorithm automatically deduces the two session types from this code.

Because `swp` is a global channel, ill-behaved client code can connect to it too:

```hkl
let val p1 = req-swp () in send p1 1;
let val p2 = req-swp () in send p2 2;
let val (x1, x2) = (recv p1, recv p2) in ecl
```

This client causes a deadlock, because the coordinator first sends on `p2` and then on `p1`, but this code orders the corresponding receives in reverse. The interleaving of sessions in this client is rejected by our type system because it is not *well-stacked*: `recv p1` is performed before the most recent endpoint (`p2`) is closed. The interleaving in the coordinator, on the other hand, is well-stacked.

**Example 2.2 (Delegation for Efficiency).**

In the previous example the coordinator is a bottleneck when exchanged values are large. A more efficient implementation delegates exchange to the clients:

```hkl
let fun coord(-) =          let fun swap(x) =
let val p1 = acc-swp ()      let val p = req-swp ()
in sel-SWAP p1;                 in case p {
let val p2 = acc-swp          SWAP: send p x; recv p
in sel-LEAD p2;                LEAD: let val q = resume p
  deleg p2 p1;                 val y = recv q
coord()                        in send q x; y }
```

Function `swap` again connects to the coordinator over channel `swp`, but now offers two choices with the labels `SWAP` and `LEAD`. If the coordinator selects the former, the swap method proceeds as before; if it selects the latter, `swap` resumes (i.e., inputs) another endpoint, binds it to `q`, and performs a `rcv` and then a `send` on `q`. The new coordinator accepts two sessions on `swp`, receiving two endpoints: `p1` and `p2`. It selects `SWAP` on `p1`, `LEAD` on `p2`, sends `p1` over `p2` and recurs.

When our system analyses the coordinator in isolation, it infers the protocol $\eta_{coord} = (!SWAP.\eta' \oplus !LEAD.\eta'.end)$ for both endpoints `p1` and `p2`. When it analyses `swap`: $T_1 \to T_2$, it infers $\eta_p = \Sigma\{?SWAP.!T_1.?T_2.end, ?LEAD.?\eta_q.end\}$ and $\eta_q = ?T_2.!T_1.end$ as the protocols of `p` and `q`, respectively. The former selects either options `SWAP` or `LEAD` and the latter offers both options.

If the coordinator is type-checked in isolation, then typing succeeds with any $\eta'$: the coordinator can delegate any session. However, because of duality, the typing of `req-swp` in the swap function implies that $\eta' = \eta_q$ and $T_1 = T_2$. Our inference algorithm can type this program and derive the above session types.
*Example 2.3 (A Database Library)*. In this example we consider the implementation of a library which allows clients to connect to a database.

```hkl
let fun coord(-) =
  let val p = acc-db ()
  fun loop(-) = case p {
    QRY: let val sql = recv p
      val res = process sql
      in send p res; loop ()
    END: () }
  in spawn coord; loop ()
  in spawn coord;
```

```hkl
let fun clientinit (-) =
  let val con = req-db ()
  fun query.sql = sel-QRY con;
    send con sql;
    recv con
  fun close(-) = sel-END con
  in (query, close)
  in eclient
```

The coordinator accepts connections from clients on channel `db`. If a connection is established, after spawning a copy of the coordinator to serve other clients, the coordinator enters a loop that serves the connected client. In this loop it offers the client two options: `QRY` and `END`. If the client selects `QRY`, the coordinator receives an SQL query, processes it (calling `process`: `sql` → `dbresult`, with these types are defined in the library), sends back the result, and loops. If the client selects `END` the connection with the coordinator closes and the current coordinator process terminates.

Function `clientinit` is exposed to the client, which can use it to request a connection with the database coordinator. When called, it establishes a connection `con` and returns two functions to the client: `query` and `close`. Then, the client code `e_client` can apply the `query` function to an `sql` object and receive a `dbresult` as many times as necessary, and then invoke `close` to close the connection. Using our two-level inference system with recursion Sect. 7, we can infer the session type of the coordinator's endpoint `p`: $\mu X. \Sigma\{?QRY. ?sql. !dbresult.X, ?END.end\}$, and check whether the client code `e_client` respects it.

This example is not typable with a substructural type system because `query` and `close` share the same (linear) endpoint `con`. Moreover, in a monadic system `e_client` will need to be converted to monadic form.

## 3 Syntax and Operational Semantics of ML<sub>S</sub>

Fig. 1 shows the syntax and operational semantics of ML<sub>S</sub>, a core of ML with session communication. An expression can be one of the usual lambda expressions or `spawn e` which evaluates `e` to a function and asynchronously applies it to the unit value; it can also be `case e {L<sub>i</sub>: e<sub>i</sub>}<sub>i∈I</sub>` which, as we will see, implements finite *external choice*. We use standard syntactic sugar for writing programs. A *system S* is a parallel composition of closed expressions (*processes*).

The operational semantics of ML<sub>S</sub> are standard; here we only discuss session-related rules. Following the tradition of binary session types [7], communication between processes happens over dynamically generated entities called *sessions* which have exactly two *endpoints*. Thus, ML<sub>S</sub> values contain a countably infinite set of endpoints, ranged over by `p`. We assume a total involution $(\tilde{\cdot})$ over this set, with the property $\tilde{p} \neq p$, which identifies *dual endpoints*.
**Exp:** $e ::= v \mid (e, e) \mid ee \mid \text{let } x = e \text{ in } e \mid \text{if } e \text{ then } e \text{ else } e \mid spawn e \mid \text{case } e\{L_i : e_i\}_{i \in I}$

**Sys:** $S ::= e \mid S \parallel S$

**Val:** $v ::= x \mid k \in \text{Const} \mid (v, v) \mid \text{fn } x \Rightarrow e \mid \text{fun } f(x) = e \mid p$
$\mid \text{req-c} \mid \text{acc-c} \mid \text{send} \mid \text{recv} \mid \text{sel-L} \mid \text{deleg} \mid \text{resume}$

**ECxt:** $E ::= [\cdot] \mid (E, e) \mid (v, E) \mid Ee \mid vE \mid \text{let } x = E \text{ in } e \mid \text{if } E \text{ then } e \text{ else } e$
$\mid spawn E \mid \text{case } E\{L_i : e_i\}_{i \in I}$

RIFT if and then $e_1$ else $e_2 \leftrightarrow e_1$

RLET let $x = v$ in $e \leftrightarrow e[v/x]$

RIFF if and then $e_1$ else $e_2 \leftrightarrow e_2$

RFIX ($\text{fun } f(x) = e, v \leftrightarrow e[\text{fun } f(x) = e/f][v/x]$

RBETA

$E[e] \parallel S \rightarrow E[e'] \parallel S \quad \text{if } e \leftrightarrow e'$

RSPN

$E[spawn v] \parallel S \rightarrow E[()] \parallel v() \parallel S$

RINIT $E_1[\text{req-c}]() \parallel E_2[\text{acc-c}]() \parallel S \rightarrow E_1[p] \parallel E_2[\bar{p}] \parallel S \quad \text{if } p, \bar{p} \text{ fresh}$

RCOM $E_1[\text{send}(p, v)] \parallel E_2[\text{recv}\bar{p}] \parallel S \rightarrow E_1[()] \parallel E_2[v] \parallel S$

RDEL $E_1[\text{deleg}(p, p')] \parallel E_2[\text{resume}\bar{p}] \parallel S \rightarrow E_1[()] \parallel E_2[p'] \parallel S$

RSEL $E_1[\text{sel-L}_j p] \parallel E_2[\text{case}\bar{p}\{L_i : e_i\}_{i \in I}] \parallel S \rightarrow E_1[()] \parallel E_2[e_j] \parallel S \quad \text{if } j \in I$

<caption>**Fig. 1.** ML<sub>S</sub> syntax and operational semantics.</caption>

A process can request (or accept) a new session by calling `req-c` (resp., `acc-c`) with the unit value, which returns the endpoint (resp., dual endpoint) of a new session. Here `c` ranges over an infinite set of global initialisation channels. To simplify presentation, the language contains `req-c` and `acc-c` for each channel `c`.

Once two processes synchronise on a global channel and each receives a fresh, dual endpoint (`RINIT` reduction), they can exchange messages (`RCOM`), `delegate` endpoints (`RDEL`) and offer a number of choices $L_i \in I$, from which the partner can select one (`RSEL`). Here `L` ranges over a countably infinite set of choice labels, and `I` is a finite set of natural numbers; $L_i$ denotes a unique label for each natural number `i` and we assume `sel-L_i` for each $L_i$.

The next two sections present the two-level type system of ML<sub>S</sub>.

# 4 First Level Typing: ML Typing and Behaviours

Here we adapt and extend the type-and-effect system of Amtoft, Nielson and Nielson [1] to session communication in ML<sub>S</sub>. A judgement C; Γ ⊢ e : T △ b states that e has type T and behaviour b, under type environment Γ and constraint environment C. The constraint environment relates type-level variables to terms and enables type inference. These components are defined in Fig. 2.

An ML<sub>S</sub> expression can have a standard type or an endpoint type Ses<sup>ρ</sup>. Function types are annotated with a behaviour variable β. Type variables α are used for ML polymorphism. As in [1], Hindley-Milner polymorphism is extended with type schemas TS of the form ∀(γ: C<sub>0</sub>). T, where γ ranges over variables α, β, ρ, ψ, and C<sub>0</sub> imposes constraints on the quantified variables with fv(C<sub>0</sub>) ⊆ {γ}. Type environments Γ bind program variables to type schemas; we let ∀(Ø).T = T.

The rules of our type-and-effect system are shown in Fig. 3 which, as in [1, Sec. 2.8], is a conservative extension of ML. This system performs both ML
<figure><img src="image_3.png" /><figcaption>**Fig. 2.** Syntax of types, behaviours, constraints, and session types.</figcaption></figure>

type checking (including type-schema inference), and behaviour checking (which enables behaviour inference). Rules TLET, TVAR, TIF, TCONST, TAPP, TFUN, TSPAWN and the omitted rule for pairs perform standard type checking and straightforward sequential $(b_1; b_2)$ and non-deterministic $(b_1 \oplus b_2)$ behaviour composition; $\tau$ is the behaviour with no effect.

Just as a type constraint $T \subseteq \alpha$ associates type $T$ with type variable $\alpha$, a behaviour constraint $b \subseteq \beta$ associated behaviour $b$ to behaviour variable $\beta$. Intuitively, $\beta$ is the non-deterministic composition of all its associated behaviours. Rule TSUB allows the replacement of behaviour $b$ with variable $\beta$; such replacement in type annotations yields a subtyping relation ($C \vdash T <: T'$). Rules TINS and TGEN are taken from [1] and extend ML's type schema instantiation and generalisation rules, respectively. Because we extend Hindley-Milner's let polymorphism, generalisation (TGEN) is only applied to the right-hand side expression of the let construct. The following definition allows the instantiation of a type schema under a global constraint environment $C$. We write $C \vdash C'$ when $C'$ is included in the reflexive, transitive, compatible closure of $C$.

**Definition 4.1 (Solvability).** $\forall(\vec{\gamma} : C_0)$. $T$ is solvable by $C$ and substitution $\sigma$ when $\text{dom}(\sigma) \subseteq \{\vec{\gamma}\}$ and $C \vdash C_0\sigma$.

In TREC, the communication effect of the body of a recursive function should be *confined*, which means it may only use endpoints it opens internally. For this reason, the function does not input nor return open endpoints or other non-confined functions ($C \vdash \text{confd}(T, T')$). Although typed under $\Gamma$ which may contain endpoints and non-confined functions, the effect of the function body is recorded in its behaviour. The second level of our system checks that if the function is called, no endpoints from its environment are affected. It also checks that the function fully consumes internal endpoints before it returns or recurs.

A type $T$ is confined when it does not contain any occurrences of the endpoint type $\text{Ses}^\rho$ for any $\rho$, and when any $b$ in $T$ is confined. A behaviour $b$ is confined when all of its possible behaviours are either $\tau$ or recursive.

To understand rule TENDP, we have to explain region variables ($\rho$), which are related to region constants through $C$. Region constants are simple program annotations $l$ (produced during pre-processing) which uniquely identify the textual
TLET

$$
\frac{
  \begin{array}{l}
    C; \Gamma \vdash e_1 : TS \triangleright b_1 \\
    \phantom{C; \Gamma \vdash e_1 :} C; \Gamma, x : TS \vdash e_2 : T \triangleright b_2 \\
    C; \Gamma \vdash \text{let } x = e_1 \text{ in } e_2 : T \triangleright b_1 ; b_2
  \end{array}
}{
  C; \Gamma \vdash \text{let } x = e_1 \text{ in } e_2 : T \triangleright b_1 ; b_2
}
$$

TVAR

$$
C; \Gamma \vdash x : \Gamma(x) \triangleright \tau
$$

TIF

$$
\frac{
  \begin{array}{l}
    C; \Gamma \vdash e_1 : \mathbf{Bool} \triangleright b_1 \\
    \phantom{C; \Gamma \vdash e_1 :} C; \Gamma \vdash e_i : T \triangleright b_i \ (i \in \{1, 2\}) \\
    C; \Gamma \vdash \text{if } e_1 \text{ then } e_2 \text{ else } e_3 : T \triangleright b_1 ; (b_2 \oplus b_3)
  \end{array}
}{
  C; \Gamma \vdash \text{if } e_1 \text{ then } e_2 \text{ else } e_3 : T \triangleright b_1 ; (b_2 \oplus b_3)
}
$$

TCONST

$$
C; \Gamma \vdash k : \text{typeof}(k) \triangleright \tau
$$

TAPP

$$
\frac{
  \begin{array}{l}
    C; \Gamma \vdash e_1 : T' \xrightarrow{\beta} T \triangleright b_1 \\
    \phantom{C; \Gamma \vdash e_1 :} C; \Gamma \vdash e_2 : T' \triangleright b_2 \\
    C; \Gamma \vdash e_1 e_2 : T \triangleright b_1 ; b_2 ; \beta
  \end{array}
}{
  C; \Gamma \vdash e_1 e_2 : T \triangleright b_1 ; b_2 ; \beta
}
$$

TFUN

$$
\frac{
  \begin{array}{l}
    C; \Gamma, x : T \vdash e : T' \triangleright \beta \\
    \phantom{C; \Gamma, x : T \vdash e : } C; \Gamma \vdash \mathit{fn} x \Rightarrow e : T \xrightarrow{\beta} T' \triangleright \tau
  \end{array}
}{
  C; \Gamma \vdash \mathit{fn} x \Rightarrow e : T \xrightarrow{\beta} T' \triangleright \tau
}
$$

TMatch

$$
\frac{
  \begin{array}{l}
    C; \Gamma \vdash e : \mathit{Ses}^{\rho} \triangleright b \quad C; \Gamma \vdash e_i : T \triangleright b_i \ (i \in I) \\
    \phantom{C; \Gamma \vdash e : \mathit{Ses}^{\rho} \triangleright b \quad C; \Gamma \vdash e_i : T \triangleright b_i \ (i \in I)} \\
    C; \Gamma \vdash \mathit{case} \ e \ \{L_i : e_i\}_{i \in I} : T \triangleright b ; \ \& \ \{\rho?L_i : b_i\}
  \end{array}
}{
  C; \Gamma \vdash \mathit{case} \ e \ \{L_i : e_i\}_{i \in I} : T \triangleright b ; \ \& \ \{\rho?L_i : b_i\}
}
$$

TENDP

$$
C; \Gamma \vdash p^l : \mathit{Ses}^\rho \triangleright \tau \quad C \vdash \rho \sim l
$$

$$
\frac{
  \begin{array}{l}
    C; \Gamma \vdash e : \mathit{Unit} \xrightarrow{\beta} \mathit{Unit} \triangleright b \\
    \phantom{C; \Gamma \vdash e : \mathit{Unit} \xrightarrow{\beta} \mathit{Unit} \triangleright b} \\
    C; \Gamma \vdash \mathit{spawn} e : \mathit{Unit} \triangleright b ; \mathit{spawn} \beta
  \end{array}
}{
  C; \Gamma \vdash \mathit{spawn} e : \mathit{Unit} \triangleright b ; \mathit{spawn} \beta
}
$$

TSUB

$$
\frac{
  \begin{array}{l}
    C; \Gamma \vdash e : T \triangleright b \\
    \phantom{C; \Gamma \vdash e : T \triangleright b} C; \Gamma \vdash e : T' \triangleright \beta
  \end{array}
}{
  C \vdash T < : T' \\
  C \vdash b \subseteq \beta
}
$$

$$
\frac{
  \begin{array}{l}
    C; \Gamma, f : T \xrightarrow{\beta} T', x : T \vdash e : T' \triangleright b \\
    \phantom{C; \Gamma, f : T \xrightarrow{\beta} T', x : T \vdash e : T' \triangleright b} \\
    C; \Gamma \vdash \mathit{fun} f(x) = e : T \xrightarrow{\beta} T' \triangleright \tau
  \end{array}
}{
  C \vdash \mathit{confd}(T, T') \\
  C \vdash \mathit{rec}_{\beta} b \subseteq \beta
}
$$

$$
\frac{
  \begin{array}{l}
    C; \Gamma \vdash e : \forall(\vec{\gamma} : C_0). T \triangleright b \\
    \phantom{C; \Gamma \vdash e : \forall(\vec{\gamma} : C_0). T \triangleright b} \\
    C; \Gamma \vdash e : T \sigma \triangleright b
  \end{array}
}{
  C; \Gamma \vdash e : T \sigma \triangleright b
}
\quad \begin{array}{l}
  \mathrm{dom}(\sigma) \subseteq \{\vec{\gamma}\} \\
  \forall(\vec{\gamma} : C_0). T \text{ is solvable by } C \text{ and } \sigma
\end{array}
$$

$$
\frac{
  \begin{array}{l}
    C \cup C_0; \Gamma \vdash e : T \triangleright b \\
    \phantom{C \cup C_0; \Gamma \vdash e : T \triangleright b} C; \Gamma \vdash e : \forall(\vec{\gamma} : C_0). T \triangleright b
  \end{array}
}{
  \begin{array}{l}
    \{\vec{\gamma}\} \cap \mathrm{fv}(\Gamma, C, b) = \emptyset \\
    \forall(\vec{\gamma} : C_0). T \text{ is solvable by } C \text{ and some } \sigma
  \end{array}
}
$$

<caption>Fig. 3. Type-and-Effect System for ML<sub>S</sub> Expressions (omitting rule for pairs).</caption>

sources of endpoints. We thus type an extended ML<sub>S</sub> syntax

$$
\textbf{Values:} \quad v ::= \dots \mid p^l \mid \mathit{req}-c^l \mid \mathit{acc}-c^l \mid \mathit{resume}^l
$$

If a sub-expression has type $\mathit{Ses}^\rho$ and it evaluates to a value $p^l$, then it must be
that $C \vdash \rho \sim l$, denoting that $p$ was generated from the code location identified
by $l$. This location will contain one of $\mathit{req}-c^l$, $\mathit{acc}-c^l$, or $\mathit{resume}^l$. These primitive
functions (typed by $\mathit{TCONST}$) are given the following type schemas.

$$
\mathit{req}-c^l : \forall (\beta \rho \psi : \mathit{push}(l : \psi) \subseteq \beta, \rho \sim l, c \sim \psi). \mathit{Unit} \xrightarrow{\beta} \mathit{Ses}^\rho
$$

$$
\mathit{acc}-c^l : \forall (\beta \rho \psi : \mathit{push}(l : \psi) \subseteq \beta, \rho \sim l, \bar{c} \sim \psi). \mathit{Unit} \xrightarrow{\beta} \mathit{Ses}^\rho
$$

$$
\mathit{resume}^l : \forall (\beta \rho \rho' : \rho?l \subseteq \beta, \rho' \sim l). \mathit{Ses}^\rho \xrightarrow{\beta} \mathit{Ses}^{\rho'}
$$

An application of `req-c^l` starts a new session on the static endpoint `l`. To type
it, `C` must contain its effect `push(l : ψ) ⊆ β`, where `ψ` is a session variable,
representing the session type of `l`. At this level session types are ignored (hence
the use of a simple `ψ`); they become important in the second level of our typing
system. Moreover, `C` must record that session variable `ρ` is related to `l` (`ρ ∼ l`
and that the “request” endpoint of channel `c` has session type `ψ` (`c ∼ ψ`). The
only difference in the type schema of acc-c^l is that the "accept" endpoint of c is related to $\psi$ ($\bar{c} \sim \psi$). Resume receives an endpoint ($\rho'$) over another one ($\rho$), recorded in its type schema ($\rho?\rho' \subseteq \beta$); $\rho$ is an existing endpoint but $\rho'$ is treated as an endpoint generated by resume', hence the constraint $\rho' \sim l$.

The following are the type schemas of the rest of the constant functions.

$$ \text{recv} : \forall (\alpha\beta\rho : \rho?\alpha \subseteq \beta, cfd(\alpha)). \text{Ses}^{\rho} \xrightarrow{\beta} \alpha $$

$$ \text{send} : \forall (\alpha\beta\rho : \rho!\alpha \subseteq \beta, cfd(\alpha)). \text{Ses}^{\rho} \times \alpha \xrightarrow{\beta} \text{Unit} $$

$$ \text{deleg} : \forall (\beta\rho\rho' : \rho!\rho' \subseteq \beta). \text{Ses}^{\rho} \times \text{Ses}^{\rho'} \xrightarrow{\beta} \text{Unit} $$

$$ \text{sel-L} : \forall (\beta\rho : \rho?L \subseteq \beta). \text{Ses}^{\rho} \xrightarrow{\beta} \text{Unit} $$

These record input ($\rho?\alpha$), output ($\rho!\alpha$), delegation ($\rho!\rho'$), or selection ($\rho!L_i$) behaviour. For input and output the constraint $cfd(\alpha)$ must be in $C$, recording that the $\alpha$ can be instantiated only with confined types.

# 5 Second Level Typing: Session Types

Session types describe the communication protocols of endpoints; their syntax is:

$$ \eta ::= \text{end} \mid !T.\eta \mid ?T.\eta \mid !\eta.\eta \mid ?\eta.\eta \mid \bigoplus_{i \in I} \{L_i : \eta_i\} \mid \&\{L_i : \eta_i\} \mid \psi $$

A session type is finished (end) or it can describe further interactions: the input ($?T.\eta$) or output ($!T.\eta$) of a *confined* value $T$, or the delegation ($!\eta'.\eta$) or resumption ($?\eta'.\eta$) of an endpoint of session type $\eta'$, or the offering of non-deterministic selection ($\bigoplus\{L_i : \eta_i\}_{i \in I}$) of a label $L_i$, signifying that session type $\eta_i$ is to be followed next.

Moreover, a session type can offer an external choice $\&\{L_i : \eta_i\}_{i \in (I_1, I_2)}$ to its communication partner. Here $I_1$ contains the labels that the process must be able to accept and $I_2$ the labels that it may accept. We require that $I_1$ and $I_2$ are disjoint and $I_1$ is not empty. Although a single set would suffice, the two sets make type inference deterministic and independent of source code order.

We express our session typing discipline as an *abstract interpretation semantics* for behaviours shown in Fig. 4. It describes transitions of the form $\Delta \vdash b \to_C \Delta' \vdash b'$, where $b, b'$ are behaviours. The $\Delta$ and $\Delta'$ are stacks on which static endpoint labels together with their corresponding session types ($l : \eta$) can be pushed and popped. Inspired by Castagna et al. [3], in the transition $\Delta \vdash b \to_C \Delta' \vdash b'$, behaviour $b$ can only use the top label in the stack to communicate, push another label on the stack, or pop the top label provided its session type is end. This stack principle gives us a partial lock freedom property (Thm. 5.2).

Rule END from Fig. 4 simply removes a finished stack frame, and rule BETA looks up behaviour variables in $C$; PLUS chooses one of the branches of non-deterministic behaviour. The PUSH rule extends the stack by adding one more frame to it, as long as the label has not been added before on the stack (see Ex. 5.2). Rules OUT and IN reduce the top-level session type of the stack by an output and input, respectively. The requirement here is that the labels in the
<figure><img src="image_4.png" /><figcaption>Fig. 4. Abstract Interpretation Semantics.</figcaption></figure>

stack and the behaviour match, the usual subtyping [4] holds for the communi-
cated types, and that the communicated types are *confined*. Note that sending
confined (recursive) functions does not require delegation of endpoints.

Transfer of endpoints is done by delegate and resume (rules DEL and RES).
Delegate sends the second endpoint in the stack over the first; resume mimics
this by adding a new endpoint label in the second position in the stack. Resume
requires a one-frame stack to guarantee that the two endpoints of the same
session do not end up in the same stack, thus avoiding deadlock [3]. If we aban-
don the partial lock freedom property guaranteed by our type system, then the
conditions in RES can be relaxed and allow more than one frame.

A behaviour reduces an internal choice session type by selecting one of its labels (ICH). A behaviour offering an external choice is reduced non-deterministically to any of its branches (ECH). The behaviour must offer all active choices ($I_1 \subseteq J$) and all behaviour branches must be typable by the session type ($J \subseteq I_1 \cup I_2$).

As we previously explained, recursive functions in ML<sub>S</sub> must be confined.
This means that the communication effect of the function body is only on end-
points that the function opens internally, and the session type of these endpoints
is followed to completion (or delegated) before the function returns or recurs.
This is enforced in Rule REC, where rec<sub>β</sub> b must have no net effect on the stack,
guaranteed by ϵ ⊢ b ⇓<sub>C'</sub>. Here C' = (C\(rec<sub>β</sub> b ⊆ β))∪(τ ⊆ β) is the original
C with constraint (rec<sub>β</sub> b ⊆ β) replaced by (τ ⊆ β) (cf., Def. 5.1). This update
(a) `let val (p1, p2) = (req-c^1, req-d^2)`
    `val p3 = if e then p1 else p2`
    `in send p3 tt`

(b) `let fun f = req-c^l`
    `val p1 = f ()`
    `in send p1 1;`
    `let val p2 = f () in send p1 2;`

<caption>**Fig. 5.** Examples of aliasing</caption>

of *C* prevents the infinite unfolding of `rec_b β`. Spawned processes must also be confined (`SPN`). We work with *well-formed* constraints:

**Definition 5.1 (Well-Formed Constraints).** *C* is *well-formed* if:

1. Type-Consistent: for all type constructors $tc_1, tc_2$, if $(tc_1(\vec{t}_1) \subseteq tc_2(\vec{t}_2)) \in C$, then $tc_1 = tc_2$, and for all $t_{1i} \in \vec{t}_1$ and $t_{2i} \in \vec{t}_2$, $(t_{1i} \subseteq t_{2i}) \in C$.

2. Region-Consistent: if $C \vdash l \sim l'$ then $l = l'$.

3. Behaviour-Compact: behaviour constraints cycles contain $a$ (`rec_β b \subseteq \beta`) $\in C$; also if (`rec_β b \subseteq \beta'`) $\in C$ then $\beta = \beta'$ and $\forall (b' \subseteq \beta) \in C$, $b' = rec_β b$.

4. Well-Confined: if $C \vdash \text{confd}(T)$ then $T \neq \text{Ses}^\rho$; also if $C \vdash \text{confd}(b)$ then $b \notin \{\rho!T, \rho?T, \rho!\rho, \rho?\rho, \rho!L_i, \rho?L_i, \&_{i \in I} \{\rho?L_i; b_i\}\}$.

The first and fourth conditions are straightforward. The third condition disallows recursive behaviours through the environment without the use of a `rec_β b` effect. All well-typed MLs programs contain only such recursive behaviours because recursion is only possible through the use of a recursive function. The second part of the condition requires that there is at most one recursive constraint in the environment using variable `β`. This is necessary for type preservation and decidability of session typing. The second condition of Def. 5.1 requires that only endpoints from a single source can flow in each `ρ`, preventing aliasing of endpoints generated at different source locations.

**Example 5.1 (Aliasing of Different Sources).** Consider the program in Fig. 5 (a). Which endpoint flows to `p3` cannot be statically determined and therefore the program cannot yield a consistent session type for channels `c` and `d`. The program will be rejected in our framework because `p3` has type `Ses^ρ` and from the constrain environment $C \vdash \rho \sim l_1, \rho \sim l_2$, which fails Def. 5.1.

Because endpoints generated from the same source code location are identified in our system, stacks are treated *linearly*: an endpoint label `l` may only once be pushed onto a stack. Every stack `Δ` contains an implicit set of the labels `Δ.labels` to record previously pushed labels.

**Example 5.2 (Aliasing From Same Source).** Consider the program in Fig. 5 (b) where endpoint `p1` has type `Ses^ρ`, with $C \vdash \rho \sim l$. The program has behaviour `push(l : η); ρ!Int; push(l : η); ρ!Int; τ`. Label `l` is pushed on the stack twice and the behaviour complies with the session type $η = !Int.end$. However the program does not respect this session type because it sends two integers on `p1` and none on `p2`. Our system rejects this program due to the violation of stack linearity.
Our system also rejects the correct version of the program in Fig. 5 (b), where the last send is replaced by send p22. This is because the label *l* associated with the variable *ρ* of a type Ses<sup>ρ</sup> is control flow insensitive. Existing techniques can make labels control flow sensitive (e.g., [14, 15]).

Using the semantics of Fig. 4 we define the following predicate which requires behaviours to follow to completion or delegate all (*l* : *η*) frames in a stack.

**Definition 5.2 (Strong normalization).** $\Delta \vdash b \Downarrow_C \bar{\Delta}'$ when for all $b'$, $\Delta'$ such that $\Delta \vdash b \to_C^* \Delta' \vdash b' \nrightarrow_C$ we have $b' = \tau$ and $\Delta' \in \{\bar{\Delta}'\}$. We write $\Delta \vdash b \Downarrow_C$ when $\Delta \vdash b \Downarrow_C \epsilon$, where $\epsilon$ is the empty stack.

Lastly, session types on dual session endpoints ($c \sim \eta, \bar{c} \sim \eta'$) must be dual ($C \vdash \eta \bowtie \eta'$) The definition of duality is standard, with the exception that internal choice is dual to external choice only if the labels in the former are included in the *active* labels in the latter.

**Definition 5.3 (Valid Constraint Environment).** *C* is valid *if there exists* a substitution σ of variables ψ with closed session types, such that Cσ is well-formed and for all (c ~ η), (c̄ ~ η') ∈ Cσ we have C ⊢ η ⋀ η'.

Combining the Two Levels

The key property here is *well-stackedness*, the fact that in a running system where each process has a corresponding stack of endpoints, there is a way to repeatedly remove pairs of endpoints with dual session types from the top of two stacks, until all stacks are empty.

**Definition 5.4 (Well-stackedness).** $C \Vdash_{ws} S$ is the least relation satisfying:

$$ \frac{C \Vdash_{ws} S, (\Delta \vdash b, e), (\Delta' \vdash b', e') \quad C \vdash \eta \bowtie \eta' \quad p, \bar{p} \not\vdash \Delta, \Delta', S}{C \Vdash_{ws} \epsilon} $$

Note that this does not mean that programs are deterministic. Multiple pairs of endpoints may be at the top of a set of stacks. Duality of endpoints guarantees that communications are safe; the ordering of endpoints in removable pairs implies the absence of deadlocks.

We let P, Q range over tuples of the form ($\Delta \vdash b, e$) and S over sequences of such tuples. In this section stack frames ($p^l : \eta$) store both endpoints and their labels. We write $C \Vdash (\overrightarrow{\Delta \vdash b, e})$ if C is well-formed and valid, ($C; \emptyset \vdash \overrightarrow{e : T \triangleright b}$), and $(\overrightarrow{\Delta \vdash b} \Downarrow_C)$, for some $\overrightarrow{T}$. We write $C \Vdash_{ws} S$ if $\overrightarrow{\Delta}$ is well-stacked. Well-typed systems enjoy session fidelity and preserve typing and well-stackedness.

**Theorem 5.1.** Let $S = \overrightarrow{\Delta \vdash b, e}$ and $C \Vdash S$ and $C \Vdash_{ws} S$ and $\overrightarrow{e} \to \overrightarrow{e'}$; then there exist $\overrightarrow{\Delta}', \overrightarrow{b}'$ such that $S' = (\overrightarrow{\Delta' \vdash b'}, \overrightarrow{e'})$ and:

1. $C \Vdash S'$ (Type Preservation)

2. $\overrightarrow{\Delta \vdash b} \to_C^* \overrightarrow{\Delta' \vdash b'}$ (Session Fidelity)

3. $C \Vdash_{ws} S'$ (Well-Stackedness Preservation)
Session fidelity and well-stackedness preservation imply communication safety, since the former guarantees that processes are faithful to session types in the stacks, while the latter that session types are dual for each pair of open endpoints $p$ and $\bar{p}$. Moreover, well-stackedness implies deadlock freedom. $P$ depends on $Q$ if the endpoint at the top of $P$'s stack has dual endpoint in $Q$.

**Lemma 5.1 (Deadlock Freedom).** $C \Vdash_{ws} S$; dependencies in $S$ are acyclic.

Type soundness is more technical. We divide system transitions to communication transitions between processes ($\rightarrow_c$) and internal transitions ($\rightarrow_i$). Let $S \rightarrow_c S'$ ($S \rightarrow_i S'$) when $S \rightarrow S'$, derived by Rule RINIT, RCOM, RDEL or RSEL of Fig. 1 (resp., any other rule); $S \Longrightarrow_c S'$ when $S \stackrel{*}{\rightarrow}_i S'$. $\Longrightarrow_i$

**Theorem 5.2 (Type Soundness).** Let $C \Vdash S$ and $C \Vdash_{ws} S$. Then

1. $S \Longrightarrow_c S'$, or

2. $S \stackrel{*}{\rightarrow}_i (\mathcal{F}, \mathcal{D}, \mathcal{W}, \mathcal{B})$ such that:

Finished processes, $\mathcal{F}$: $\forall P \in \mathcal{F}. P = (\epsilon \Vdash \tau, v), \text{ for some } v;$

Diverging processes, $\mathcal{D}$: $\forall P \in \mathcal{D}. P \rightarrow_i^\infty$;

Waiting proc., $\mathcal{W}$: $\forall P \in \mathcal{W}. P = (\Delta \Vdash b, E[e]) \text{ and } e \in \{\text{req-c}^l, \text{acc-c}^l\}$;

Blocked processes, $\mathcal{B}$: $\forall P \in \mathcal{B}. P = (\Delta \Vdash b, E[e]) \text{ and } e \in \{\text{send } v, \text{recv } v, \text{ deleg } v, \text{ resume } v, \text{ sel-L } v, \text{ case } v \{L_i \Rightarrow e_i\}_{i \in I}\} \text{ and } P \text{ transitively depends on a process in } \mathcal{D} \cup \mathcal{W}.$

A well-typed and well-stacked ML$_S$ system will either be able to perform a communication, or, after finite internal steps, it will reach a state where some processes are values ($\mathcal{F}$), some internally diverge ($\mathcal{D}$), some are waiting for a partner process to open a session ($\mathcal{W}$), and some are blocked on a session communication ($\mathcal{B}$). Crucially, in states where communication is not possible, $\mathcal{B}$ transitively depends on $\mathcal{D} \cup \mathcal{W}$. Thus, in the absence of divergence and in the presence of enough processes to start new sessions, no processes can be blocked; the system will either perform a communication or it will terminate (partial lock freedom).

**Corollary 5.1 (Partial Lock Freedom).** If $C \Vdash S$, $C \Vdash_{ws} S$, and $S \Longrightarrow_c$ and $S \stackrel{*}{\rightarrow}_i (\mathcal{F}, \emptyset, \emptyset, \mathcal{B})$ then $\mathcal{B} = \emptyset$.

# 6 Inference Algorithm

We use three inference algorithms, $\mathcal{W}$, $\mathcal{SI}$ and $\mathcal{D}$. The first infers functional types and communication effects and corresponds to the first level of our type system. The other two infer session types from the abstract interpretation rules of Fig. 4 ($\mathcal{SI}$) and the duality requirement of Def. 5.3 ($\mathcal{D}$), corresponding to the second level of the type system.

Algorithm $\mathcal{W}$ is a straightforward adaptation of the homonymous algorithm from [1]: given an expression $e$, $\mathcal{W}$ calculates its type $t$, behaviour $b$ and constraints set $C$; no session information is calculated. $\mathcal{W}$ generates pairs of fresh constraints $c \sim \psi$ and $\bar{c} \sim \psi'$ for each global channel $c$ in the source program; $\psi$ and $\psi'$ are unique. Results of $\mathcal{W}$'s soundness and completeness follow from [1].
For all constraints $(c \sim \psi) \in C$, Algorithm *SI* infers a substitution $\sigma$ and a refined set $C'$ such that $\epsilon \models b\sigma \Downarrow_{C'} \epsilon$. The substitution only maps $\psi$ variables to session types. The final $C'$ is derived from $C$ by applying $\sigma$ and possibly adding more type constraints of the form $(T \subseteq T')$. The core of this algorithm is the abstract interpreter $MC$, which explores all possible transitions from $\epsilon \models b$.

Algorithm $MC$ is designed in a continuation-passing style, using a continuation stack $K ::= \epsilon \mid b \cdot K$.

As transition paths are explored, previously discovered branches of internal and external choices in session types may need to be expanded. For example, if Algorithm $MC$ encounters a configuration $(l : \bigoplus \{L_i : \eta_i\}_{i \in I}) \models l!L_j$ where $j \notin I$, the inference algorithm needs to add the newly discovered label $L_j$ to the internal choice on the stack.

To do this, internal and external choices are removed from the syntax of sessions, and replaced with special variables $\psi_{in}$ and $\psi_{ex}$. These variables are bound by unique choice constraints, extending the syntax of constraints (Fig. 2):

$$C ::= \dots \mid \bigoplus \{L_i : \eta_i\}_{i \in I} \sim \psi_{in} \mid \& \{L_i : \eta_i\}_{i \in (I_1, I_2)} \sim \psi_{ex}$$

$MC$ updates $\psi_{in}$ and $\psi_{ex}$ constraints in $C$ with newly discovered branches. For example it may add new labels to an internal choice, or move active labels to inactive in an external choice.

We now give more detail for some inference steps of Algorithm $MC$. The full algorithm can be found in an online technical report<fnref n="1" />. Algorithm $MC$ terminates successfully when all sessions on the stack have terminated, the input behaviour is $\tau$ and the continuation stack is empty:

$$MC(\Delta \models \tau, C, \epsilon) = (\sigma, C\sigma) \quad \text{if } \sigma = \text{finalize } \Delta$$

When this clause succeeds, $\Delta$ may be empty or it may contain frames of the form $(l : \psi)$ or $(l : \text{end})$. The helper function finalise $\Delta$ returns a substitution $\sigma$ that maps all such $\psi$'s to end. If this is not possible (i.e., a session on $\Delta$ is not finished) finalise raises an error.

New frames are pushed on the stack when the behaviour is `push(l : \eta)`:

$$MC(\Delta \models \text{push}(l : \eta), C, K) = (\sigma_2\sigma_1, C_2) \quad \text{if } (\sigma_1, \Delta_1) = \text{checkFresh}(l, \Delta) \quad \text{and } (\sigma_2, C_2) = MC((l : \eta\sigma_1) \cdot \Delta_1 \models \tau, C\sigma_1, K\sigma_1)$$

where `checkFresh` checks that $l$ has never been in $\Delta$.

When the behaviour is an operation that pops a session from the stack, such as a `send(l!T)`, $MC$ looks up the top frame on the stack, according to the stack principle. There are two cases to consider: either the top frame contains a fresh variable $\psi$, or some type has been already inferred. The algorithm here is:

<footnote n="1">¹ Spaccasassi, C., Koutavas, V.: Type-Based Analysis for Session Inference. ArXiv e-prints (Oct 2015), http://arxiv.org/abs/1510.03929v3.</footnote>
$$MC((l: \psi) \cdot \Delta \models \rho!T, C, K) = (\sigma_2 \sigma_1, C_2)$$

if $C \vdash l \sim \rho$

and $\sigma_1 = [\psi \mapsto !\alpha.\psi']$ where $\alpha, \psi'$ fresh

and $(\sigma_2, C_2) = MC((l: \psi') \cdot \Delta \sigma_1 \models \tau, C \sigma_1 \cup \{T \subseteq \alpha\}, K \sigma_1)$

$$MC((l: !\alpha.\eta) \cdot \Delta \models \rho!T, C, K) = MC((l: \eta) \cdot \Delta \models \tau, C \cup \{T \subseteq \alpha\}, K)$$

if $C \vdash l \sim \rho$

In the first case, $MC$ checks that $\rho$ in the behaviour corresponds to $l$ at the top of the stack. It then produces the substitution $[\psi \mapsto !\alpha.\psi']$, where $\alpha$ and $\psi'$ are fresh, and adds $(T \subseteq \alpha)$ to $C$. The second case produces no substitution.

The clauses for delegation are similar:

$$MC((l: \psi) \cdot (l_d : \eta_d) \cdot \Delta \models \rho! \rho_d, C, K) = (\sigma_2 \sigma_1, C_2)$$

if $C \vdash l \sim \rho$ and $C \vdash l_d \sim \rho_d$

and $\sigma_1 = [\psi \mapsto !\eta_d.\psi']$ where $\psi'$ fresh

and $(\sigma_2, C_2) = MC((l: \psi') \cdot \Delta \sigma \models \tau, C \sigma_1, K \sigma_1)$

$$MC((l: !\eta_d.\eta) \cdot (l_d : \eta'_d) \cdot \Delta \models \rho! \rho_d, C, K) = (\sigma_2 \sigma_1, C_2)$$

if $C \vdash l \sim \rho$ and $C \vdash l_d \sim \rho_d$

and $(\sigma_1, C_1) = \text{sub}(\eta'_d, \eta_d, C)$

and $(\sigma_2, C_2) = MC((l: \eta) \cdot \Delta \sigma \models \tau, C_1, K \sigma_1)$

The main difference here is that, in the second clause, the sub function checks that $C \vdash \eta'_d <: \eta_d$ and performs relevant inference. Moreover, the input $\Delta$ must contain at least two frames (the frame below the top one is delegated).

The cases for receive, label selection and offer, and resume are similar (see online report). In the cases for label selection and offering, the algorithm updates the $\psi_{in}$ and $\psi_{ex}$ variables, as discussed above. In the case of resume, the algorithm checks that the stack contains one frame.

In behaviour sequencing and branching, substitutions are applied eagerly and composed iteratively, and new constraints are accumulated in $C$:

$$MC(\Delta \models b_1; b_2, C, K) = MC(\Delta \models b_1, C, b_2 \cdot K)$$

$$MC(\Delta \models b_1 \oplus b_2, C, K) = (\sigma_2 \sigma_1, C_2)$$

if $(\sigma_1, C_1) = MC(\Delta \models b_1, C, K)$

and $(\sigma_2, C_2) = MC(\Delta \sigma_1 \models b_2 \sigma_1, C_1, K \sigma_1)$

When a recursive behaviour $\text{rec}_b \beta$ is encountered, Algorithm $MC$ needs to properly setup the input constraints $C$ according to Rule REC of Fig. 4:

$$MC(\Delta \models \text{rec}_b b, C) = (\sigma_2 \sigma_1, C_2)$$

if $C = C' \uplus \{b' \subseteq \beta\}$

and $(\sigma_1, C_1) = MC(\epsilon \models b, C' \cup \{\tau \subseteq \beta\}, \epsilon)$

and $(\sigma_2, C_2) = MC(\Delta \sigma_1 \models \tau, (C_1 \setminus \{\tau \subseteq \beta\}) \cup (\{b' \subseteq \beta\}) \sigma_1, K \sigma_1)$

Here the algorithm first calls $MC$ on $\epsilon \models b$, checking that the recursion body $b$ is self-contained under $C'$, in which the recursion variable $\beta$ is bound to $\tau$. This update of $C$ prevents the infinite unfolding of $\text{rec}_b \beta$. It then restores back the constraint on $\beta$, applies the substitution $\sigma_1$, and continues inference.
The clause for spawn b is similar, except that C is unchanged. Variables $\beta$ are treated as the internal choice of all behaviours $b_i$ bound to $\beta$ in C:

$$MC(\Delta \models \beta, C, K) = MC(\Delta \models b, C, K) \\ \text{where } b = \bigoplus\{b_i \mid \exists i. (b_i \subseteq \beta) \in C\}$$

Inference fails when $MC$ reaches a stuck configuration $\Delta \models b$ other than $\epsilon \models \tau$, corresponding to an error in the session type discipline.

To prove termination of $SI$, we first define the translation $[[b]]_C^g$, that replaces $\beta$ variables in $b$ with the internal choice $\bigoplus\{b_i \mid (b_i \subseteq \beta) \in C\}$. Due to behaviour-compactness (Def. 5.1), $[[b]]_C^g$ is a finite ground term, i.e. a finite term without $\beta$ variables. Except for Rule BETA, transitions in Fig. 4 never expand $b$; they either consume $\Delta$ or $b$. Since $[[b]]_C^g$ is finite when $C$ is well-formed, $\epsilon \models [[b]]_C^g$ generates a finite state space and Algorithm $MC$ always terminates.

Similar to ML type inference, the worst-case complexity of $MC$ is exponential to program size: $MC$ runs in time linear to the size of $[[b]]_C^g$, which in the worst case is exponentially larger than $b$, which is linear to program size. The worst case appears in pathological programs where, e.g., each function calls all previously defined functions. We intend to explore whether this is an issue in practice, especially with an optimised dynamic programming implementation of $MC$.

Soundness and completeness of $SI$ follow from the these properties of $MC$.

**Lemma 6.1 (Soundness of MC).** Let $C$ be well-formed and $MC(\Delta \models b, C) = (\sigma_1, C_1)$; then $\Delta\sigma_1 = \Delta'$ and $\Delta' \models b\sigma_1 \Downarrow_{C_1}$.

**Lemma 6.2 (Completeness of MC).** Let $C$ be well-formed and $(\Delta \models b)\sigma \Downarrow_C$; then $MC(\Delta \models b, C_0) = (\sigma_1, C_1)$ and $\exists\sigma'$ such that $C \vdash C_1\sigma'$ and $\forall\psi \in \text{dom}(\sigma)$, $C \vdash \sigma(\psi) <: \sigma'(\sigma_1(\psi))$.

Completeness states that $MC$ computes the most general constraints $C_1$ and substitution $\sigma_1$, because, for any $C$ and $\sigma$ such that $(\Delta \models b)\sigma$ type checks, $C$ specialises $C_1$ and $\sigma$ is an instance of $\sigma_1$, after some extra substitution $\sigma'$ of variables (immaterial for type checking).

Algorithm $\mathcal{D}$ collects all $c \sim \eta_1$ and $\bar{c} \sim \eta_2$ constraints in $C'$, generates duality constraints $\eta_1 \bowtie \eta_2$ and iteratively checks them, possibly substituting $\psi$ variables. It ultimately returns a $C''$ which is a valid type solution according to Def. 5.3. Soundness and completeness of Algorithm $\mathcal{D}$ is straightforward.

We now show how $SI$ infers the correct session types for Ex. 2.1 from Sect. 2. We assume that Algorithm $\mathcal{W}$ has already produced a behaviour $b$ and constraints $C$ for this example. For clarity, we simplify $b$ and $C$: we remove spurious $\tau$s from behaviour sequences, replace region variables $\rho$ with labels (only one label flows to each $\rho$), and perform simple substitutions of $\beta$ variables.

**Example 6.1 (A Swap Service).**

There are three textual sources of endpoints in this example: the two occurrences of acc-swp in coord, and req-swp in swap. A pre-processing step automatically annotates them with three unique labels $l_1, l_2$ and $l_3$. Algorithm $\mathcal{W}$ infers $b$ and $C$ for Ex. 2.1; the behaviour $b$ (simplified) is:

spawn ($\beta_{coord}$); spawn ($\beta_{swap}$); spawn ($\beta_{swap}$)
In this behaviour three processes are spawned: one with a $\beta_{coord}$ behaviour, and two with a $\beta_{swap}$ behaviour. The behaviour associated to each of these variables is described in C, along with other constraints:

1. $\text{rec}_{\beta_{coord}}(\text{push}(l_1 : \psi_1); l_1?\alpha_1; \text{push}(l_2 : \psi_1); l_2?\alpha_2; l_2!\alpha_1; l_1!\alpha_2); \beta_{coord} \subseteq \beta_{coord}$

2. $\text{push}(l_3 : \psi_2); l_3!\text{Int}; l_3?\alpha_3 \subseteq \beta_{swap}$

3. $\overline{\text{swap}} \sim \psi_1$

4. $\text{swap} \sim \psi_2$

The above behaviour and environment are the inputs to Algorithm SI, implementing session type inference according to the second level of our framework. The invocation $\mathcal{SI}(b, C)$ calls $\mathcal{MC}(\epsilon \models b, C, \epsilon)$, where the first $\epsilon$ is the empty endpoint stack $\Delta$ and the second $\epsilon$ is the empty continuation stack. Behaviour $b$ is decomposed as $b = K[b']$, where $b' = \text{spawn}(\beta_{coord})$ and $K$ is the continuation $[ ]$; $\text{spawn}(\beta_{swap})$; $\text{spawn}(\beta_{swap})$. The algorithm thus calls $\mathcal{MC}(\epsilon \models \text{spawn}(\beta_{coord}), C, K)$, which, after replacing $\beta_{coord}$ and unfolding its inner recursive behaviour becomes:

$$ \mathcal{MC}(\epsilon \models \text{push}(l_1 : \psi_1); l_1?\alpha_1; \text{push}(l_2 : \psi_1); l_2?\alpha_2; l_2!\alpha_1; l_1!\alpha_2; \beta_{coord}, C_1, \epsilon) $$

Here $C_1$ is equal to $C$ above, with the exception of replacing Constraint 1 with the constraint $(\tau \subseteq \beta_{coord})$. Inference is now straightforward: the frame $(l_1 : \psi_1)$ is first pushed on the endpoint stack. From behaviour $l_1?\alpha_1$ the algorithm applies substitution $[\psi_1 \mapsto ?\alpha_4.\psi_4]$, where $\psi_4$ and $\alpha_4$ are fresh, and generates constraint $(\alpha_4 \subseteq \alpha_1)$ obtaining $C_2$. We thus get:

$$ \mathcal{MC}((l_1 : \psi_4) \models \text{push}(l_2: ?\alpha_4.\psi_4); l_2?\alpha_2; l_2!\alpha_1; l_1!\alpha_2; \beta_{coord}, C_2, \epsilon) $$

After the next push, the endpoint stack becomes $(l_2 : ?\alpha_4.\psi_4) \cdot (l_1 : \psi_4)$. The next behaviour $l_2?\alpha_2$ causes $\mathcal{MC}$ to create constraint $(\alpha_4 \subseteq \alpha_2)$ obtaining $C_3$, and to consume session $?\alpha_4$ from the top frame of the endpoint stack.

$$ \mathcal{MC}((l_2 : \psi_4) \cdot (l_1 : \psi_4) \models l_2!\alpha_1; l_1!\alpha_2; \beta_{coord}, C_3, \epsilon) $$

Because of $l_2!\alpha_1$, $\mathcal{MC}$ generates $[\psi_3 \mapsto !\alpha_5.\psi_5]$ and $(\alpha_1 \subseteq \alpha_5)$ obtaining $C_4$.

$$ \mathcal{MC}((l_2 : \psi_5) \cdot (l_1 : !\alpha_5.\psi_5) \models l_1!\alpha_2; \beta_{coord}, C_4, \epsilon) $$

Since $l_1$ in the behaviour and $l_2$ at the top of the endpoint stack do not match, $\mathcal{MC}$ infers that $\psi_5$ must be the terminated session end. Therefore it substitutes $[\psi_5 \mapsto \text{end}]$ obtaining $C_5$. Because of the substitutions, $C_5$ contains $\overline{\text{swap}} \sim ?\alpha_4. !\alpha_5. \text{end}$. After analysing $\beta_{swap}$, $\mathcal{MC}$ produces $C_6$ where $\overline{\text{swap}} \sim !\text{Int}. !\alpha_6. \text{end}$.

During the above execution $\mathcal{MC}$ verifies that the stack principle is respected and no endpoint label is pushed on the stack twice. Finally the algorithm calls $\mathcal{D}(C_6)$ which performs a duality check between the constraints of $\overline{\text{swap}}$ and $\text{swap}$, inferring substitution $[\alpha_4 \mapsto \text{Int}, \alpha_6 \mapsto \alpha_5]$. The accumulated constraints on type variables $\alpha$ give the resulting session types of the swap channel endpoints: $(\overline{\text{swap}} \sim ?\text{Int}. !\text{Int}. \text{end})$ and $(\text{swap} \sim !\text{Int}. ?\text{Int}. \text{end})$.
# 7 A Proposal for Recursive Session Types

The system we have presented does not include recursive session types. Here we propose an extension to the type system with recursive types. The inference algorithm for this extension is non-trivial and we leave it to future work.

In this extension, a recursive behaviour may partially use a recursive session type and rely on the continuation behaviour to fully consume it. First we add *protected* recursive session types: $\eta ::= ... | \mu X.\eta | X$. The first level of our type system remains unchanged, as it is parametric to session types, and already contains recursive functions and behaviours.

A recursive behaviour $\mathbf{rec}_\beta b$ operating on an endpoint $l$ with session type $\mu X.\eta$ may: (a) run in an infinite loop, always unfolding the session type; (b) terminate leaving $l$ at type end; (c) terminate leaving $l$ at type $\mu X.\eta$. Behaviour $b$ may have multiple execution paths, some terminating, ending at $\tau$, and some recursive, ending at a recursive call $\beta$. They all need to leave $l$ at the same type, either end or $\mu X.\eta$; the terminating paths of $b$ determine which of the two session types $l$ will have after $\mathbf{rec}_\beta b$. If $b$ contains no terminating paths then we assume that $l$ is fully consumed by $\mathbf{rec}_\beta b$ and type the continuation with $l$ at end.

To achieve this, we add a *stack environment* $D$ in the rules of Fig. 4, which maps labels $l$ to stacks $\Delta$. If $\Delta_1 = (l : \mu X.\eta)$, we call an $l$-path from $\Delta_1 \models b_1$ any finite sequence of transitions such that $\Delta_1 \models b_1 \to_{C,D} \dots \to_{C,D} \Delta_n \models b_n \to_{C,D} \dots$. A $l$-path is called $l$-finitary if there is no $b_i = \tau^l$ for any configuration $i$ in the series; otherwise we say that the path is $l$-recursive. We write $(l : \mu X.\eta) \models b \Downarrow_{C,D}^{\mathbf{fin}} \Delta'$ when the last configuration of all $l$-finitary paths from $(l : \mu X.\eta) \models b$ is $\Delta' \models \tau$. Similarly, we write $(l : \mu X.\eta) \models b \Downarrow_{C,D}^{\mathbf{rec}} \Delta'$ when the last configuration of all $l$-recursive paths from $(l : \mu X.\eta) \models b$ is $\Delta' \models \tau^l$. When no $l$-paths from $(l : \mu X.\eta) \models b$ is $l$-finitary, we stipulate $(l : \mu X.\eta) \models b \Downarrow_{C,D}^{\mathbf{fin}} (l : \text{end})$ holds. We add the following rules to those of Fig. 4.

$$ \begin{array}{l@{\qquad}l} \textbf{REC2} & \frac{ \begin{array}{l} (l : \mu X.\eta) \models b \Downarrow_{C',D'}^{\mathbf{fin}} \Delta' \\ (l : \mu X.\eta) \models b \Downarrow_{C',D'}^{\mathbf{rec}} \Delta' \end{array} }{ (l : \mu X.\eta) \cdot \Delta \models \mathbf{rec}_\beta b \to_{C,D} \Delta' \cdot \Delta \models b' } & \begin{array}{l} \Delta' \in \{(l : \text{end}), (l : \mu X.\eta)\} \\ C' = (C \setminus (\mathbf{rec}_\beta b \subseteq \beta)) \cup (\tau^l \subseteq \beta) \\ D' = D[l \mapsto \Delta'] \end{array} \end{array} $$

$$ \begin{array}{l@{\qquad}l} \textbf{RCALL} & \frac{ \begin{array}{l} (l : \eta[X \mapsto \mu X.\eta]) \cdot \Delta \models b \to_{C,D} \Delta' \models b' \end{array} }{ (l : \mu X.\eta) \models \tau^l \to_{C,D} D(l) \models \tau } \\ \textbf{UNF} & \frac{ \begin{array}{l} (l : \mu X.\eta) \cdot \Delta \models b \to_{C,D} \Delta' \models b' \end{array} }{ (l : \mu X.\eta) \models b \to_{C,D} \Delta' \models b' } \end{array} $$

Rule REC2 requires that both $l$-finitary and $l$-recursive paths converge to the same stack $\Delta'$, either $(l : \text{end})$ or $(l : \mu X.\eta)$. In this rule, similarly to rule REC in Fig. 4, we replace the recursive constraint $(\mathbf{rec}_\beta b \subseteq \beta)$ with $(\tau^l \subseteq \beta)$, representing a trivial recursive call of $\beta$. This guarantees that all $l$-paths have a finite number of states. The $D$ environment is extended with $l \mapsto \Delta'$, used in Rule RCALL to obtain the session type of $l$ after a recursive call. Rule UNF simply unfolds a recursive session type.
# 8 Related Work and Conclusions

We presented a new approach for adding binary session types to high-level programming languages, and applied it to a core of ML with session communication. In the extended language our system checks the session protocols of interesting programs, including one where pure code calls library code with communication effects, without having to refactor the pure code (Ex. 2.3). Type soundness guarantees partial lock freedom, session fidelity and communication safety.

Our approach is modular, organised in two levels, the first focusing on the type system of the source language and second on typing sessions; the two levels communicate through *effects*. In the first level we adapted and extended the work of Amtoft, Nielson and Nielson [1] to session communication, and used it to extract the communication effect of programs. In the second level we developed a session typing discipline inspired by Castagna et al. [3]. This modular approach achieves a provably complete session inference for finite sessions without programmer annotations.

Another approach to checking session types in high-level languages is to use substructural type systems. For example, Vasconcelos et al. [18] develop such a system for a functional language with threads, and Wadler [19] presents a linear functional language with effects. Type soundness in the former guarantees session fidelity and communication safety, and in the latter also lock freedom and strong normalisation. Our system is in between these two extremes: lock freedom is guaranteed only when processes do not diverge and their requests for new sessions are met. Other systems give similar guarantees (e.g., [3, 16]).

Toninho et al. [16] add session-typed communication to a functional language using a monad. Monads, similar to effects, cleanly separate session communication from the rest of the language features which, unlike effects, require parts of the program to be written in a monadic style. Pucella and Tov [13] use an indexed monad to embed session types in Haskell, however with limited endpoint delegation: delegation relies on moving capabilities, which cannot escape their static scope. Our Ex. 2.2 is not typable in that system because of this. In [13] session types are inferred by Haskell's type inference. However, the programmer must guide inference with expressions solely used to manipulate type structures.

Tov [17] has shown that session types can be encoded in a language with a general-purpose substructural type system. Type inference alleviates the need for typing annotations in the examples considered. Completeness of session inference relies on completeness of inference in the general language, which is not clear.

Igarashi et al. [9] propose a reconstruction algorithm for finite types in the linear π calculus. Inference is complete and requires no annotations. Padovani [11] extends this work to pairs, disjoint sums and regular recursive types.

Mezzina [10] gives an inference algorithm for session types in a calculus of services. The type system does not support recursive session types and endpoint delegation. It does allow, however, to type replicated processes that only use finite session types, similar to our approach.
Bibliography

[1] Amtoft, T., Nielson, H.R., Nielson, F.: Type and effect systems - behaviours for concurrency. Imperial College Press (1999)

[2] Caires, L., Pfenning, F.: Session types as intuitionistic linear propositions. In: Gastin, P., Laroussinie, F. (eds.) CONCUR, LNCS, vol. 6269, pp. 222–236. Springer (2010)

[3] Castagna, G., Dezani-Ciancaglini, M., Giachino, E., Padovani, L.: Foundations of session types. In: PPDP. pp. 219–230. ACM (2009)

[4] Gay, S., Hole, M.: Subtyping for session types in the pi calculus. Acta Informatica 42(2-3), 191–225 (2005)

[5] Gay, S., Vasconcelos, V.: Linear type theory for asynchronous session types. Journal of Functional Programming 20(01), 19–50 (Jan 2010)

[6] Honda, K.: Types for dyadic interaction. In: Best, E. (ed.) CONCUR, LNCS, vol. 715, pp. 509–523. Springer (1993)

[7] Honda, K., Vasconcelos, V.T., Kubo, M.: Language primitives and type discipline for structured communication-based programming. In: Hankin, C. (ed.) PLS (ESOP), LNCS, vol. 1381, pp. 122–138. Springer (1998)

[8] Hüttel, H., Lanese, I., Vasconcelos, V., Caires, L., Carbone, M., Deniélou, P., Padovani, L., Ravara, A., Tuosto, E., Vieira, H., Zavattaro, G.: Foundations of session types and behavioural contracts. ACM Comp. Surv. To appear

[9] Igarashi, A., Kobayashi, N.: Type reconstruction for linear π-calculus with I/O subtyping. Inf. Comput. 161(1), 1–44 (2000)

[10] Mezzina, L.G.: How to infer finite session types in a calculus of services and sessions. In: Lea, D., Zavattaro, G. (eds.) Coordination Models and Languages, LNCS, vol. 5052, pp. 216–231. Springer (2008)

[11] Padovani, L.: Type reconstruction for the linear π-calculus with composite regular types. Logical Methods in Computer Science 11(4) (2015)

[12] Palsberg, J.: Type-based analysis and applications. In: PASTE. pp. 20–27. ACM (2001)

[13] Pucella, R., Tov, J.A.: Haskell session types with (almost) no class. In: Haskell Symposium. pp. 25–36. ACM (2008)

[14] Shivers, O.: Control-flow analysis of higher-order languages. Ph.D. thesis, CMU (1991)

[15] Tofte, M., Talpin, J.: Implementation of the typed call-by-value lambda-calculus using a stack of regions. In: POPL. pp. 188–201. ACM (1994)

[16] Toninho, B., Caires, L., Pfenning, F.: Higher-order processes, functions, and sessions: A monadic integration. In: Felleisen, M., Gardner, P. (eds.) PLS (ESOP), LNCS, vol. 7792, pp. 350–369. Springer (2013)

[17] Tov, J.: Practical Programming with Substructural Types. Ph.D. thesis, Northeastern University (2012)

[18] Vasconcelos, V., Gay, S., Ravara, A.: Type checking a multithreaded functional language with session types. Th. Computer Sc. 368(1-2), 64–87 (2006)

[19] Wadler, P.: Propositions as sessions. In: ICFP. pp. 273–286. ACM (2012)