Multiparty Session Types for Safe Runtime Adaptation in an Actor Language
(Extended version)
Multiparty Session Types for Safe Runtime Adaptation in an Actor Language

Human fallibility, unpredictable operating environments, and
the heterogeneity of hardware devices
are driving the need for software to be able to adapt
as seen in the Internet of Things or telecommunication networks.
Unfortunately, mainstream programming languages do not readily allow a software
component to sense and respond to its operating environment, by
discovering, replacing, and communicating with
components that are not part of the original system design, while
maintaining static correctness guarantees.  In particular, if a new component is
discovered at runtime, there is no guarantee that its communication
behaviour is compatible with existing components.

We address this problem by using multiparty session types with explicit
connection actions, a type formalism used to model distributed communication
protocols. By associating session types with software components, the discovery
process can check protocol compatibility and, when required, correctly replace
components without jeapordising safety.

We present the design and implementation of , the first
actor-based language with adaptive features and a static session type system,
and apply it to a case study based on an adaptive DNS server. We formalise the
type system of and prove the safety of well-typed programs, making
essential use of recent advances in non-classical multiparty session

§ INTRODUCTION

The era of single monolithic stand-alone computers has long been replaced by a
landscape of heterogeneous and distributed computers and software applications.
Technologies such as the
IoT [Xia et al., 2012], self-driving cars [Visintainer et al., 2013], or autonomous networks [Bouabene et al., 2010] bring the new challenge of needing to successfully operate in face of ever-changing environments, technologies, devices, and human errors, necessitating the need to adapt.

Here, we define dynamic self-adaptation—hereafter referred to as adaptation—as the ability of a software component to sense and respond to its operating environment, by discovering, replacing, and communicating with other software components at runtime that are not part of the original system design [Baumann et al., 1999, Rellermeyer et al., 2007].
There are many examples of adaptive systems, as well as the mechanisms of
adaptation they leverage, such as discovery [Jara et al., 2012],
modularisation [Hayton et al., 1999], dynamic code loading and
migration [Cesarini and Vinoski, 2016, Gu et al., 2004]. Commercially, Steam's in-home
streaming system[<http://store.steampowered.com/streaming/>]
enables video games to dynamically transfer their input/output across a range of
devices. Academically, RE$^\mathrm{X}$ [Porter et al., 2016] enables software to
self-assemble predefined components, using machine learning to reconfigure the
software in response to environmental changes.

Despite strong interest in adaption and substantial work on the mechanisms of
adaptation, current programming languages either lack the capabilities to ensure
that adaptation can be achieved safely and correctly, or they check correctness
dynamically, resulting in runtime overheads which may not be acceptable for
resource-constrained devices.

Specifically, if an adaptive system discovers new software components at
these components must interact with the system in a purposeful manner. In
concurrent and distributed systems, such interaction goes beyond a simple
function call / return expressed with standard types and type systems:
interaction involves complex communication protocols that constrain the
sequence and type of data exchanged. For example, knowing that two components
communicate integers and strings does not describe if or when they will be sent
or received.
In spite of growing interest in the topic, for example, the recent formation of the United
Nations group considering creative
mainstream programming languages do not support the
specification and verification of communication protocols in
concurrent and distributed systems. In turn, errors are discovered late in the
development process and potentially after deployment.

Even where all components are known statically, communication safety cannot be
guaranteed: as an example, the RE$^\mathrm{X}$ system's programming language specifies
sequential call / return interfaces for components, but not communication
protocols for concurrent components.
The adaptation in the Steam in-home streaming system is even more limited, being restricted to detection of input/output devices from a set of compatible possibilities. In both cases, the adaptive aspects of the software have been defined and designed ahead of time, as opposed to being composed on-demand at runtime, leaving no scope for extending the system via runtime discovery and replacement.

This situation brings us to a key research question:

Can a programming language support static (compile-time) verification of safe runtime dynamic self-adaptation, i.e., discovery, replacement and communication?

The problem of static verification of safe communication is addressed by multiparty session types [Honda, 1993, Honda et al., 1998, Honda et al., 2008].
Multiparty session types (MPSTs) are a type formalism used to specify the
type, direction and sequence of communication actions
between two or more participants. Session types guarantee that software conforms
to predefined communication protocols, rather than risking errors manifesting
themselves at runtime.

There is already some work in the literature on adaptation and session types,
but it does not answer our research question. We discuss related work in
<ref>, but in brief, the state-of-the-art has some combination of
the following limitations: theory for a formal model such as the $\pi$-calculus
[Coppo et al., 2015, Castellani et al., 2016, Di Giusto and Pérez, 2015, Di Giusto and Pérez, 2015], rather than a
real-world programming language; omission of some aspects of adaptation, such as
runtime discovery [Hu and Yoshida, 2017]; or verification by runtime monitoring
[Neykova and Yoshida, 2014, Neykova and Yoshida, 2017, Fowler, 2016], as opposed to static checking.

To answer our research question,
we implement , the first actor language leveraging MPSTs
to provide compile-time verification of safe dynamic runtime adaptation:
we can statically guarantee that a discovered actor will comply
with a communication protocol, and guarantee that replacing an actor's behaviour
(e.g., to fix a bug) will not jeapordise communication safety.
Key to our approach is the combination of the actor
paradigm [Hewitt et al., 1973], for its process addressability
and explicit message passing, with explicit connection
actions [Hu and Yoshida, 2017] in multiparty session types, which allow discovered
actors to be invited into a session.

The overarching contribution of this work is the design, implementation, and
formalisation of a language which supports dynamic self-adaptation while
guaranteeing communication safety. We achieve this through a novel integration
of an actor-based language and multiparty session types with explicit connection
actions. Specifically, we introduce:

* and its compiler (<ref>): we
present an actor language, , which supports safe adaptable
applications using MPSTs. Our framework supports:

* MPST specifications, both standard and using explicit
connection actions (<ref>);

* MPSTs to provide guarantees of protocol compliance in runtime discovery (<ref>);

* automatic generation of application code from MPSTs (<ref>)

* An adaptive DNS case study (<ref>): using MPSTs and runtime discovery to show safe dynamic self-adaptation can be achieved in a non-trivial software service

* A core calculus for  (<ref>): we
formalise and prove type safety and progress.

The formalism makes several technical contributions: it is the first
actor-based calculus with statically-checked MPSTs; and it is the first
calculus to provide a language design and semantics for explicit
connection actions, which had previously only been explored at the type level.
Our design requires exception handling in the style of Mostrous and Vasconcelos, 2018
and Fowler et al., 2019, and the metatheory makes essential (and novel) use
of non-classical multiparty session types [Scalas and Yoshida, 2019].

The implementation and examples are available in the paper's companion artifact.

Global protocol

[basicstyle=, numbers=left, language = ensemble]
global protocol Bookstore
(role Sell, role Buy1, role Buy2)
book(string) from Buy1 to Sell;
book(int) from Sell to Buy1;
quote(int) from Buy1 to Buy2;
choice at Buy2
agree(string) from Buy2 to Buy1, Sell;
transfer(int) from Buy1 to Sell;
transfer(int) from Buy2 to Sell;
quit(string) from Buy2 to Buy1, Sell;

Local protocol for +Sell+

[language = ensemble, label=lst:scribble-buy1]
local protocol Bookstore_Sell
(self Sell,role Buy1,role Buy2)
book(string) from Buy1;
book(int) to Buy1;
choice at Buy2
agree(string) from Buy2;
transfer(int) from Buy1;
transfer(int) from Buy2;
quit(string) from Buy2;

Global and local protocols for Bookstore

§ MULTIPARTY SESSION TYPES

Multiparty session types [Honda et al., 2008] are a type
formalism used to describe communication protocols in
concurrent and distributed systems.  An MPST describes communication among
multiple software components or participants, by specifying the type and
the direction of data exchanged, which is given as a sequence of send and
receive actions.

We first introduce MPSTs (formalised in <ref>) via
Scribble [Yoshida et al., 2014], a specification
language for communicating protocols based on the theory of
multiparty session types.  We start with a global type, which describes
the interactions among all communicating participants.  Using the Scribble tool,
a global protocol can be validated, guaranteeing its correctness, and
then projected for each participant. Projection returns a local
type, which describes communication actions from the viewpoint of that

<ref> shows the classic  (also known
as Two-Buyer) example, written in Scribble.
We have three communicating
participants (roles): two buyers  and , and one seller
, where the buyers wish to buy a book from the seller.
sends the title of the book of type
string to  (line 3).
Next,  sends the price of the book of type
int to  (line 4).  At this stage,
invites  to share the cost of the
book, by sending them a  of type int that
should pay (line 5). It is 's internal choice
(line 6) to either  (line 7), or  the protocol (line
11). After agreement, both  and
their  to  (lines 8 and 9, respectively).

Projecting the  global protocol into each of the communicating
participants returns their local protocols. <ref> shows the
local protocol for ; we omit  and  as
they are similar.  Note that the local protocol only includes actions relevant
to .

Explicit connection actions.

The  protocol assumes that all roles are connected at the
start of the session. This is undesirable when a participant is only needed for
part of a session, or the identity of a participant depends on data
exchanged in the protocol.

[basicstyle=, numbers=left, language = ensemble]
explicit global protocol OnlineStore
(role Customer, role Store, role Courier)
login(string) connect Customer to Store;
do Browse(Customer, Store, Courier);

aux global protocol Deliver
(role Customer, role Store, role Courier)
address(string) from Customer to Store;
deliver(string) connect Store to Courier;
ref(int) from Courier to Store;
disconnect Courier and Store;
ref(int) from Store to Customer;
disconnect Store and Customer;

[basicstyle=, numbers=left, language = ensemble]
aux global protocol Browse
(role Customer, role Store, role Courier)
item(string) from Customer to Store;
price(int) from Store to Customer;
choice at Customer
do Browse(Customer, Store, Courier);
do Deliver(Customer, Store, Courier);
quit() from Customer to Store;
disconnect Store and Customer;

Global protocol for

Consider Figure <ref>, which details the protocol
for an online shopping service, inspired by the travel agency protocol detailed
by Hu and Yoshida, 2017. The protocol is organised as three
subprotocols: , the entry-point;
, where the customer
repeatedly requests quotes for items; and , where
the store requests delivery from a courier.
In contrast to , each connection must be established explicitly
(note that +connect+ replaces +from+ when initiating a

Note in particular that  is only involved in the
subprotocol. The store can therefore choose
which courier to use based on, for example, the weight of the item or the
customer's location. Furthermore, it is not necessary to involve the courier if
the customer does not choose to make a purchase.

§ : AN ACTOR LANGUAGE FOR RUNTIME ADAPTATION

In this section, we present , a new session-typed actor-based
language based on Ensemble [Harvey, 2015, Harvey and Sventek, 2017].
actors are addressable, single-threaded entities with share-nothing
semantics, and communicate via message passing. However, differently from the
classic definition of the actor model
[Hewitt et al., 1973, Agha, 1990], the
communication model in is channel-based.
supports both static and dynamic topologies:

Static Topologies All participants are present at the start of the session and remain involved for
the duration of the session. This is based on traditional MPSTs [Honda et al., 2008].

Dynamic Topologies Participants can connect and disconnect during a session. This builds on the more recent idea of explicit connection actions [Hu and Yoshida, 2017].

§.§ : basic language features

type Isnd is interface(out integer output)
type Ircv is interface(in integer input)

stage home
actor sender presents Isnd
value = 1;
send value on output;
value := value + 1;

actor receiver presents Ircv
receive data from input;
printString(": ");

s = new sender();
r = new receiver();
establish topology(s, r);

A simple program

An actor has its own private state
and a single thread of control expressed as a
clause, which is repeated until explicitly told to stop.
Every actor executes within a , which represents a memory space.
Actors do not share state, but instead communicate via message passing along
half-duplex, simply-typed channels.

<ref> shows a simple program which
defines, instantiates and connects two actors, one of which sends linearly
increasing values to the other.
The program defines two interfaces +Isnd+ and +Ircv+, declaring an output and input channel respectively.
The +boot+ clause (lines 19–23) is
executed first and creates an instance of each actor (lines 20–21), using the
appropriate +constructor+ (lines 7 and 13, respectively). This creates
and begins executing new threads for each actor, which follow the logic of the
relevant +behaviour+ clause. Next, the +boot+ clause binds the
actor's channels together (line 22, discussed later in
Once bound, the
+sender+ actor sends the contents of +value+ on its channel,
increments it, and goes back to the beginning of its behaviour loop (lines
8–11). The +receiver+ actor waits for a message, binds the message to
+data+, displays it, and returns to the top of its behaviour loop
(lines 14–18).
inherits Ensemble's native support for
runtime software adaptation actions [Harvey and Sventek, 2017]:

Discover The ability to locate an arbitrary actor or stage reference at runtime, given an  and .

Install Given an actor type, the ability to  it at a specified stage.

Migrate The ability for an executing actor to move to another

Replace The ability to replace an executing actor A by a new instantiation of actor B, the latter continuing at the same stage as A, if A and B have the same .

Interact: Given an actor reference (either spawned, discovered, or communicated),  the ability to connect to its channels at runtime and then communicate.

We focus on the underlined actions and apply session types to guarantee communication safety. The reason for this choice is that discover, replace and interact are actions that modify how actors operate, whereas the other actions, install and migrate, affect where actors operate, but not their behaviour.

[mybox=colBox] (SGP) Scribble
Global Protocol;
[mybox=colBox,right=of SGP] (SLP) Scribble
Local Protocol;
[mybox=colBox,right=of SLP] (EST) EnsembleS
[mybox=colBox,right=of EST] (EXE) Executable;
[myarrow=SLP] (SGP) – (SLP);
[myarrow=EST] (SLP) – (EST);
[myarrow=EXE] (EST) – (EXE);
(SGP) – node[below, yshift=-0.75cm]Scribble Tool (SLP);
(SLP) – node[below, yshift=-0.75cm]StMungo (EST);
(EST) – node[below, yshift=-0.75cm]EnsembleS Compiler (EXE);

Automatic Actor Skeleton Generation Process

§.§ Session types in

A  type in represents a communication protocol for an actor, i.e., a local protocol (or local session type) validated and projected from a global session type.

We extend the StMungo [Kouzapas et al., 2018] tool to generate template code that supports session types. <ref> shows an overview of the actor template code generation from a global session type, and <ref> shows an example of the generated code.

First, a developer defines a global session type in Scribble [Yoshida et al., 2014] (<ref>, first stage).
The Scribble tool checks that the protocol is well-formed and valid according to MPST theory and projects the global protocol into local protocols for each participant (<ref>, second stage).
For each local protocol, the StMungo tool produces (<ref>, third stage) $i$) the  type, $ii$) the interface and type definitions, and $iii$) the actor template.
The generated code is parsed by the compiler, producing executable code (<ref>, fourth stage).

Let us now look at the  local protocol, given in <ref>.
Following the code generation process in <ref>, the template items $i$), $ii$) and $iii$) for  correspond respectively to the code blocks starting in lines 3, 14, and 24 in <ref>.

The  local protocol is translated as an  type in <ref> (lines 3–12).
It shows a sequence of send and receive actions (lines 4–6), followed by a choice at  (lines 7–12), which determines the next set of communication actions.

Following session type specifications,
channels define both the payload type and the  that this channel expects to interact with (lines 14–21,  <ref>). The compiler uses this information to ensure that the  of each channel matches the  associated with the actor it is connected to.

An  may  a  type (line 24, <ref>).
This tells the compiler that the logic within the  clause of that actor must follow the communication protocol defined in the .

It is important to note that the code generation in
<ref> is optional and the typechecker is
independent of this process.

[ escapechar=@,
numbers=left, multicols=2]
// FILE AUTOMATICALLY GENERATED
type Buy1 is session(
book(string) to Sell;
book(int) from Sell;
quote(int) to Buy2;
choice at Buy2
Choice0_agree(string) from Buy2;
transfer(int) to Sell;
Choice0_quit(string) from Buy2;
type Buy1I is interface(
out Seller, string toSell_string,
in Seller, integer fromSell_integer,
out Buy2, integer toBuy2_integer,
in Buy2, Choice0 fromBuy2_agreequit,
in Buy2, string fromBuy2_string,
out Sell, integer toSell_integer,
stage home
actor Buy1A presents Buy1I follows Buy1
payload1 = "";
send payload1 on toSell_string;
receive payload2 from fromSell_integer;
payload3 = 42;
send payload3 on toBuy2_integer;
// Receive choice from other actor
receive payload4 from fromBuy2_agreequit;
case Choice0_agree:
receive payload5 from fromBuy2_string;
payload6 = 42;
send payload6 on toSell_integer;
case Choice0_quit:
receive payload7 from fromBuy2_string;

// Omitted: Buy2A and SellA actors
buyer1 = new Buy1A();
buyer2 = new Buy2A();
seller = new SellA();
// other actors...
establish topology(buyer1,buyer2,seller);

EnsembleS static session template

§.§ Channel connections: static and dynamic

If an actor follows a  type, then its channel connections must be 1-1. This is the standard linearity requirement for session types: if there are multiple senders on one channel, then their messages can interfere and it is not possible to statically check that the session is followed correctly.
avoids this problem by using a single channel for each message type between each pair of participants.
For example, in <ref>, each of the three actors communicates strings and integers with both of the other actors. Because channels are unidirectional, each actor therefore has 8 channels: 2 to send strings and 2 to send integers to both other actors, and similarly 4 channels for receiving.

Static connections.

When using session types with static topologies, and all actors in the
session are known from the beginning of the application, provides the
statement to create the connections between the
specified  actors (line 22, <ref>;
line 51, <ref>).
A compile-time error is generated if the topology is ill-defined (e.g., if the
+session+s do not compose or if the channels do not match).

Dynamic connections.
supports reconfigurable channels and dynamic connections, via  and  statements.
The  statement takes two references to actors which follow s (line 6, <ref>). It connects all of the channels of the two specified actors such that the channel and actor's s match.
A compile-time error is raised if the s are incompatible.
Conversely, the  statement disconnects (line 9, <ref>).

§.§ Adaptation via discovery and replacement

[ escapechar=@,
// define query alpha
query_a = alpha();
actor_s = discover(
Buyer1_interface, @Buyer1_session@, query_a);
if (actor_s[0].length > 1)
@link me with actor_s[0];@
msg = "book";
send msg on toB_string;
@unlink Buyer1_session;@

Session type-based discovery

supports runtime discovery of local or remote actor
instances. As an example, in a sensor network, it may be desirable to connect to a
sensor which has a battery level above a certain threshold. The query
language allows the user to define a query on non-functional properties (such as
battery level, signal strength, or name), as well as the channels exposed by an
actor's interface. This ensures that any discovered actor has the correct number
and type of channels, and satisfies user's preferences. To ensure that the
discovered actor also obeys a declared protocol, uses
types in the discovery process. The green box in
<ref> shows how a  is
used in the actor discovery process, and the yellow box shows how such actors
are connected together.
Runtime discovery does not appear in the  because it does not affect the behaviour of an application directly.

numbers=left, multicols=2]
// session and interface definitions
actor fastA presents accountingI
follows accountingSession
receive data on input;
send data on output;

actor slowA presents accountingI
follows accountingSession
pS= new property[2] of property("",0);
pS[0]:= new property("serial",823);
pS[1]:= new property("version",2);
publish pS;

receive data on input;
send data on output;

query alpha()  $serial==823 && $version<4;

actor main presents mainI
// Find the slow actors matching query
actor_s = discover(accountingI,
accountingSession, alpha());
// Replace them with efficient versions
if(actor_s[0].length > 1)
replace actor_s[0] with fastA();

Session type-based replacement

also supports the replacement of executing actors, much like the
hot-code swapping in Erlang [Cesarini and Vinoski, 2016].  The new actor
must present the same interface as it takes over the channels of the
actor being replaced at the location it was executing.  Replacement happens at
the beginning of an actor's  loop. Replacement has many uses,
such as updating, changing, or extending some of the functionalities of existing
software, and is particularly useful in embedded
systems [Hughes et al., 2009, Hui and Culler, 2004].
The existing and new actors must follow the same
type, guaranteeing that replacement will not break existing actor

<ref> shows an example of a main
actor searching for actors of type  (line 32), and replacing them
with new actors of type  (lines 35–37). The  actors are located by defining a query (line 26) over user-defined properties, which are published (lines 16–18). The discovery process is the same as above, but now the discovered actors are used for replacement rather than just communication.

§.§ Implementation

is implemented in C, and supports reference-counted garbage
collection and exceltions. Applications are compiled to Java source code,
and then to custom Java class files for use with a custom VM [Cameron et al., 2013].
These applications can be executed on the desktop, parallel accelerators
(e.g. GPUs), Raspberry Pi, Lego NXT, and Tmote Sky hardware platforms, and use a
range of networking technologies.

Compact representations of session types are retained at runtime in order to
support discovery.
skeleton generation code is based on the StMungo
tool [Kouzapas et al., 2018], which is implemented as an ANTLR
listener, and session typechecking is supported by modifying the original
Ensemble typechecker to ensure that each communication action is permitted by
the actor's declared session type.

Since builds directly on top of the original Ensemble implementation,
it inherits Ensemble's runtime system. Performance results can be found
in [Harvey and Sventek, 2017].

§ CASE STUDY: DNS

[ escapechar=@,
numbers=left, multicols=2]
type Iclient is interface(
outRootServer,string RootServer_stringOut,
in RootServer,string RootServer_stringIn,
outZoneServer,string ZoneServer_stringOut,
in ZoneServer,string ZoneServer_stringIn,
in ZoneServer,choice_enum	ZoneServer_choiceIn,
in RootServer,choice_enum	RootServer_choiceIn)

type choice_enum is

query find_name(string n) $name == n; }

actor c presents Iclient
follows Client {
dom_name = "nii.ac.jp";
constructor() { }
rootQuery = find_name("jp");
// Find Root Server
root_s =
discover(IServer, RootServer, rootQuery);
// search until root_s non-empty
link me with root_s[0];
send domain_name on RootServer_stringOut;
receive c_msg	from RootServer_choiceIn;
case TLDResponse:
receive ZoneServerAddr_msg
from RootServer_stringIn;
unlink RootServer;
while(true) Lookup : {
// Find ZoneServer
zone_s =
discover(IServer,	ZoneServer,
link me with zone_s[0];
// Ask ZoneServer
send dom_name on ZoneServer_stringOut;
receive c_msg2 from ZoneServer_choiceIn;
case PartialResolution:
receive str_msg from ZoneServer_stringIn;
ZoneServerAddr_msg := str_msg;
unlink ZoneServer;
continue Lookup;
case InvalidDomain:
receive str_msg from ZoneServer_stringIn;
unlink ZoneServer;
case ResolutionComplete:
receive str_msg from ZoneServer_stringIn;
unlink ZoneServer;
break Lookup;
// keep looking
case InvalidTLD:
receive str_msg from RootServer_stringIn;
unlink RootServer;
} } }
\end{lstlisting}
\caption{EnsembleS DNS client}
\label{lst:ensemble-dns-client}
\end{figure}

\begin{wrapfigure}{l}{0.525\textwidth}
\begin{lstlisting}[ escapechar=@,language=ensemble]
type Client is session(
connect RootServer;
RootRequest(DomainName) to RootServer;
choice at RootServer{
TLDResponse(ZoneServerAddress) from RootServer;
disconnect RootServer;
rec Lookup {
connect ZoneServer;
ResolutionRequest(DomainName) to ZoneServer;
choice at ZoneServer {
from ZoneServer;
disconnect ZoneServer;
continue Lookup;
} or {
InvalidDomain(String) from ZoneServer;
disconnect ZoneServer;
} or {
ResolutionComplete(IPAddress) from ZoneServer;
disconnect ZoneServer;
} or {
InvalidTLD(String) from RootServer;
disconnect RootServer;
\end{lstlisting}
\caption{EnsembleS DNS client \texttt{session} type \vspace{-1em}}
\label{lst:ensemble-dns-client-session}
\end{wrapfigure}
To illustrate the use of session types for adaptive programming, we consider a
real-world case study: the domain name system (DNS). DNS is a hierarchical,
globally distributed translation system that converts an internet host name
(domain name) into its corresponding numerical Internet Protocol (IP)
address~[Mockapetris, 1987].

The process begins by transmitting a domain name to one of many well-known \emph{root} servers. This server either rejects bad requests, or provides the information to contact a \emph{zone} server. The zone server may know the IP address of the domain name; if not it refers the request to another zone server. This process continues until either the IP address is returned, or the name cannot be found.

To develop an adaptive DNS example, we assume no \emph{a priori} information
about server location, and instead use explicit discovery to find
root and zone servers based on session types and server properties. We use an
existing Scribble description of DNS as a starting point~[Fowler, 2016]. To
illustrate adaptation we focus on the client who is querying DNS.

\autoref{lst:ensemble-dns-client-session} shows the \texttt{session} type for the client actor which asks DNS to resolve a domain name. The client first asks for a root server (lines 2--3), and then either is informed that the request is invalid (lines 24--25) or recursively queries zone servers (lines 7--22) until the IP address is found (lines 19--20), or an error is reported (lines 16--17). Based on this \texttt{session}, StMungo generates \EnsembleS types and interface definitions and a skeleton actor. Minimally completing the generated skeleton produces the code in \autoref{lst:ensemble-dns-client}.

In this example, discovery is used to locate the root server (lines 21--25, in
\autoref{lst:ensemble-dns-client}) and the zone server (line 37). In each case,
the \texttt{session} for the relevant server is provided to ensure that the
discovered actor follows the expected protocol.  When either server is located,
the client \texttt{link}s with it (lines 27 and 39), enabling communication.
When communication with the server is no longer required, the client
\texttt{unlink}s explicitly (lines 34, 47, 51, 55, 62).

Although explicit discovery is used at the language level, there is nothing to
prevent the implementation of discovery from caching the addresses of the root
and zone servers. This does not affect the use of sessions in discovery or the
safety they provide, as the type-based guarantees are still enforced. However,
this would potentially improve performance of the system. Additionally, if a
cached entry becomes stale, the full discovery process can again be used without
code modification or degradation in trust.

A version of DNS which uses discovery allows the system to become more flexible
and resilient to changing operational conditions, such as topology changes in
the servers and their data. Session types ensure compatibility
with the discovered actors.

\section{A Core Calculus for EnsembleS}\label{sec:core-calculus}

In this section, we provide a formal characterisation of \textsc{EnsembleS}.
In doing so, we show that our integration of adaptation with multiparty session
types is safe, allowing adaptation while ruling out communication mismatches.

\subparagraph{Relationship to implementation.}
Our core calculus aims to distil the essence of the interplay between adaptation
and session-typed communication with explicit connection actions.
Therefore, we concentrate on a functional core calculus rather than an
imperative one: imperative variable binding serves only to clutter the
formalism, and our fine-grain call-by-value representation can be thought of as
an intermediate language.

Interfaces and unidirectional, simply-typed channels in
\textsc{EnsembleS} are an implementation artifact:
sending on a channel whose type changes is equivalent to sending on multiple
channels with different types.
Moreover, following theoretical accounts of multiparty session
types~[Honda et~al., 2008, Coppo et~al., 2016, Hu and Yoshida, 2017],
instead of having send and receive (resp.\ connect and accept) operations
followed by branching (as done in Mungo and StMungo), we have
unified \calcwd{send} and \calcwd{receive} constructs which communicate a label
along with the message payload.

Since session typing is the interesting part of discovery, we omit
properties and queries from the formalism; their inclusion is routine.
Finally, we concentrate on \emph{dynamic} topologies with explicit
connection actions rather than static topologies since they are important for
adaptation and more interesting technically.

\subsection{Syntax}

\begin{figure}[t]
\header{Syntax of Types and Terms}
\[
\begin{array}{lrcl}
\text{Actor class names} & \actorcls \\
\text{Actor definitions} & D & ::= & \actordef{\actorcls}{\loctya}{M} \\
\text{Roles} & \prole, \qrole, \srole, \trole \\
\text{Recursion Labels} & l \\
\text{Behaviours} & \behaviour & ::= & M \midspace \bstop \\
\text{Types} & A, B & ::= & \pidty{S} \midspace \one \\
\text{Values} & V, W & ::= & x \midspace () \\
\text{Actions} & L & ::= & \effreturn{V} \midspace \continue{l} \midspace \raiseexn \\
& & \midspace & \new{\actorcls} \midspace \self \midspace
\replace{V}{\behaviour} \midspace \newdiscover{S}  \\
& & \midspace & \newconn{\ell}{V}{W}{\prole}
\midspace  \newaccept{\prole}{\ell_i(x_i) \mapsto M_i}_i \\
& & \midspace & \newsend{\ell}{V}{\prole} \midspace
\newrecv{\prole}{\ell_i(x_i) \mapsto M_i}_i \\
& & \midspace & \newwait{\prole} \midspace \newdisconn{\prole} \\
\text{Computations} & M, N & ::= & \efflet{x}{M}{N} \midspace \trycatch{L}{M}
\midspace \annst{l}{M} \midspace L
\end{array}
\]
\header{Syntax of Session Types}
\[
\begin{array}{lrcl}
\text{Session Actions} & \locacta, \locactb & ::= &
\localtysend{\prole}{\ell}{\tya} \midspace \localtyconn{\prole}{\ell}{\tya}
\midspace \localtyrecv{\prole}{\ell}{\tya}
\midspace \localtyaccept{\prole}{\ell}{\tya} \midspace \localtywait{\prole} \\
\text{Session Types} & \loctya, \loctyb, \loctyc & ::= &
\sumact{i \in I}{\alpha_i \then \locty_i} \midspace \recty{X}{\loctya} \midspace X \midspace
\localtydisconn{\prole} \midspace \localend \\
\text{Communication Actions} & \commdir & ::= & {!} \midspace {?} \\
\text{Disconnection Actions} & \disconndir & ::= & {\waitact} \midspace {\disconnact}
\end{array}
\]
\caption{Syntax}
\label{fig:syntax}
\end{figure}

\subparagraph{Definitions.}
Figure~\ref{fig:syntax} shows the syntax of Core \textsc{EnsembleS} terms and types.
We let $$ range over actor class names and $D$ range over definitions;
each definition $M$ specifies the actor's class name,
session type, and behaviour.
Like class tables in Featherweight Java~[Igarashi et~al., 2001],
we assume a fixed mapping from class names to definitions.

\subparagraph{Values.}
Since our calculus is inherently effectful, we work in the setting of
\emph{fine-grain call-by-value}~[Levy et~al., 2003], where we have an
explicit static stratification of values and computations and an explicit
evaluation order similar to A-normal form~[Flanagan et~al., 1993].
Values $V, W$ describe data that has been computed, and for the sake of simplicity,
consist of variables and the unit value.
Other base values (such as integers or booleans) can be encoded or added

\subparagraph{Computations.}
The $xMN$ construct evaluates $M$, binding its result to $x$ in
$N$.  The calculus supports exception handling over a single \emph{action} $L$
using $LM$, where $M$ is evaluated if $L$ raises an exception, and
labelled recursion using $lM$, stating that
inside term $M$, a process can recurse to label $l$ using $l$.
\emph{Actions} $L$ denote the basic steps of a computation.
The $V$ construct denotes a value.

\subparagraph{Concurrency and adaptation constructs.}
The $$ construct spawns a new actor of class $$ and
returns its PID. The $$ construct returns the current actor's PID.
An actor can replace the behaviour of
itself or another actor $V$ using $V$. An actor can
\emph{discover} other actors following a session type $$ using the
$$ construct, which returns the PID of the discovered

\subparagraph{Session communication constructs.}
An actor can connect to an actor $W$ playing role $$ using
$ℓVW$, sending a message with label $ℓ$ and payload
An actor can accept a connection from another actor playing role
$$ using $ℓ_ix_i ↦M_i_i$, which
allows an actor to receive a choice of messages; given a message with label
$ℓ_j$, the payload is bound to $x_j$ in the continuation $N_j$.
Once connected, an actor can communicate using the $send$ and
$receive$ constructs. An actor can disconnect from
$$ using $$, and await the disconnection of
$$ using $$.

\subparagraph{Types.}
Types, ranged over by $, $, include the unit type $$ and process IDs
$$; the parameter $$ refers to the statically-known
initial session type of the actor (i.e., the session type declared in the
$follows$ clause of a definition).
Unlike in channel-based session-typed systems, process IDs themselves need not
be linear: any number of actors can have a \emph{reference} to another actor,
but each actor may only be in a single session at a time. PIDs can be passed as
payloads in session communications.

\subparagraph{Session types.}

Session types are ranged over by $, , $ and follow the
formulation of~Hu and Yoshida, 2017. A session type can be a choice of actions,
written $i ∈I$, a recursive session type
$X$ binding recursion variable $X$ in continuation $$,
a recursion variable $X$, a disconnection action $$,
or the finished session $$.
The syntax of session types is more liberal than traditional
`directed' presentations in order to allow output-directed choices to send or
connect to different roles.

Session actions
$$ involve sending ($!$), receiving ($?$), connecting ($!!$), or
accepting ($??$) a message $ℓ(A)$ with label $ℓ$ and type $A$;
or awaiting another participant's disconnection
As well as disallowing self-communication, following~Hu and Yoshida, 2017,
we require the following syntactic restrictions on session types:

\begin{definition}[Syntactic validity]
A choice type $S = \sumact{i \in I}{\locact_i \then \loctya_i}$ is \emph{syntactically valid}
\begin{enumerate}
\item it is an output choice, i.e., each $\locact_i$ is a send or connection
action; or
\item it is a \emph{directed} input choice, i.e., $S =\sumact{i \in I}{\localtyrecv{\prole}{\ell_i}{A_i} {.} \loctya_i}$
$S = \sumact{i \in I}{\localtyaccept{\prole}{\ell_i}{A_i} {.} \loctya_i}$; or
\item the choice consists of single wait action $\localtywait{\prole} \then
\loctya$.
\end{enumerate}
\end{definition}
In the remainder of the paper, we assume that all session types are
syntactically valid.

\subparagraph{Session correlation.}
The most general form of explicit connection actions allows a participant to
leave and re-join a session, or accept connections from multiple different
participants. Such generality comes at a cost, since care must be taken to
ensure that the \emph{same} participant plays the role throughout the session.

To address this \emph{session correlation} issue,~Hu and Yoshida, 2017 propose two
solutions: either augment
global types with type-level assertions and check conformance dynamically, or adopt
a lightweight syntactic restriction which requires that
each local type must contain at most a single accept action as its top-level
construct. We opt for the latter, enforcing the constraint as part of our safety
property (\secref{sec:formalism:preservation}), and by requiring that
$$ does not have a continuation. (Note that the behaviour
will repeat, so $$ will be able to accept again after disconnecting).
As~Hu and Yoshida, 2017 show, this design still supports the most common use cases of
explicit connection actions.

\subparagraph{Global types.}
Traditional MPST works~[Honda et~al., 2008, Coppo et~al., 2016]
use \emph{global types} to describe the interactions between participants at a
global level, which are then projected into \emph{local types}; projectability
ensures safety and deadlock-freedom.

Since we are using explicit connection actions, traditional approaches are
insufficiently flexible as they do not account for certain roles being present
in certain branches but not others. Following~Scalas et~al., 2017 and
subsequently non-classical MPSTs~[Scalas and Yoshida, 2019], we instead formulate our
typing rules and safety properties using collections of local types.

It is, however, still convenient to write a global type and have local types
computed programatically. Global types are defined as follows:

\[
\begin{array}{lrcl}
\text{Global Actions} & \globact & ::= & \globalsend{\prole}{\qrole}{\ell}{\tya}
\midspace
\globalconn{\prole}{\qrole}{\ell}{\tya}
\midspace
\globaldisconn{\prole}{\qrole} \\
\text{Global Types} & G & ::= & \sumact{i \in I}{\globact_i \then G_i} \midspace \recty{X}{G} \midspace X \midspace \globalend
\end{array}
\]}
Global actions $$ describe interactions between participants:
$ℓ$ states that role $$ sends a
message with label $ℓ$ and payload type $$ to $$. Similarly,
$ℓ$ states that $$ connects to
$$ by sending a message with label $ℓ$ and payload type $$. The
disconnection action $$ states that role $$
disconnects from role $$.

We can write the \texttt{OnlineStore} example from~\autoref{sec:session-types}
as follows:

\[
\bl
\globalconn{\role{Customer}}{Store}{\var{login}}{\tylit{String}} \then
\mu \mkwd{Browse} \then \\
\quad
\bl
\quad
\bl
\globalsend{\role{Customer}}{\role{Store}}{\var{item}}{\tylit{String}}
\then \globalsend{\role{Store}}{\role{Customer}}{\var{price}}{\tylit{Int}}
\then \mkwd{Browse}
\el
\\
\\
\quad
\bl
\globalsend{\role{Customer}}{\role{Store}}{\var{address}}{\tylit{String}}
\then \globalconn{\role{Store}}{\role{Courier}}{\var{deliver}}{\tylit{String}}
\then \\
\globalsend{\role{Courier}}{\role{Store}}{\var{ref}}{\tylit{Int}}
\then \globaldisconn{\role{Courier}}{\role{Store}} \then \globalsend{\role{Store}}{\role{Customer}}{\var{ref}}{\tylit{Int}}
\then \\
\globaldisconn{\role{Store}}{\role{Customer}} \then \globalend
\el
\\
\\
\quad
\bl
\globalsend{\role{Customer}}{\role{Store}}{\var{quit}}{\one} \then
\globaldisconn{\role{Store}}{\role{Customer}} \then \globalend
\el
\el
\el
\]}Although projectability in our setting does not necessarily guarantee safety and
deadlock-freedom, we show a projection algorithm, adapted from that
of~Hu and Yoshida, 2017, in Appendix~\ref{appendix:projection}. The resulting local
types can then be checked for safety~\secrefp{sec:formalism:preservation}.

\subparagraph{Protocols and Programs.}
Terms do not live in isolation; they refer to a set of \emph{protocols}, and
evaluate in the context of an actor.
A \emph{protocol} maps role names to local session types.

\begin{definition}[Protocol]
A \emph{protocol} is a set $\{ \prole_i : \loctya_i \}_i$ mapping role names to
session types.
\end{definition}

As an example, consider the protocol for the online shop example:

\[
\left\{
\bl
\role{Customer} : \localtyconn{\role{Store}}{\var{login}}{\tylit{String}}
\then \mu \mkwd{Browse} \then \\
\bl
\qquad
\localtysend{\role{Store}}{\var{item}}{\tylit{String}} \then
\localtyrecv{\role{Store}}{\var{price}}{\tylit{Int}} \then
\mkwd{Browse} \\
\quad +
\quad
\localtysend{\role{Store}}{\var{address}}{\tylit{String}} \then
\localtyrecv{\role{Store}}{\var{ref}}{\tylit{Int}} \then
\localtywait{\role{Store}} \then \localend \\
\quad +
\quad
\localtysend{\role{Store}}{\var{quit}}{\one} \then
\localtywait{\role{Store}} \then \localend,
\vspace{0.5em}
\el
\\
\role{Store} :
\localtyaccept{\role{Customer}}{\var{login}}{\mkwd{String}} \then
\mu \mkwd{Browse} \then \\
\bl
\qquad
\localtyrecv{\role{Customer}}{\var{item}}{\mkwd{String}} \then
\localtysend{\role{Customer}}{\var{price}}{\mkwd{Int}} \then
\mkwd{Browse} \\
\quad + \quad
\localtyrecv{\role{Customer}}{\var{address}}{\mkwd{String}} \then
\localtyconn{\role{Courier}}{\var{deliver}}{\mkwd{String}} \then
\localtyrecv{\role{Courier}}{\var{ref}}{\mkwd{Int}} \then \\
\qquad
\localtywait{\role{Courier}} \then
\localtysend{\role{Customer}}{\var{ref}}{\mkwd{Int}} \then
\localtydisconn{\role{Customer}} \\
\quad + \quad
\localtyrecv{\role{Customer}}{\var{quit}}{\one} \then
\localtydisconn{\role{Customer}},
\vspace{0.5em}
\el
\\
\role{Courier} :
\localtyaccept{\role{Store}}{\var{deliver}}{\tylit{String}} \then
\localtysend{\role{Store}}{\var{ref}}{\tylit{Int}} \then
\localtydisconn{\role{Store}}
\el
\right\}
\]

We can now consider an implementation of a $Store$ actor, which uses
discovery to find a courier.  We write $ℓx; M$ and
$ℓx; M$ as
syntactic sugar for
$ ℓx ↦M$ and
$ ℓx ↦M$ respectively, and write
$M; N$ as syntactic sugar for $xMN$ for a fresh variable $x$.
We assume the existence of a function \mkwd{lookupPrice}, and define
$CourierType$ as
StoredeliverString StorerefInt Store

\[
\bl
\calcwd{actor} \: \mkwd{Store} \: \calcwd{follows} \: \ty{\role{Store}} \: \{ \\
\simpleaccept{\var{login}}{\var{credentials}}{\role{Customer}}; \\
\annstone{\mkwd{Browse}} \\
\quad
\bl
\newrecvone{\role{Customer}} \{ \\
\quad
\bl
\msg{\var{item}}{\var{name}} \mapsto \\
\quad
\bl
\newsend{\var{price}}{\mkwd{lookupPrice}(\var{name})}{\role{Customer}};
\\
\continue{\mkwd{Browse}}
\el
\\
\msg{\var{address}}{\var{addr}} \mapsto \\
\quad
\bl
\efflettwo{\var{pid}}{\newdiscover{\mkwd{CourierType}}} \\
\newconn{\var{deliver}}{\var{addr}}{\var{pid}}{\role{Courier}}; \\
\simplerecv{\var{ref}}{\var{r}}{\role{Courier}}; \\
\newwait{\role{Courier}}; \\
\newsend{\var{ref}}{\var{r}}{\role{Customer}}; \\
\newdisconn{\role{Customer}}
\el
} \\
\msg{\var{quit}}{()} \mapsto \newdisconn{\role{Customer}} \\
\el
} \\
\}
\el
\el
} \\
\}
\el
\]

A \emph{program} consists of actor definitions, protocol definitions, and the
`boot' clause to be run in order to set up initial actor communication.

\begin{definition}[Program]
An \EnsembleS \emph{program} is a 3-tuple $(\seq{D}, \seq{P}, M)$ of
a set of definitions, protocols, and an initial term to be evaluated.
\end{definition}

In the context of a program, we write $$ to refer to the session type
associated with role $$ as defined by the set of protocols.
Given an actor definition $M$,
we define $ = $ and $u = M$.

\subsection{Typing rules}

\begin{figure}[t]
\begin{minipage}[t]{0.26\textwidth}
\headersig{Definition typing}{$\dseq{D}$}
\begin{mathpar}
\inferrule
\tseq[\loctya]{\cdot}{\loctya}{M}{\tya}{\localend}
{ \dseq{\actordef{\actorcls}{\loctya}{M}} }
\end{mathpar}
\end{minipage}
\hfill
\begin{minipage}[t]{0.26\textwidth}
\headersig{Value typing}{$\vseq{\Gamma}{V}{\tya}$}
\begin{mathpar}
\inferrule
{ x : A \in \Gamma }
{ \vseq{\Gamma}{x}{A} }

\inferrule
{ }
{ \vseq{\Gamma}{()}{\one} }
\end{mathpar}
\end{minipage}
\hfill
\begin{minipage}[t]{0.42\textwidth}
\headersig{Behaviour typing}{$\bseq[\loctya]{\Gamma}{\behaviour}$}
\begin{mathpar}
\inferrule
{ }
{ \bseq[\loctya]{\Gamma}{\bstop} }

\inferrule
{ \tseq[\loctya]{\Gamma}{\loctya}{M}{A}{\localend} }
{ \bseq[\loctya]{\Gamma}{M} }
\end{mathpar}
\end{minipage}

\headersig{Typing rules for computations}{$\tseq{\Gamma}{\loctya}{M}{A}{\loctya'}$}

\subheader{Functional Rules}
\begin{mathpar}
\inferrule
\tseq{\Gamma}{\loctya}{M}{\tya}{\loctya'} \\
\tseq{\Gamma, x : \tya}{\loctya'}{N}{\tyb}{\loctya''}
{ \tseq{\Gamma}{\loctya}{\efflet{x}{M}{N}}{B}{\loctya''} }

\inferrule
{ \vseq{\Gamma}{V}{A} }
{ \tseq{\Gamma}{\loctya}{\effreturn{V}}{\tya}{\loctya} }

\inferrule
{ \tseq{\Gamma, l : \loctya}{\loctya}{M}{\tya}{\loctya'} }
\tseq{\Gamma}{\loctya}{\annst{l}{M}}{\tya}{\loctya'}

\inferrule
{ }
{ \tseq{\Gamma, l : \loctya}{\loctya}{\continue{l}}{\tya}{\loctya'} }
\end{mathpar}

\subheader{Actor / Adaptation Rules}
\begin{mathpar}
\inferrule
{ \sesstype{u} = \loctyc  }
{ \tseq{\Gamma}{\loctya}{\new{u}}{\pidty{\loctyc}}{\loctya} }

\inferrule
{ }
{ \tseq{\Gamma}{\loctya}{\self}{\pidty{\loctyb}}{\loctya}  }

\inferrule
{ }
{  \tseq{\Gamma}{\loctya}{\newdiscover{\loctyc}}{\pidty{\loctyc}}{\loctya} }

\inferrule
{ \vseq{\Gamma}{V}{\pidty{\loctyc}} \\ \bseq[\loctyc]{\Gamma}{\behaviour}  }
{ \tseq{\Gamma}{\loctya}{\replace{V}{\behaviour}}{\one}{\loctya} }
\end{mathpar}

\caption{Typing rules (1)}
\label{fig:term-typing-1}
\end{figure}

Figures~\ref{fig:term-typing-1} and~\ref{fig:term-typing-2} show the typing
rules for \EnsembleS. Value typing, with judgement $ΓVA$, states
that under environment $Γ$, value $V$ has type $A$.
Judgement $D$ states that an actor definition $uM$
is well-typed if its body is typable under, and fully consumes, its statically-defined session type
The behaviour typing judgement $[]Γ$ states that
given static session type $$, behaviour $$ is well-typed under
$Γ$. Specifically, $$ is always well-typed, and $M$ is well-typed if
it is typable under and fully consumes $$.

\subsubsection{Term typing.}\label{sec:formalism:term-typing}
The typing judgement for terms
$[]ΓMA'$ reads ``in an actor following $$, under typing environment $Γ$ and with current session
type $$, term $M$ has type $A$ and updates the session type to
$'$''. Note that the term typing judgement, reminiscent of parameterised
monads~[Atkey, 2009], contains a session precondition
$$ and may perform
some session communication actions to arrive at postcondition $'$.

\subparagraph{Functional rules.}
Rule \textsc{T-Let} is a sequencing operation: given a construct
$xMN$ where $M$ has pre-condition $$ and post-condition
$'$, and where $N$ has pre-condition $'$ and post-condition
$”$, the overall construct has pre-condition $$ and
post-condition $”$.

Following Kouzapas \emph{et al.}~[Kouzapas et~al., 2018], we formalise recursion through
expressions: term $lM$ states that $M$ is an expression which can loop to
$l$ by evaluating $l$.
We take an equi-recursive view of session types, identifying recursive sessions
with their unfolding ($μX. S = S { μX . S / X}$), and assume that recursion is guarded.
Rule \textsc{T-Rec}
extends the typing environment with a recursion label defined at the current
session type.
Rule \textsc{T-Continue} ensures that the pre-condition must match the label
stored in the environment, but has arbitrary type and any post-condition since
the return type and post-condition depend on the enclosing loop's base case.

\subparagraph{Actor and adaptation rules.}
Rule \textsc{T-New} states that creating an actor of
class $u$ returns a PID parameterised by the session type declared in the class
of $u$. Rule \textsc{T-Self} retrieves a PID for the current actor,
parameterised by the statically-defined session type of the local actor (i.e.,
the $$ in the judgement $[]ΓMA'$).
Rule \textsc{T-Discover} states $$ returns a PID of type
$$. Finally, given a behaviour $$ typable under a
static session type $$, and a process ID with the matching static type
$$, \textsc{T-Replace} allows replacement, and returns the unit

\begin{figure}[t]

\subheader{Exception handling rules}
\vspace{-1em}
\begin{mathpar}
\inferrule
{ }
{ \tseq{\Gamma}{\loctya}{\raiseexn}{\tya}{\loctya'} }

\inferrule
\tseq{\Gamma}{\loctya}{L}{A}{\loctya'} \\
\tseq{\Gamma}{\loctya}{M}{A}{\loctya'}
{ \tseq{\Gamma}{\loctya}{\trycatch{L}{M}}{A}{\loctya'} }
\end{mathpar}

\subheader{Session communication rules}
\begin{mathpar}
\inferrule
\localtyconn{\prole_j}{\ell_j}{\tya_j} \in \{\locact_i\}_{i \in I} \\
\vseq{\Gamma}{V}{\tya_j} \\
\vseq{\Gamma}{W}{\pidty{\loctyb}} \\
\loctyb = \ty{\prole_j}
{ \tseq{\Gamma}
{\sumact{i \in I}{\locact_i \then \loctya_i}}

\inferrule
{ \localtysend{\prole_j}{\ell_j}{\tya_j} \in \{ \locact_i \}_{i \in I} \\
\vseq{\Gamma}{V}{\tya_j} }
{ \tseq{\Gamma}{\sumact{i \in
I}{\locact_i \then \loctya_i}}{\newsend{\ell_j}{V}{\prole_j}}{\one}{\locty'_j}   }

\inferrule
(\tseq{\Gamma, x_i : \tyb_i}{\locty_i}{M_i}{\tya}{S})_{i \in I}
{ \tseq{\Gamma}
{\sumact{i \in I}{\localtyaccept{\qrole}{\ell_i}{\tyb_i} \then \locty_i}}
{\newaccept{\qrole}{\ell_i(x_i) \mapsto M_i}_{i \in I}}

\inferrule
(\tseq{\Gamma, x_i : \tyb_i}{\locty_i}{M_i}{A}{S})_{i \in I}
{ \tseq{\Gamma}
{\sumact{i \in I}{\localtyrecv{\qrole}{\ell_i}{\tyb_i} \then \locty_i}}
{\newrecv{\qrole}{\ell_i(x_i) \mapsto M_i}_{i \in I}}

\inferrule
{ }
{ \tseq{\Gamma}
{\localtywait{\qrole} \then \loctya}

\inferrule
{ }
{ \tseq{\Gamma}
{\localend} }
\end{mathpar}

\caption{Typing rules (2)}
\label{fig:term-typing-2}
\end{figure}

\subparagraph{Exception handling rules.}
Figure~\ref{fig:term-typing-2} shows the rules for exception handling and
session communication. \textsc{T-Raise} denotes raising an exception; since
it does not return, it can have an arbitrary return type and postcondition. Rule
\textsc{T-Try} types an exception handler $LM$ which acts over a
single action $L$. If $L$ raises an exception, then $M$ is evaluated instead.
Since $L$ only scopes over a single action, the $try$ and $catch$
clauses have the same pre- and post-conditions to allow the action to be retried
if necessary.

\begin{remark}
Following~Mostrous and Vasconcelos, 2018, our $\trycatch{L}{M}$ construct scopes over a
\emph{single} action and is discarded afterwards.
We opt for this simple approach since in our setting exceptions are a means
to an end, but (at the coast of a more involved type system) we could
potentially scope over multiple actions as long as the handler is compatible
with all potential exit conditions~[Gordon, 2020]. We leave a
thorough exploration to future work.
\end{remark}

\subparagraph{Session communication rules.}
Rule \textsc{T-Conn} types a term $ℓ_jVW_j$.
Given the precondition is a choice type
containing a branch $ℓ_j_j '_j$,
and the remote actor reference is $W$ of type $S$,
the rule ensures that $S$ is compatible with the type of $_j$,
and ensures that the label and payload are compatible with the session type.
The session type is then advanced to $'_j$.
Rule \textsc{T-Send} follows the same pattern.

Given a session type $i ∈Ix_iA_i S_i$, rule \textsc{T-Accept} types term $ℓ_ix_i ↦M_i_i
∈I$, enabling an actor to accept connections with messages
$ℓ_i$, binding the payload $x_i$ in each continuation $M_i$.
Like $case$ expressions in functional languages, each continuation must
be typable under an environment extended with $x_i : A_i$, under session type
$_i$, and each branch must have same result type and postcondition.  Rule
\textsc{T-Recv} is similar.

Rule \textsc{T-Wait} handles waiting for a participant $$ to disconnect
from a session, requiring a pre-condition of $ $,
returning the unit type and advancing the session type to $$.
Rule \textsc{T-Disconnect} is similar and advances the session type to $$.

\subsection{Operational semantics}

We describe the semantics of \EnsembleS via a deterministic reduction relation
on terms, and a nondeterministic reduction relation on configurations.

\begin{figure}[t]
{\footnotesize \header{Runtime syntax} \vspace{-2em}}
\[
\begin{array}{lccl}
\text{Names} & n & ::= & a \midspace s \vspace{0.3em} \\
\text{Configurations} & \config{C}, \config{D}, \config{E} & ::= & (\nu n)
\config{C} \midspace \config{C} \parallel \config{D} \midspace
\eactor{a}{M}{\connstate}{\behaviour} \midspace \zap{\sessindextwo{s}{\prole}}
\midspace \confzero
\\
\text{Connection state} & \connstate & ::= & \bot \midspace
\newconnsess{s}{\prole}{\rolesetq} \vspace{0.3em} \\
\text{Runtime environments} \!\! & \rtenv & ::= & \cdot \midspace \rtenv, a : \loctya \midspace
\rtenv, \sessindexroles{s}{\prole}{\rolesetq}{\loctya} \vspace{0.3em} \\
\text{Evaluation contexts} & E & ::= & F \midspace \efflet{x}{E}{M} \\
\text{Top-level contexts} & F & ::= & [~] \midspace \trycatch{[~]}{M} \\
\text{Pure contexts} & \ep & ::= & [~] \midspace \efflet{x}{\ep}{M} \\
\end{array}
\]

\headersig{Term reduction}{$M \teval N$}
\[
\begin{array}{lrcl}
\textsc{E-Let} & \efflet{x}{\effreturn{V}}{M} & \teval & M \{ V / x \} \\
\textsc{E-TryReturn} & \trycatch{\effreturn{V}}{M} & \teval & \effreturn{V} \\
\textsc{E-TryRaise} & \trycatch{\raiseexn}{M} & \teval
& M \\
\textsc{E-Rec} & \annst{l}{M} & \teval & M \{ \annst{l}{M} / \continue{l} \} \\
\textsc{E-LiftM} & E[M] & \teval & E[N] \quad \text{if } M \teval N
\end{array}
\]
\headersig{Configuration reduction (1)}{$\config{C} \ceval \config{D}$}
\subheader{Actor / adaptation rules}
\begin{mathpar}
\inferrule
{ }
{ \eactor{a}{\effreturn{V}}{\bot}{M} \ceval \eactor{a}{M}{\bot}{M} }

\inferrule
{ b \text{ is fresh} \\ \bhv{u} = M }
\eactor{a}{E[\new{u}]}{\connstate}{\behaviour} \ceval \\\\
(\nu b) (\eactor{a}{E[\effreturn{b}]}{\connstate}{\behaviour} \parallel
\eactor{b}{M}{\bot}{M})

\inferrule
{ }
{ \eactor{a}{E[\replace{b}{\behaviour'}]}{\connstate_1}{\behaviour_1} \parallel
\eactor{b}{N}{\connstate_2}{\behaviour_2} \ceval \\\\
\eactor{a}{E[\effreturn{()}]}{\connstate_1}{\behaviour_1} \parallel
\eactor{b}{N}{\connstate_2}{\behaviour'} }

\inferrule
{ }
{ \eactor{a}{E[\replace{a}{\behaviour'}]}{\connstate}{\behaviour}
\ceval \\\\
\eactor{a}{E[\effreturn{()}]}{\connstate}{\behaviour'}}

\inferrule
{ \sesstype{b} = \loctya \\\\
\neg ((N = \effreturn{V} \vee N = \raiseexn) \wedge \behaviour_2 = \bstop)  }
{ \eactor{a}{E[\newdiscover{\loctya}]}{\connstate_1}{\behaviour_1} \parallel
\eactor{b}{E'[N]}{\connstate_2}{\behaviour_2} \ceval\\\\
\eactor{a}{E[\effreturn{b}]}{\connstate_1}{\behaviour_1} \parallel
\eactor{b}{E'[N]}{\connstate_2}{\behaviour_2}

\inferrule
{ }
{ \eactor{a}{E[\self]}{\connstate}{\behaviour}
\ceval
\eactor{a}{E[\effreturn{a}]}{\connstate}{\behaviour} }
\end{mathpar}

\caption{Operational semantics (1)}
\label{fig:config-reduction-1}
\end{figure}

\subsubsection{Runtime syntax}

Figure~\ref{fig:config-reduction-1} shows the runtime syntax and the first part
of the reduction rules for \EnsembleS.

Whereas static syntax and typing rules describe code that a user would write,
runtime syntax arises during evaluation. We introduce two types of runtime name:
$s$ ranges over \emph{session names}, which are created when a process initiates
a session, and $a$ ranges over \emph{actor names}, which uniquely identify each
actor once it has been spawned by $new$.

\subparagraph{Configurations.}
Configurations, ranged over by $C, D, E$, represent
the concurrent fragment of the language. Like in the
$π$-calculus~[Milner, 1999],
name restrictions $(νn)C$ bind name $n$ in $C$,
$C ∥D$ denotes $C$ and $D$ running
in parallel, and the $$ configuration denotes the inactive process.

Actors are represented at runtime as a 4-tuple
$aM$, where $a$ is the actor's runtime name;
$M$ is the term currently evaluating; $$ is the connection state; and
$$ is the actor's current behaviour.
A connection state is either \emph{disconnected}, written $$, or playing role
$$ in session $s$ and connected to roles $$, written

Inspired by~Mostrous and Vasconcelos, 2018 and~Fowler et~al., 2019, a
\emph{zapper thread} $s$ indicates that participant
$$ in session $s$ cannot be used for future communications, for example
due to the actor playing the role crashing due to an unhandled exception.

\subparagraph{Runtime typing environments.}
Whereas $Γ$ is an unrestricted typing environment used for typing values
and configurations, we introduce $$ as a linear runtime environment.
Runtime environments can contain entries of type $a : S$, stating that actor $a$
has \emph{statically-defined} session type $S$, and entries of type
$sS$, stating that in session $s$, role
$$ is connected to roles $$ and \emph{currently} has session type

\subparagraph{Evaluation contexts.}
Due to our fine-grain call-by-value presentation, evaluation contexts $E$ allow
nesting only in the immediate subterm of a $let$ expression.
The top-level frame $F$ can either be a hole, or a single, top-level exception
handler. Pure contexts $$ do not include exception handling frames.

To run a program, we place it in an \emph{initial configuration}.

\begin{definition}[Initial configuration]
An \emph{initial configuration} for an \EnsembleS program with boot clause $M$
is of the form $(\nu a)(\eactor{a}{M}{\bot}{\bstop})$.
\end{definition}

\subsubsection{Reduction rules}

\begin{figure}[t]
\footnotesize{
\headersig{Configuration reduction (2)}{$\config{C} \ceval \config{D}$}
\subheader{Session reduction rules}
\begin{mathpar}
\inferrule
{ j \in I }
{ \eactor{a}{E[F[\newconn{\ell_j}{V}{b}{\qrole}]]}{\bot}{\behaviour_1} \parallel
\eactor{b}{E'[F'[\newaccept{\prole}{\ell_i(x_i) \mapsto M_i}_{i \in
I}]]}{\bot}{\behaviour_2} \ceval \\
(\nu s)
(\eactor{a}{E[\effreturn{()}]}{\newconnsess{s}{\prole}{\qrole}}{\behaviour_1} \parallel
\eactor{b}{E'[M_j \{ V / x_j \}]}{\newconnsess{s}{\qrole}{\prole}}{\behaviour_2})

\inferrule
{ \qrole \not\in \rolesetr }
\eactor{a}{E[F[\newconn{\ell_j}{V}{b}{\qrole}]]}{\newconnsess{s}{\prole}{\rolesetr}}{\behaviour_1} \parallel
\eactor{b}{E'[F'[\newaccept{\prole}{\ell_i(x_i) \mapsto N_i}_{i \in
I}]]}{\bot}{\behaviour_2} \ceval \\
\eactor{a}{E[\effreturn{()}]}{\newconnsess{s}{\prole}{\rolesetr, \qrole}}{\behaviour_1} \parallel
\eactor{b}{E'[N_j \{ V / x_j \}]}{\newconnsess{s}{\qrole}{\prole}}{\behaviour_2}

\inferrule
((N = \effreturn{V} \vee N = \ep[\raiseexn]) \wedge \behaviour_2 = \bstop) \vee
\connstate_2 \ne \bot
\eactor{a}{E[\newconn{\ell_j}{V}{b}{\qrole}]}{\connstate_1}{\behaviour_1} \parallel
\eactor{b}{N}{\connstate_2}{\behaviour_2} \ceval
\eactor{a}{E[\raiseexn]}{\connstate_1}{\behaviour_1} \parallel
\eactor{b}{N}{\connstate_2}{\behaviour_2}

\inferrule
{ }
{ \eactor{a}{E[F[\newwait{\qrole}]]}{\newconnsess{s}{\prole}{\rolesetr, \qrole}}{\behaviour_1}
\parallel
\eactor{b}{E'[F'[\newdisconn{\prole}]]}{\newconnsess{s}{\qrole}{\prole}}{\behaviour_2}
\ceval \\
\eactor{a}{E[\effreturn{()}]}{\newconnsess{s}{\prole}{\rolesetr}}{\behaviour_1} \parallel
\eactor{b}{E'[\effreturn{()}]}{\bot}{\behaviour_2}

\inferrule
{ j \in I \\ \qrole \in \rolesetr \\ \prole \in \rolesets }
\eactor{a}{E[F[\newsend{\ell_j}{V}{\qrole}]]}{\newconnsess{s}{\prole}{\rolesetr}}{\behaviour_1} \parallel
\eactor{b}{E'[F'[\newrecv{\prole}{\ell_i(x_i) \mapsto M_i}_{i \in
I}]]}{\newconnsess{s}{\qrole}{\rolesets}}{\behaviour_2} \ceval \\
\eactor{a}{E[\effreturn{()}]}{\newconnsess{s}{\prole}{\rolesetr}}{\behaviour_1} \parallel
\eactor{b}{E'[M_j \{ V / x_j \}]}{\newconnsess{s}{\qrole}{\rolesets}}{\behaviour_2}

\inferrule
{ }
(\nu s)(\eactor{a}{\effreturn{V}}{\newconnsess{s}{\prole}{\emptyset}}{\behaviour})
\ceval
\eactor{a}{\effreturn{V}}{\bot}{\behaviour}
\end{mathpar}
\caption{Operational semantics (2)}
\label{fig:config-reduction-2}
\end{figure}

\begin{figure}[t]
\headersig{Configuration reduction (3)}{$\config{C} \ceval \config{D}$}
\subheader{Exception handling rules}
\begin{mathpar}
\inferrule
{ \subj{M} = \qrole }
\eactor{a}{E[M]}{\newconnsess{s}{\prole}{\rolesetr}}{\behaviour} \parallel
\zap{\sessindextwo{s}{\qrole}}
\ceval \\\\
\eactor{a}{E[\raiseexn]}{\newconnsess{s}{\prole}{\rolesetr}}{\behaviour}
\parallel \zap{\sessindextwo{s}{\qrole}}

\inferrule
{ }
{ \eactor{a}{\ep[\raiseexn]}{\newconnsess{s}{\prole}{\rolesetr}}{\behaviour} \ceval \\\\
\eactor{a}{\raiseexn}{\bot}{\behaviour} \parallel \zap{\sessindextwo{s}{\prole}} }

\inferrule
{ }
{ \eactor{a}{\ep[\raiseexn]}{\bot}{M} \ceval\\\\ \eactor{a}{M}{\bot}{M} }
\end{mathpar}

\subheader{Administrative rules}
\begin{mathpar}
\inferrule
{ M \teval M' }
\eactor{a}{E[M]}{\connstate}{\behaviour} \ceval
\eactor{a}{E[M']}{\connstate}{\behaviour}

\inferrule
{ \config{C} \equiv \config{C}' \\
\config{C}' \ceval \config{D}' \\\\
\config{D}' \equiv \config{D} }
{ \config{C} \ceval \config{D} }

\inferrule
{ \config{C} \ceval \config{C}' }
{ \config{C} \parallel \config{D} \ceval \config{C}' \parallel \config{D} }

\inferrule
{ \config{C} \ceval \config{D} }
{ (\nu n) \config{C} \ceval (\nu n) \config{D}}
\end{mathpar}

\headersig{Configuration equivalence}{$\config{C} \equiv \config{D}$}
\begin{mathpar}
\config{C} \parallel \config{D} \equiv \config{D} \parallel \config{C}

\config{C} \parallel (\config{D} \parallel \config{E}) \equiv (\config{C} \parallel \config{D}) \parallel \config{E}

(\nu n_1)(\nu n_2)\config{C} \equiv (\nu n_2)(\nu n_1) \config{C}

\config{C} \parallel (\nu n)\config{D} \equiv (\nu n)(\config{C} \parallel
\config{D}) \quad \text{if } n \not\in \fn{\config{C}}

(\nu s)(\zaptwo{s}{\prole_1} \parallel \cdots \parallel \zaptwo{s}{\prole_n}) \parallel
\config{C} \equiv \config{C}

\config{C} \parallel \confzero \equiv \config{C}
\end{mathpar}

\caption{Operational semantics (3)}
\label{fig:config-reduction-3}
\end{figure}

Term reduction $$ is standard $β$-reduction, save for
\textsc{E-TryRaise} which evaluates the failure continuation in the case of an
We consider four
subcategories of configuration reduction rules: actor and adaptation rules; session
communication rules; exception handling rules; and administrative rules.

\subparagraph{Actor / adaptation rules.}
Given a
fully-evaluated actor, \textsc{E-Loop} runs the term specified by the actor's
Rule \textsc{E-New} allows actor $a$ to spawn a new actor of class $$
by creating a fresh runtime actor name $b$ and a new actor process of the form
$bMM$ where $M$ is the behaviour specified by $$,
returning the process ID $b$.
Rules \textsc{E-Replace} and \textsc{E-ReplaceSelf} handle replacement by
changing the behaviour of an actor, returning the unit value to the caller.
Rule \textsc{E-Discover} returns the process ID of an actor $b$ if it has the
desired static session type $S$.
Rule \textsc{E-Self} returns the PID of the local actor.

\subparagraph{Session communication rules.}
An actor begins a session by connecting to another actor while disconnected;
such a case is handled by rule \textsc{E-ConnInit}. Suppose we have a
disconnected actor $a$ evaluating a connection statement
$ℓ_jVb$, evaluating in parallel with a disconnected
actor $b$ evaluating an accept statement $ℓ_i(x_i) ↦M_i_i ∈I$. Rule \textsc{E-ConnInit} returns the unit value to actor $a$;
creates a fresh session name restriction $s$, sets the connection
state of $a$ to $s$ and of $b$ to
accepting actor $b$ then evaluates continuation $M_j$ with $V$
substituted for $x_j$.
Since exception handlers only scope over a single communication action, the
top-level frames $F, F'$ in each actor are discarded if the
communication succeeds.
Rule \textsc{E-Conn} handles the case where the connecting actor is already part
of a session and behaves similarly to \textsc{E-ConnInit}, without creating a
new session name restriction.
A connection can fail if an actor attempts to connect to another actor which is
terminated or is
already involved in a session; in these cases, \textsc{E-ConnFail} raises an
exception in the connecting actor.

Rule \textsc{E-Disconn} handles the case where an actor $b$ leaves a session,
synchronising with an actor $a$. In this case, the unit value is returned to
both callers, and the connection state of $b$ is set to $$.
Rule \textsc{E-Comm} handles session communication when two participants are
already connected to the same session, and is similar to \textsc{E-Conn}.
Rule \textsc{E-Complete} garbage collects a session after it has completed and
sets the initiator's connection state to $$.

\subparagraph{Exception handling rules.}
Exception handling rules allow safe session communication in
the presence of exceptions. Rule \textsc{E-CommRaise} states that if an actor is
attempting to communicate with a role no longer present due to an
exception, then an exception should be raised. We write $E[M] = $ if
$M ∈{ ℓV, ℓ_i(x_i)↦N_i_i,
, }$.
Rule \textsc{E-FailS} states that if a connected actor encounters an unhandled
exception, then a zapper thread will be generated for the current role, the
actor will become disconnected, and the current evaluation context will be
discarded. Rule \textsc{E-FailLoop} restarts an actor encountering an
unhandled exception.

\subparagraph{Administrative rules.}
The remaining rules are administrative: \textsc{E-LiftM} allows term reduction
inside an actor; \textsc{E-Equiv} allows reduction modulo structural congruence;
\textsc{E-Par} allows reduction under parallel composition; and \textsc{E-Nu}
allows reduction under name restrictions.

\subparagraph{Configuration equivalence.}
Reduction includes configuration equivalence $≡$, defined as the smallest
congruence relation satisfying the axioms in
The equivalence rules extend the usual $π$-calculus structural congruence
rules with a `garbage collection' equivalence, which allows us to
discard a session where all participants have exited due to an error.

\subsection{Metatheory}
We now turn our attention to showing that session typing allows runtime
adaptation and discovery while precluding communication mismatches and

\subsubsection{Runtime typing}
To reason about the metatheory, we introduce typing rules for
configurations~(\autoref{fig:rt-typing}): the judgement
$ΓC$ states that configuration $C$ is
well-typed under term typing environment $Γ$ and runtime typing environment

\begin{figure}[t]
\headersigarg
{Runtime Typing Rules}
\vspace{-1em}
\begin{mathpar}
\inferrule
{ \cseq{\Gamma, a : \pidty{\loctya}}{\rtenv, a : \loctya}{\config{C}} }
{ \cseq{\Gamma}{\rtenv}{(\nu a) \config{C}} }

\inferrule
\rtenv' = \{\sessindexroles{s}{\prole_i}{\rolesetq_i}{\locty_{\prole_i}}\}_{i \in I} \\
\proparg{\rtenv'} \\
s \not\in \rtenv \\
\cseq{\Gamma}{\rtenv, \rtenv'}{\config{C}} \\\\
\prop \text{ is a safety property}
{ \cseq{\Gamma}{\rtenv}{(\nu s) \config{C}} }

\inferrule
{ \cseq{\Gamma}{\rtenv_1}{\config{C}} \\ \cseq{\Gamma}{\rtenv_2}{\config{D}} }
{ \cseq{\Gamma}{\rtenv_1, \rtenv_2}{\config{C} \parallel \config{D} } }

\inferrule
{ }
{ \cseq{\Gamma}{\sessindexroles{s}{\prole}{\rolesetq}{S}}{\zap{\sessindextwo{s}{\prole}}} }

\inferrule
{ }
{ \cseq{\Gamma}{\cdot}{\confzero} }

\inferrule
\loctyb = \loctya \vee \loctyb = \localend \\
a : \pidty{\loctya} \in \Gamma \\\\
\tseq[\loctya]{\Gamma}{\loctyb}{M}{A}{\localend} \\
\bseq[\loctya]{\Gamma}{\behaviour}
{ \cseq{\Gamma}{a : \loctya}{\eactor{a}{M}{\bot}{\behaviour}} }

\inferrule
a : \pidty{\loctyb} \in \Gamma \\\\
\tseq{\Gamma}{\loctya}{M}{A}{\localend} \\
\bseq{\Gamma}{\behaviour}
{ \cseq{\Gamma}{a : \loctyb, \sessindexroles{s}{\prole}{\rolesetq}{\locty}}{
\eactor{a}{M}{\newconnsess{s}{\prole}{\rolesetq}}{\behaviour}}
\end{mathpar}
\caption{Runtime typing rules}
\label{fig:rt-typing}
\end{figure}

Rule \textsc{T-Pid} types actor name restriction $(νa)C$
by adding a PID into the term
environment, and extending the runtime typing environment $a:S$; the linearity
of the runtime typing environment therefore means that the system must contain precisely
one actor with name $a$.

Session name restrictions $(νs)C$ are typed by
\textsc{T-Session}.
We follow the formulation of~Scalas and Yoshida, 2019 which types multiparty
sessions using a parametric safety property $φ$; we discuss safety
properties in more depth in Section~\ref{sec:formalism:preservation}.
Let $'$ be a
runtime typing environment containing only mappings of the form
$s_i_iS_i$. Assuming $$ does not contain any mappings
involving session $s$ and $'$ satisfies $φ$, the rule states that $C$ is typable under typing environment $Γ$ and runtime typing environment $, '$.
It is sometimes convenient to annotate session $ν$-binders with their
environment, e.g., $(νs : ') C$.

Rule \textsc{T-Par} types each subconfiguration of a parallel composition by
splitting the linear runtime environment. Rule \textsc{T-Zap} types a zapper
thread $s$, assuming the runtime environment
contains an entry $s$ for any session type

Finally, rules \textsc{T-DisconnectedActor} and \textsc{T-ConnectedActor} type
disconnected and connected actor configurations respectively.
Given an actor with name $a$ and static session type $$, both rules require that
the typing environment contains $a : $ and
runtime environment contains $a : $.
Both rules require that the current session type is fully consumed by the
currently-evaluating term and that the actor's behaviour should be typable under
Rule \textsc{T-DisconnectedActor} requires that the currently-evaluating term
must be typable under either $$ or $$, whereas to type a
connection state of $s$ and current session type
$$, \textsc{T-ConnectedActor} requires an entry
$s$ in the runtime environment.

\subsubsection{Preservation}\label{sec:formalism:preservation}
We now prove that reduction preserves typability and thus that actors only
perform communication actions specified in their session types.  Due to our use
of explicit connection actions, classical MPST approaches are too limited for
our purposes.  Our approach, following that of~Scalas and Yoshida, 2019, is to
introduce a labelled transition system (LTS) on local types, and specify a
generic safety property based around local type reduction. The property can then
refined; in our case, we will later specialise the property in order to prove

\begin{figure}[t]
\header{Labels}
\[
\begin{array}{lrcl}
\text{Labels} & \ltslbl & ::= & \ltscomm{s}{\prole}{\qrole}{\ell}{A} \midspace
\ltsconnpair{s}{\prole}{\qrole}{\ell} \midspace
\ltsdisconnact{s}{\prole}{\qrole} \\
\text{Synchronisation labels} & \synclbl & ::= &
\ltspair{s}{\prole}{\qrole}{\ell} \midspace
\ltsconnpair{s}{\prole}{\qrole}{\ell} \midspace
\ltsdisconnpair{s}{\prole}{\qrole}
\end{array}
\]

\header{Reduction on runtime typing environments}

\subheadersig{Local Reduction}{$\Delta \annarrow{\ltslbl} \Delta'$}
\begin{mathpar}
\inferrule
{ \exists j \in I . \locact_j = \localtyconn{\qrole}{\ell_j}{\tya_j} \\\\
\ty{\qrole} = \sumact{k \in K}{\localtyaccept{\prole}{\ell_k}{\tyb_k} \then \loctyb_k} \\
j \in K \\
\tya_j = \tyb_j
\sessindexroles{s}{\prole}{\rolesetr}{\sumact{i \in I}{\locact_i \then \loctya_i}}
\annarrow{\ltsconnpair{s}{\prole}{\qrole}{\ell_j}}
\sessindexroles{s}{\prole}{\rolesetr, \qrole}{\locty_j},
\sessindexroles{s}{\qrole}{\prole}{\loctyb_j}

\inferrule
{ \exists j \in I . \locact_j = \localcomm{\qrole}{\ell_j}{\tya_j} \\
\qrole \in \rolesetr
{ \sessindexroles{s}{\prole}{\rolesetr}{\sumact{i \in I}{\locact_i \then \locty_i}}
\annarrow{\ltscomm{s}{\prole}{\qrole}{\ell_j}{\tya_j}}
\sessindexroles{s}{\prole}{\rolesetr}{\locty_j}

\inferrule
{ }
{ \sessindexroles{s}{\prole}{\rolesetr, \qrole}{\localtywait{\qrole} \then S} \annarrow{\ltswait{s}{\prole}{\qrole}}
\sessindexroles{s}{\prole}{\rolesetr}{S}

\inferrule
{ }
{ \sessindexroles{s}{\prole}{\qrole}{\localtydisconn{\qrole}}
\annarrow{\ltsdisconn{s}{\prole}{\qrole}} \cdot } \\

\inferrule
{ \rtenv, \sessindexroles{s}{\prole}{\rolesetq}{\locty \{ \recty{X}{\locty} / X \}} \annarrow{\ltslbl} \rtenv' }
{ \rtenv, \sessindexroles{s}{\prole}{\rolesetq}{\recty{X}{\locty}} \annarrow{\ltslbl} \rtenv' }

\inferrule
{ \rtenv \annarrow{\ltslbl} \rtenv' }
{ \rtenv, \sessindexroles{s}{\prole}{\rolesetq}{\locty} \annarrow{\ltslbl} \rtenv', \sessindexroles{s}{\prole}{\rolesetq}{\locty} }

\inferrule
{ \rtenv \annarrow{\ltslbl} \rtenv' }
{ \rtenv, a {:} \loctya \annarrow{\ltslbl} \rtenv', a {:} \loctya }

\end{mathpar}

\subheadersig{Synchronisation}{$\Delta \syncannarrow{\synclbl} \Delta'$}
\begin{mathpar}
\inferrule
\rtenv \annarrow{\ltsconnpair{s}{\prole}{\qrole}{\ell}} \rtenv'
{ \rtenv \syncannarrow{\ltsconnpair{s}{\prole}{\qrole}{\ell}} \rtenv' }

\inferrule
{ \rtenv_1 \annarrow{\ltscomm[{!}]{s}{\prole}{\qrole}{\ell}{\tya}} \rtenv'_1
\\
\rtenv_2 \annarrow{\ltscomm[{?}]{s}{\qrole}{\prole}{\ell}{\tya}} \rtenv'_2 }
{ \rtenv_1, \rtenv_2 \syncannarrow{\ltspair{s}{\prole}{\qrole}{\ell}} \rtenv'_1, \rtenv'_2 }

\inferrule
{ \rtenv_1 \annarrow{\ltswait{s}{\prole}{\qrole}} \rtenv'_1 \\
\rtenv_2 \annarrow{\ltsdisconn{s}{\qrole}{\prole}} \rtenv'_2 }
{ \rtenv_1, \rtenv_2 \syncannarrow{\ltsdisconnpair{s}{\prole}{\qrole}} \rtenv'_1, \rtenv'_2 }
\end{mathpar}
\caption{Labelled transition system for runtime typing environments}
\label{fig:rt-lts-reduction}
\end{figure}

\subparagraph{Reduction on runtime typing environments.}
Figure~\ref{fig:rt-lts-reduction} shows the LTS on runtime typing environments.
There are two judgements: $ '$, which handles
reduction of individual local types, and a \emph{synchronisation} judgement
$ '$.

Rule \textsc{ET-Conn} handles the reduction of role $$,
where the choice session type contains a connection action
If $$ has a statically-defined session type $k ∈Kℓ_kB_k _k$
which can accept $ℓ_j$ from from $$, and the
payload types match, reduction
advances $$'s session type,
adds $$ to $$'s connected role set,
and introduces an entry for $$ into the
environment. The reduction emits a label

Given a role $$ connected to $$ with a session choice containing a
send or receive action $ℓ_jA '_j$,
rule \textsc{ET-Act} will
emit a label $sℓ_jA_j$ and advance the session
type of $$.

Rule \textsc{ET-Wait} handles the reduction of $$ actions, $s,
$, where $$ waits for $$ to
disconnect: the reduction emits label $[]$
and removes $$ from $$'s connected roles. Similarly,
rule \textsc{ET-Disconn} handles disconnection, by emitting label
$[]$ and removing the entry from the
\textsc{ET-Rec} handles recursive types, and the \textsc{ET-Cong} rules
handle reduction of sub-environments.

Rule \textsc{ET-ConnSync} states that connection is a synchronisation action,
and rules \textsc{ET-Comm} and \textsc{ET-Disconn} handle synchronisation
between dual actions in sub-environments, emitting synchronisation labels
$sℓ$ and $s$
respectively. We omit the congruence rules for synchronisation actions.
We say that a runtime environment \emph{reduces}, written $$, if
there exists some $'$ such that $'$.

\subparagraph{Safety.}
A \emph{safety property} describes a set of invariants on typing environments
which allow us to prove preservation. Since the type system is parametric
in the given safety property, we can tweak the property to permit or rule out
different typing environments satisfying particular behavioural properties;
however, we need only prove type preservation once, using the weakest safety
property. Our safety property is different to the safety property described
by~Scalas and Yoshida, 2019 in order to account for explicit connection actions.

\raggedright
\begin{definition}[Safety Property]\label{def:safety}
$\prop$ is a \emph{safety property} of runtime typing contexts $\rtenv$ if:
\begin{enumerate}
\item $\proparg{\rtenv, \sessindexroles{s}{\prole}{\rolesetr}{\sumact{i \in I}{\locacta_i \then
\loctya_i}}, \sessindexroles{s}{\qrole}{\rolesets}{\sumact{j \in J}{
\localtyrecv{\prole}{\ell_j}{\tyb_j} \then \loctyb_j}}}$ implies that if
$\localtycomm{\qrole}{{!}}{\ell_k}{\tya_k} \in \{ \locact_i \}_{i \in I}$,
then $k \in J$, $\qrole \in \rolesetr$, $\prole \in \rolesets$, and $\tya_k = \tyb_k$.
\item $\proparg{\rtenv, \sessindexroles{s}{\prole}{\rolesetr}{\sumact{i \in I}{\locact_i \then
\locty_i}}}$ implies that
if $\locact_i = \localtyconn{\qrole}{\ell_j}{\tya_j} \in \{ \locact_i
\}_{i \in I}$,
then $\qrole \not\in \rolesetr$,
$\sessindexrolesnoty{s}{\qrole}{\rolesets} \not\in \dom{\rtenv}$, and
$\ty{\qrole} = \sumact{k \in K}{\localtyaccept{\prole}{\ell_k}{\tyb_k} \then \loctyb_k}$
with $j \in K$ and $\tya_j = \tyb_j$.
\item $\proparg{\rtenv, \sessindexroles{s}{\prole}{\rolesetq}{\recty{X}{S}}}$ implies
$\proparg{\rtenv, \sessindexroles{s}{\prole}{\rolesetq}{S \{ \recty{X}{S} / X \}}}$
\item $\proparg{\rtenv}$ and $\rtenv \synceval \rtenv'$ implies $\proparg{\rtenv'}$
\end{enumerate}

A runtime typing environment is \emph{safe}, written
$\safe{\rtenv}$, if $\proparg{\rtenv}$ for a safety property $\prop$.
\end{definition}
Clause (1) ensures that communication actions between participants are
compatible: if $$ is sending a message with label $ℓ$ and payload type
$$ to $$, and $$ is receiving from $$,
then the two roles must be connected,
and $$ must be able to receive $ℓ$ with a matching payload.

Clause (2) states that if $$ is connecting to a role $$ with label
$ℓ$, then
$$ should not already be involved in the session, and should be able to
accept from $$ on message label $ℓ$ with a compatible payload type.
The requirement that $$ is not already involved in the session rules
out the \emph{correlation} errors described in
Clause (3) handles recursion, and clause (4) requires that
safety is preserved under environment reduction.

\subparagraph{Concretising the safety property.}
In order to deduce that a runtime typing environment $$ is safe, we define
$ = { ' ' }$
and verify that $$ is a safety property by ensuring that it satisfies all
clauses in~\autoref{def:safety}.

\subparagraph{Properties on protocols and programs.}
It is useful to distinguish active and inactive session types, depending on
whether their associated role is currently involved in a session, and identify
the initiator of a session.

\begin{definition}[Active and Inactive Session Types]
A session type $S$ is \emph{inactive}, written $\tyinactive{S}$, if $S =
\localend$ or $S = \sumact{i \in I}{\localtyaccept{\prole}{\ell_i}{\tya_i} \then {\loctya_i}}$. Otherwise, $S$ is \emph{active}, written $\tyactive{S}$.
\end{definition}

\begin{definition}[Initiator, unique initiator]
Given a protocol $\proto$, a role $\prole : \loctya_\prole \in \proto$ is an \emph{initiator} if
$S_\prole = \sumact{i \in I}{ \locact_i \then \loctya_i }$, and each $\locact_i$ is a connection action
Role $\prole$ is a \emph{unique initiator} of $\proto$ if
$\tyinactive{\loctya_{\qrole}}$ for all
$\qrole \in \proto \setminus \{ \prole : \loctya_{\prole} \} $.
\end{definition}

A protocol is \emph{well-formed} if it is safe and has a unique initiator.

\begin{definition}[Well-formed protocol]
A protocol $P = \{ \prole_i : \loctya_i \}_{i \in I}$ is \emph{well-formed}
if it has a unique initiator $\qrole$ of type $\loctya$ and
$\safe{ \sessindexroles{s}{\qrole}{\emptyset}{\loctya} }$ for any $s$.
\end{definition}

By way of example, the online shopping protocol is well-formed: \role{Customer}
is the protocol's unique initiator, and it is straightforward to verify that
$ sCustomer∅ Customer $.

\begin{definition}[Well-formed program]
A program $(\seq{D}, \seq{P}, M)$ is \emph{well-formed} if:
\begin{enumerate}
\item For each actor definition $D = \actordef{u}{\loctya}{N} \in \seq{D}$,
there exists some role $\prole \in \seq{P}$ such that $\ty{\prole}
= \loctya$, and
\item Each protocol $P \in \seq{P}$ is well-formed and has a distinct set of
\item The `boot clause' $M$ is typable under the empty typing environment
and does not perform any communication actions:
\end{enumerate}
\end{definition}
When discussing the metatheory, we only consider configurations defined with
respect to a well-formed program. Specifically, we henceforth assume that each
actor definition in the system follows a session type matched by a role in a
given protocol, assume each role belongs to a single protocol, and assume that
all protocols are well-formed.

Given a safe runtime environment, configuration reduction preserves typability;
details can be found in Appendix~\ref{appendix:proofs}.
We write $ℛ^?$ for the reflexive closure of a relation $ℛ$.

\begin{restatable}[Preservation (Configurations)]{theorem}{configpres}\label{thm:configpres}
Suppose $\cseq{\Gamma}{\rtenv}{\config{C}}$ with $\safe{\rtenv}$ and where
$\config{C}$ is defined wrt.\ a well-formed program.
If $\config{C} \ceval \config{C}'$, then there exists some $\rtenv'$ such that $\rtenv \maybesynceval
\rtenv'$ and $\cseq{\Gamma}{\rtenv'}{\config{C}'}$.
\end{restatable}

Preservation shows that each actor conforms to its session type, and that
communication never introduces unsoundness due to mismatching payload types.

\subsubsection{Progress}\label{sec:formalism:progress}
We now show a progress property, which shows that given
\emph{protocols} which satisfy a progress property, \EnsembleS
\emph{configurations} do not get stuck due to deadlocks.

A \emph{final} runtime typing environment contains a single, disconnected role
of type $$, reflecting the intuition that all roles will eventually
disconnect from a protocol initiator.

\begin{definition}[Final environment]
An environment $\rtenv$ is \emph{final}, written $\finished{\rtenv}$,
$\rtenv = \{
\sessindexroles{s}{\prole}{\emptyset}{\localend} \}$ for some $s$ and
\end{definition}

So far, we have considered \emph{safe} protocols, which ensure the absence of
communication mismatches. We say that an environment \emph{satisfies progress}
if each active role can eventually perform an action, each potential send is
eventually matched by a receive, and non-reducing environments are final.
Let $$ denote the roles referenced in a
synchronisation label (i.e., $ = { , } $ for
$∈{ sℓ,
s }$).

\begin{definition}[Progress (Runtime typing
A runtime typing environment $\rtenv$ \emph{satisfies progress}, written
$\prog{\rtenv}$, if:
\begin{itemize}
\item \textit{(Role progress)} for each $\sessindexroles{s}{\prole_i}{\rolesetq_i}{\loctya_i} \in
\rtenv$ s.t.\ $\tyactive{\loctya_i}$, $\rtenv
\synceval^* \rtenv' \syncannarrow{\synclbl}$ with $\prole \in \roles{\synclbl}$
\item \textit{(Eventual comm.)}
if $\rtenv \!\syncevalstar\! \rtenv' \!\annarrow{\ltscomm[{!}]{s}{\prole}{\qrole}{\ell}{A}}$,
then $\rtenv' \syncannarrow{\seq{\synclbl}} \rtenv''
\annarrow{\ltscomm[{?}]{s}{\qrole}{\prole}{\ell}{A}}$,
with $\prole \not\in \roles{\seq{\synclbl}}$
\item \textit{(Correct termination)} $\rtenv \syncevalstar
\rtenv' \not\synceval$ implies $\finished{\rtenv}$
\end{itemize}
\end{definition}

The online shopping example satisfies progress, since all roles will always
eventually be able to fire an action once connected, and since all roles
disconnect, the non-reducing final environment will be of the form

\begin{definition}[Progress (Programs)]
A well-formed program $(\seq{D}, \seq{P}, M)$ \emph{satisfies progress}
if each $P \in \seq{P}$ has a unique initiator $\qrole$ of type $\loctya$ and
$\prog{ \sessindexroles{s}{\qrole}{\emptyset}{\loctya} }$ for any $s$.
\end{definition}

It is useful to define a \emph{configuration context} $G$ as
the one-hole context $G ::=  [ ] (νs)G G
A \emph{session} consists of a session name restriction and all connected actors
and zapper threads.  Each well-typed configuration can be written as a sequence
of sessions, followed by all disconnected actors.

\begin{definition}[Session]
A configuration is a \emph{session} $\sgroup$ if it can be written:\\
(\nu s)(\eactor{a_1}{M_1}{\newconnsess{s}{\prole_1}{\rolesetq_1}}{\behaviour_1}
\parallel \cdots \parallel
\eactor{a_m}{M_m}{\newconnsess{s}{\prole_m}{\rolesetq_m}}{\behaviour_m}
\parallel
\zap{\sessindextwo{s}{\prole_{m + 1}}}
\parallel \cdots
\parallel
\zap{\sessindextwo{s}{\prole_{n}}}
\end{definition}

An actor is \emph{terminated} if it has reduced to a value or has an unhandled
exception, and has the behaviour $$.  An unmatched discover occurs when no
other actors match a given session type.  An actor is \emph{accepting} if it is
ready to accept a connection.

\begin{definition}[Terminated actor, unmatched discover, accepting actor]\hfill
\begin{itemize}
\item An actor $\eactor{a}{M}{\connstate}{\behaviour}$ is \emph{terminated}
if $M = \effreturn{V}$ or $M = \ep[\raiseexn]$, and $\behaviour = \bstop$.
\item An actor $\eactor{a}{E[\newdiscover{S}]}{\connstate}{\behaviour}$ which is a subconfiguration
of $\config{C}$ has an \emph{unmatched discover} if no other
non-terminated actor in
$\config{C}$ has session type $S$.
\item An actor $\eactor{a}{M}{\connstate}{\behaviour}$
is \emph{accepting} if $M =
E[\newaccept{\prole}{\msg{\ell_j}{x_j} \mapsto N_j}_j]$ for
some evaluation context $E$ and role $\prole$.
\end{itemize}
\end{definition}

Unhandled exceptions will propagate through a session, progressively cancelling
all roles. A \emph{failed session} consists of only zapper threads.

\begin{definition}[Failed session]
We say that a session $\sgroup$ is a \emph{failed session}, written
$\failed{\sgroup}$, if
$\sgroup \equiv (\nu s)(\zaptwo{s}{\prole_1} \parallel \cdots \parallel \zaptwo{s}{\prole_n})$.
\end{definition}

The key \emph{session progress} lemma establishes the reducibility of each session which does not
contain an unmatched discover and is typable under a reducible runtime typing

\begin{restatable}[Session Progress]{lemma}{sessgroupprogress}\label{lem:sess-group-progress}
If $\cseq{\cdot}{\cdot}{\config{C}}$ where $\config{C}$ does not contain an
unmatched discover, $\config{C} \equiv
\config{G}[\sgroup]$ and $\sgroup = (\nu s: \rtenv) \config{D}$ with
$\prog{\rtenv}$, and $\sgroup$ is not a failed session, then $\config{C} \ceval$.
\end{restatable}

There are several steps to proving Lemma~\ref{lem:sess-group-progress}.
we introduce \emph{exception-aware} reduction on runtime typing environments,
which explicitly accounts for zapper threads at the type level, and show that
exception-aware environments threads retain safety and progress. Second, we
introduce \emph{flattenings}, which show that runtime typing
environments containing only unary output choices can type configurations
blocked on communication actions, and that flattenings preserve environment
reducibility. Finally, we show that configurations typable under flat,
reducible typing environments can reduce. Full details can be found in

We can now show our second main result: in the absence of unmatched discovers,
a configuration can either reduce, or it consists only of accepting and
terminating actors.

\begin{restatable}[Progress]{theorem}{progress}\label{thm:progress}
Suppose $\cseq{\cdot}{\cdot}{\config{C}}$ where $\config{C}$ is defined
wrt.\ a well-formed program which satisfies progress, and $\prog{\rtenv}$ for
each $(\nu s : \rtenv) \config{C}'$ in $\config{C}$.
If $\config{C}$ does not contain an unmatched discover,
$\exists \config{D}$ such that $\config{C}
\ceval \config{D}$, or
$\config{C} \equiv \confzero$, or
$\config{C} \equiv (\nu b_1 \cdots \nu b_n)(\eactor{b_1}{N_1}{\bot}{\behaviour_1} \parallel \cdots \parallel
\eactor{b_n}{N_n}{\bot}{\behaviour_n})$
where each $b_i$ is terminated or accepting.
\end{restatable}

The proof eliminates all failed sessions by the structural congruence
rules; shows that the presence of sessions implies reducibility
(Lem.~\ref{lem:sess-group-progress}); and reasons about disconnected actors.

In addition to each
actor conforming to its session type~(\autoref{thm:configpres}),
Theorem~\ref{thm:progress} guarantees that the system does not deadlock. It
follows that session types ensure safe communication.

Theorem~\ref{thm:progress} assumes the absence of unmatched discovers. This is not a
significant limitation in practice, however, as unmatched discovers can be mitigated with
timeouts, where a timeout would trigger an exception.

\section{Related Work}
\label{sec:related}

\subparagraph{Behavioural typing for actors.}
Mostrous and Vasconcelos, 2011 present the first theoretical account of session types in an actor
language; their work effectively overlays a channel-based session
typing discipline on mailboxes using Erlang's
reference generation capabilities.

Neykova and Yoshida, 2017 use MPSTs to specify
communication in an actor system, implemented in Python.
Fowler~[Fowler, 2016] implements similar ideas in Erlang,
with extensions to allow subsessions~[Demangeon and Honda, 2012] and failure handling.
Neykova and Yoshida, 2017 later improve the recovery
mechanism of Erlang by using MPSTs to calculate a minimal set of affected roles.
The above works check multiparty session typing dynamically. We are first to
both formalise and implement static multiparty session type checking for an
actor language.

Active objects (AOs)~[de~Boer et~al., 2007] are actor-like concurrent objects
where results of asynchronous method invocations are returned through futures.
Bagherzadeh and Rajan, 2017 study \emph{order types} for an AO calculus, which
characterise causality and statically rule out data races. In contrast to MPSTs,
order types work bottom-up through type inference.
Kamburjan et~al., 2016 apply an MPST-like system to Core ABS~[Johnsen et~al., 2010],
a core AO calculus;
they establish soundness via a translation to register automata rather than via an operational semantics.

de'Liguoro and Padovani, 2018 introduce \emph{mailbox types}, a type system for
first-class, unordered mailboxes. Their calculus generalises the actor
model, since each process can be associated with more than one mailbox.
Their type discipline allows multiple writers and a single reader for each
mailbox, and ensures conformance, deadlock-freedom, and for many programs,
junk-freedom. Our approach is based on MPSTs and is more

\subparagraph{Non-classical multiparty session types.}
MPSTs were introduced
by~Honda et~al., 2008.
\emph{Classical} MPST theories are grounded in binary duality: safety follows as
a consequence of \emph{consistency} (pointwise binary duality of interactions
between participants), and deadlock-freedom follows from projectability from a
global type.

Unfortunately, classical MPSTs are restrictive: there are many protocols which
are intuitively safe but not consistent. Scalas and Yoshida, 2019 introduced the first
\emph{non-classical} multiparty session
calculus. Instead of ensuring safety using binary duality, they define
an LTS on local types and \emph{safety property} suitable for proving type
preservation; since the type system is \emph{parametric} in the safety property
(inspired by~Igarashi and Kobayashi, 2004 in the $π$-calculus), the property can be
customised in order to guarantee different properties such as deadlock-freedom
or liveness.
Hu and Yoshida, 2017 formalise MPSTs with explicit connection actions via an LTS on
types rather than providing a concrete language design or calculus; in our
setting, a calculus is vital in order to account for the impact of adaptation
constructs. A key contribution of our work is the use of non-classical MPSTs to
prove preservation and progress properties for a calculus incorporating MPSTs
with explicit connection actions.

\subparagraph{Adaptation.}
None of the above work considers adaptation. The literature on formal studies of
adaptation is mainly based on process calculi, without programming language
design or implementation. Bravetti \emph{et al.} [Bravetti et~al., 2012] develop a
process calculus that allows parts of a process to be dynamically replaced with
new definitions. Their later work [Bravetti et~al., 2012] uses temporal logic
rather than types to verify adaptive processes. Di Giusto and P\'{e}rez
[Di Giusto} and P{\'{e}}rez, 2015] define a session type system for the same process calculus,
and prove that adaptation does not disrupt active sessions.
Later,~Di Giusto} and P{\'{e}}rez, 2015 use an event-based approach so that adaptation
can depend on the state of a session protocol.
Anderson and Rathke [Anderson and Rathke, 2012] develop an MPST-like calculus and study
dynamic software update providing guarantees of communication safety and
liveness. Differently from our work, they do not consider runtime discovery of
software components and do not provide an implementation.

Coppo \emph{et al.} [Coppo et~al., 2015] consider self-adaptation, in which a system
reconfigures itself rather than receiving external updates.
They define an MPST calculus with self-adaptation
and prove type safety. Castellani \emph{et al.} [Castellani et~al., 2016] extend
[Coppo et~al., 2015] to also guarantee properties of secure information flow,
but neither of these works have been implemented.
Dalla Preda \emph{et al.} [Preda et~al., 2017] develop the AIOCJ system based on
choreographic programming for runtime updates. Their work is implemented in the
Jolie language~[Montesi et~al., 2007], but they do not consider runtime discovery.

In this work we focus on correct communication in the absence of adversaries, and do not consider security. The literature on security and behavioural types is surveyed by Bartoletti \emph{et al.} [Bartoletti et~al., 2015] and could provide a basis for future work on security properties.

\section{Conclusion and Future Work}
\label{sec:future-conc}

Modern computing increasingly requires software components to \emph{adapt} to
their environment, by \emph{discovering}, \emph{replacing}, and
\emph{communicating} with other components which may not be part of the
system's original design. Unfortunately, up until now, existing programming
languages have lacked the ability to support adaptation both
\emph{safely} and \emph{statically}.
We therefore asked:
\begin{quote}
\textit{Can a programming language support static (compile-time) verification of safe runtime
dynamic self-adaptation, i.e., discovery, replacement and communication?}
\end{quote}

We have answered this question in the affirmative by introducing \EnsembleS, an
actor-based language supporting adaptation, which uses multiparty session types
to guarantee communication safety, using explicit connection
actions to invite discovered actors into a session.
We have demonstrated the safety of our system by proving  type soundness
theorems which state that each actor follows its session type, and that
communication does not introduce deadlocks. Our formalism makes essential use of
\emph{non-classical} MPSTs.

\subparagraph{Future work.}

Currently, in both the theory and implementation, each actor only takes part in
a single session. Unlike dynamically-checked implementations of session typing
for actors~[Neykova and Yoshida, 2014, Fowler, 2016], this means that a message received by an actor in one
session cannot trigger an interaction in another (e.g., the Warehouse example
in~[Neykova and Yoshida, 2014]).
A key focus for future work will be to allow actors to partake in multiple sessions.

Currently, \EnsembleS discovery and replacement requires type equality.  We
envisage that we could relax this constraint to subtyping~[Scalas et~al., 2017] or
perhaps bisimilarity on local types to increase expressiveness.

In order to avoid session correlation errors, we require that each role includes
at most a single top-level $accept$ construct (c.f.~[Hu and Yoshida, 2017]). It
would be interesting to investigate the more general setting, which would likely
require dependent types.

\begin{thebibliography}{57}
\providecommand{\natexlab}[1]{#1}
\providecommand{\url}[1]{\texttt{#1}}
\expandafter\ifx\csname urlstyle\endcsname\relax
\providecommand{\doi}[1]{doi: #1}\else
\providecommand{\doi}{doi: \begingroup \urlstyle{rm}\Url}\fi

[Agha, 1990]
Gul~A. Agha.
\newblock \emph{{ACTORS} - a model of concurrent computation in distributed
\newblock {MIT} Press series in artificial intelligence. {MIT} Press, 1990.

[Anderson and Rathke, 2012]
Gabrielle Anderson and Julian Rathke.
\newblock Dynamic software update for message passing programs.
\newblock In Ranjit Jhala and Atsushi Igarashi, editors, \emph{Programming
Languages and Systems - 10th Asian Symposium, {APLAS} 2012, Kyoto, Japan,
December 11-13, 2012. Proceedings}, volume 7705 of \emph{Lecture Notes in
Computer Science}, pages 207--222. Springer, 2012.
\newblock ISBN 978-3-642-35181-5.
\newblock \doi{10.1007/978-3-642-35182-2\_15}.
\newblock URL \url{https://doi.org/10.1007/978-3-642-35182-2\_15}.

[Atkey, 2009]
Robert Atkey.
\newblock Parameterised notions of computation.
\newblock \emph{Journal of Functional Programming}, 19\penalty0 (3-4):\penalty0
335--376, 2009.

[Bagherzadeh and Rajan, 2017]
Mehdi Bagherzadeh and Hridesh Rajan.
\newblock Order types: static reasoning about message races in asynchronous
message passing concurrency.
\newblock In \emph{AGERE!@SPLASH}, pages 21--30. {ACM}, 2017.

[Bartoletti et~al., 2015]
Massimo Bartoletti, Ilaria Castellani, Pierre{-}Malo Deni{\'{e}}lou,
Mariangiola Dezani{-}Ciancaglini, Silvia Ghilezan, Jovanka Pantovic, Jorge~A.
P{\'{e}}rez, Peter Thiemann, Bernardo Toninho, and Hugo~Torres Vieira.
\newblock Combining behavioural types with security analysis.
\newblock \emph{Journal of Logical and Algebraic Methods in Programming},
84\penalty0 (6):\penalty0 763--780, 2015.
\newblock \doi{10.1016/j.jlamp.2015.09.003}.
\newblock URL \url{https://doi.org/10.1016/j.jlamp.2015.09.003}.

[Baumann et~al., 1999]
J.~Baumann, F.~Hohl, K.~Rothermel, and M.~Stra\ss{}er.
\newblock \emph{MOLE — Concepts of Mobile Agent System}, page 535–554.
\newblock ACM Press/Addison-Wesley Publishing Co., USA, 1999.
\newblock ISBN 0201379287.

[Bouabene} et~al., 2010]
G.~{Bouabene}, C.~{Jelger}, C.~{Tschudin}, S.~{Schmid}, A.~{Keller}, and
\newblock The autonomic network architecture ({ANA}).
\newblock \emph{IEEE Journal on Selected Areas in Communications}, 28\penalty0
(1):\penalty0 4--14, 2010.
\newblock \doi{10.1109/JSAC.2010.100102}.

[Bravetti et~al., 2012]
Mario Bravetti, Cinzia {Di Giusto}, Jorge~A. P{\'{e}}rez, and Gianluigi
\newblock Towards the verification of adaptable processes.
\newblock In \emph{Proceedings (Part {I}) of the 5th International Symposium on
Leveraging Applications of Formal Methods, Verification and Validation
(ISoLA)}, volume 7609 of \emph{Lecture Notes in Computer Science}, pages
269--283. Springer, 2012{\natexlab{a}}.
\newblock \doi{10.1007/978-3-642-34026-0_20}.
\newblock URL \url{https://doi.org/10.1007/978-3-642-34026-0_20}.

[Bravetti et~al., 2012]
Mario Bravetti, Cinzia {Di Giusto}, Jorge~A. P{\'{e}}rez, and Gianluigi
\newblock Adaptable processes.
\newblock \emph{Logical Methods in Computer Science}, 8\penalty0 (4),
\newblock \doi{10.2168/LMCS-8(4:13)2012}.
\newblock URL \url{https://doi.org/10.2168/LMCS-8(4:13)2012}.

[Cameron et~al., 2013]
Callum Cameron, Paul Harvey, and Joseph Sventek.
\newblock A virtual machine for the {Insense} language.
\newblock In \emph{Proceedings of the International Conference on Mobile
Wireless Middleware, Operating Systems and Applications (Mobilware)}, pages
1--10. IEEE, 2013.
\newblock \doi{10.1109/Mobilware.2013.17}.

[Castellani et~al., 2016]
Ilaria Castellani, Mariangiola Dezani{-}Ciancaglini, and Jorge~A. P{\'{e}}rez.
\newblock Self-adaptation and secure information flow in multiparty
\newblock \emph{Formal Aspects of Computing}, 28\penalty0 (4):\penalty0
669--696, 2016.
\newblock \doi{10.1007/s00165-016-0381-3}.
\newblock URL \url{https://doi.org/10.1007/s00165-016-0381-3}.

[Cesarini and Vinoski, 2016]
Francesco Cesarini and Steve Vinoski.
\newblock \emph{Designing for Scalability with Erlang/OTP: Implement Robust,
Fault-Tolerant Systems}.
\newblock O'Reilly Media, Inc., 1st edition, 2016.
\newblock ISBN 1449320732.

[Coppo et~al., 2015]
Mario Coppo, Mariangiola Dezani{-}Ciancaglini, and Betti Venneri.
\newblock Self-adaptive multiparty sessions.
\newblock \emph{Service Oriented Computing and Applications}, 9\penalty0
(3-4):\penalty0 249--268, 2015.
\newblock \doi{10.1007/s11761-014-0171-9}.
\newblock URL \url{https://doi.org/10.1007/s11761-014-0171-9}.

[Coppo et~al., 2016]
Mario Coppo, Mariangiola Dezani{-}Ciancaglini, Nobuko Yoshida, and Luca
\newblock Global progress for dynamically interleaved multiparty sessions.
\newblock \emph{Mathematical Structures in Computer Science}, 26\penalty0
(2):\penalty0 238--302, 2016.

[de~Boer et~al., 2007]
Frank~S. de~Boer, Dave Clarke, and Einar~Broch Johnsen.
\newblock A complete guide to the future.
\newblock In \emph{{ESOP}}, volume 4421 of \emph{Lecture Notes in Computer
Science}, pages 316--330. Springer, 2007.

[de'Liguoro and Padovani, 2018]
Ugo de'Liguoro and Luca Padovani.
\newblock Mailbox types for unordered interactions.
\newblock In \emph{{ECOOP}}, volume 109 of \emph{LIPIcs}, pages 15:1--15:28.
Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik, 2018.

[Demangeon and Honda, 2012]
Romain Demangeon and Kohei Honda.
\newblock Nested protocols in session types.
\newblock In \emph{{CONCUR}}, volume 7454 of \emph{Lecture Notes in Computer
Science}, pages 272--286. Springer, 2012.

[Di Giusto} and P{\'{e}}rez, 2015]
Cinzia {Di Giusto} and Jorge~A. P{\'{e}}rez.
\newblock An event-based approach to runtime adaptation in
communication-centric systems.
\newblock In \emph{Proceedings of the 11th and 12th International Workshops on
Web Services, Formal Methods and Behavioural Types (WS-FM 2014, WS-FM/BEAT
2015)}, Lecture Notes in Computer Science, pages 67--85. Springer,
\newblock \doi{10.1007/978-3-319-33612-1_5}.
\newblock URL \url{https://doi.org/10.1007/978-3-319-33612-1_5}.

[Di Giusto} and P{\'{e}}rez, 2015]
Cinzia {Di Giusto} and Jorge~A. P{\'{e}}rez.
\newblock Disciplined structured communications with disciplined runtime
\newblock \emph{Science of Computer Programming}, 97:\penalty0 235--265,
\newblock \doi{10.1016/j.scico.2014.04.017}.
\newblock URL \url{https://doi.org/10.1016/j.scico.2014.04.017}.

[Flanagan et~al., 1993]
Cormac Flanagan, Amr Sabry, Bruce~F. Duba, and Matthias Felleisen.
\newblock The essence of compiling with continuations.
\newblock In \emph{{PLDI}}, pages 237--247. {ACM}, 1993.

[Fowler, 2016]
Simon Fowler.
\newblock An {Erlang} implementation of multiparty session actors.
\newblock In \emph{Proceedings of the 9th Interaction and Concurrency
Experience (ICE)}, volume 223 of \emph{Electronic Proceedings in Theoretical
Computer Science}, pages 36--50. Open Publishing Association, 2016.
\newblock \doi{10.4204/EPTCS.223.3}.

[Fowler et~al., 2019]
Simon Fowler, Sam Lindley, J.~Garrett Morris, and S{\'{a}}ra Decova.
\newblock Exceptional asynchronous session types: session types without tiers.
\newblock \emph{Proc. {ACM} Program. Lang.}, 3\penalty0 ({POPL}):\penalty0
28:1--28:29, 2019.

[Gordon, 2020]
Colin~S. Gordon.
\newblock Lifting sequential effects to control operators.
\newblock In \emph{{ECOOP}}, volume 166 of \emph{LIPIcs}, pages 23:1--23:30.
Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik, 2020.

[Gu} et~al., 2004]
T.~{Gu}, H.~K. {Pung}, and D.~Q. {Zhang}.
\newblock Toward an {OSGi}-based infrastructure for context-aware applications.
\newblock \emph{IEEE Pervasive Computing}, 3\penalty0 (4):\penalty0 66--74,
\newblock \doi{10.1109/MPRV.2004.19}.

[Harvey, 2015]
Paul Harvey.
\newblock \emph{A linguistic approach to concurrent, distributed, and adaptive
programming across heterogeneous platforms}.
\newblock PhD thesis, School of Computing Science, University of Glasgow, 2015.
\newblock URL \url{http://theses.gla.ac.uk/6749/}.

[Harvey and Sventek, 2017]
Paul Harvey and Joseph Sventek.
\newblock Adaptable actors: just what the world needs.
\newblock In \emph{Proceedings of the 9th Workshop on Programming Languages and
Operating Systems (PLOS)}, pages 22--28. ACM, 2017.
\newblock ISBN 978-1-4503-5153-9.
\newblock \doi{10.1145/3144555.3144559}.
\newblock URL \url{http://doi.acm.org/10.1145/3144555.3144559}.

[Hayton et~al., 1999]
Richard Hayton, Michael Bursell, Douglas~I. Donaldson, W.~Harwood, and Andrew
\newblock Mobile {J}ava objects.
\newblock \emph{Distributed Syst. Eng.}, 6\penalty0 (1):\penalty0 51, 1999.
\newblock \doi{10.1088/0967-1846/6/1/306}.
\newblock URL \url{https://doi.org/10.1088/0967-1846/6/1/306}.

[Hewitt et~al., 1973]
Carl Hewitt, Peter~Boehler Bishop, and Richard Steiger.
\newblock A universal modular {ACTOR} formalism for artificial intelligence.
\newblock In \emph{Proceedings of the 3rd international joint conference on
Artificial intelligence}, pages 235--245, San Francisco, CA, USA, 1973.
Morgan Kaufmann Publishers Inc.
\newblock URL \url{http://dl.acm.org/citation.cfm?id=1624775.1624804}.

[Honda, 1993]
Kohei Honda.
\newblock Types for dyadic interaction.
\newblock In \emph{{CONCUR} '93, 4th International Conference on Concurrency
Theory}, volume 715 of \emph{Lecture Notes in Computer Science}, pages
509--523. Springer, 1993.
\newblock \doi{10.1007/3-540-57208-2\_35}.
\newblock URL \url{https://doi.org/10.1007/3-540-57208-2\_35}.

[Honda et~al., 1998]
Kohei Honda, Vasco~Thudichum Vasconcelos, and Makoto Kubo.
\newblock Language primitives and type discipline for structured
communication-based programming.
\newblock In \emph{Programming Languages and Systems - ESOP'98, 7th European
Symposium on Programming}, volume 1381 of \emph{Lecture Notes in Computer
Science}, pages 122--138. Springer, 1998.
\newblock \doi{10.1007/BFb0053567}.
\newblock URL \url{https://doi.org/10.1007/BFb0053567}.

[Honda et~al., 2008]
Kohei Honda, Nobuko Yoshida, and Marco Carbone.
\newblock Multiparty asynchronous session types.
\newblock In \emph{Proceedings of the 35th Annual ACM SIGPLAN-SIGACT Symposium
on Principles of Programming Languages (POPL)}, volume~43, pages 273--284.
ACM, 2008.
\newblock \doi{10.1145/1328897.1328472}.
\newblock URL \url{http://doi.acm.org/10.1145/1328897.1328472}.

[Hu and Yoshida, 2017]
Raymond Hu and Nobuko Yoshida.
\newblock Explicit connection actions in multiparty session types.
\newblock In \emph{Proceedings of the 20th International Conference on
Fundamental Approaches to Software Engineering (FASE)}, Lecture Notes in
Computer Science, pages 116--133. Springer, 2017.
\newblock ISBN 978-3-662-54494-5.
\newblock \doi{10.1007/978-3-662-54494-5_7}.
\newblock URL \url{https://doi.org/10.1007/978-3-662-54494-5_7}.

[Hughes et~al., 2009]
Danny Hughes, Klaas Thoelen, Wouter Horr\'{e}, Nelson Matthys, Javier~Del Cid,
Sam Michiels, Christophe Huygens, and Wouter Joosen.
\newblock {LooCI}: a loosely-coupled component infrastructure for networked
embedded systems.
\newblock In \emph{Proceedings of the 7th International Conference on Advances
in Mobile Computing and Multimedia (MoMM)}, pages 195--203. ACM, 2009.
\newblock ISBN 978-1-60558-659-5.
\newblock \doi{http://doi.acm.org/10.1145/1821748.1821787}.
\newblock URL \url{http://doi.acm.org/10.1145/1821748.1821787}.

[Hui and Culler, 2004]
Jonathan~W. Hui and David Culler.
\newblock The dynamic behavior of a data dissemination protocol for network
programming at scale.
\newblock In \emph{Proceedings of the 2nd International Conference on Embedded
Networked Sensor Systems (SenSys)}, pages 81--94. ACM, 2004.
\newblock ISBN 1-58113-879-2.
\newblock \doi{10.1145/1031495.1031506}.
\newblock URL \url{http://doi.acm.org/10.1145/1031495.1031506}.

[Igarashi and Kobayashi, 2004]
Atsushi Igarashi and Naoki Kobayashi.
\newblock A generic type system for the pi-calculus.
\newblock \emph{Theor. Comput. Sci.}, 311\penalty0 (1-3):\penalty0 121--163,

[Igarashi et~al., 2001]
Atsushi Igarashi, Benjamin~C Pierce, and Philip Wadler.
\newblock Featherweight {J}ava: a minimal core calculus for {J}ava and {GJ}.
\newblock \emph{ACM Transactions on Programming Languages and Systems},
23\penalty0 (3):\penalty0 396--450, 2001.

[Jara et~al., 2012]
Antonio~J Jara, Pedro Martinez-Julia, and Antonio Skarmeta.
\newblock Light-weight multicast {DNS} and {DNS-SD} ({lmDNS-SD}): {IPv6}-based
resource and service discovery for the web of things.
\newblock In \emph{2012 Sixth international conference on innovative mobile and
internet services in ubiquitous computing}, pages 731--738. IEEE, 2012.

[Johnsen et~al., 2010]
Einar~Broch Johnsen, Reiner H{\"{a}}hnle, Jan Sch{\"{a}}fer, Rudolf Schlatte,
and Martin Steffen.
\newblock {ABS:} {A} core language for abstract behavioral specification.
\newblock In \emph{{FMCO}}, volume 6957 of \emph{Lecture Notes in Computer
Science}, pages 142--164. Springer, 2010.

[Kamburjan et~al., 2016]
Eduard Kamburjan, Crystal~Chang Din, and Tzu{-}Chun Chen.
\newblock Session-based compositional analysis for actor-based languages using
\newblock In \emph{{ICFEM}}, volume 10009 of \emph{Lecture Notes in Computer
Science}, pages 296--312, 2016.

[Kouzapas et~al., 2018]
Dimitrios Kouzapas, Ornela Dardha, Roly Perera, and Simon~J. Gay.
\newblock Typechecking protocols with {Mungo} and {StMungo}: a session type
toolchain for {Java}.
\newblock \emph{Science of Computer Programming}, 155:\penalty0 52--75, 2018.
\newblock ISSN 0167-6423.
\newblock \doi{https://doi.org/10.1016/j.scico.2017.10.006}.
\newblock URL
\url{http://www.sciencedirect.com/science/article/pii/S0167642317302186}.

[Levy et~al., 2003]
Paul~Blain Levy, John Power, and Hayo Thielecke.
\newblock Modelling environments in call-by-value programming languages.
\newblock \emph{Information and Computation}, 185\penalty0 (2):\penalty0
182--210, 2003.

[Milner, 1999]
Robin Milner.
\newblock \emph{Communicating and mobile systems - the Pi-calculus}.
\newblock Cambridge University Press, 1999.

[Mockapetris, 1987]
Paul~V Mockapetris.
\newblock {RFC} 1035: Domain names - implementation and specification, 1987.

[Montesi et~al., 2007]
Fabrizio Montesi, Claudio Guidi, and Gianluigi Zavattaro.
\newblock Composing services with {JOLIE}.
\newblock In \emph{{ECOWS}}, pages 13--22. {IEEE} Computer Society, 2007.

[Mostrous and Vasconcelos, 2018]
Dimitris Mostrous and Vasco~T. Vasconcelos.
\newblock Affine sessions.
\newblock \emph{Log. Methods Comput. Sci.}, 14\penalty0 (4), 2018.

[Mostrous and Vasconcelos, 2011]
Dimitris Mostrous and Vasco~Thudichum Vasconcelos.
\newblock Session typing for a featherweight {Erlang}.
\newblock In \emph{Proceedings of the 13th International Conference on
Coordination Models and Languages (COORDINATION)}, volume 6721 of
\emph{Lecture Notes in Computer Science}, pages 95--109. Springer, 2011.
\newblock \doi{10.1007/978-3-642-21464-6_7}.
\newblock URL \url{https://doi.org/10.1007/978-3-642-21464-6_7}.

[Neykova and Yoshida, 2014]
Rumyana Neykova and Nobuko Yoshida.
\newblock Multiparty session actors.
\newblock In \emph{Proceedings of the 16th IFIP WG 6.1 Conference on
Coordination Models and Languages (COORDINATION)}, volume 8459 of
\emph{Lecture Notes in Computer Science}, pages 131--146. Springer, 2014.
\newblock \doi{10.1007/978-3-662-43376-8_9}.
\newblock URL \url{https://doi.org/10.1007/978-3-662-43376-8_9}.

[Neykova and Yoshida, 2017]
Rumyana Neykova and Nobuko Yoshida.
\newblock Multiparty session actors.
\newblock \emph{Logical Methods in Computer Science}, 13\penalty0
(1:17):\penalty0 1--30, 2017{\natexlab{a}}.
\newblock \doi{10.23638/LMCS-13(1:17)2017}.
\newblock URL \url{https://doi.org/10.23638/LMCS-13(1:17)2017}.

[Neykova and Yoshida, 2017]
Rumyana Neykova and Nobuko Yoshida.
\newblock Let it recover: multiparty protocol-induced recovery.
\newblock In \emph{Proceedings of the 26th International Conference on Compiler
Construction (CC)}, pages 98--108. ACM, 2017{\natexlab{b}}.
\newblock URL \url{http://dl.acm.org/citation.cfm?id=3033031}.

[Porter et~al., 2016]
Barry Porter, Matthew Grieves, Roberto~Rodrigues Filho, and David Leslie.
\newblock {REX}: A development platform and online learning approach for
runtime emergent software systems.
\newblock In \emph{12th {USENIX} Symposium on Operating Systems Design and
Implementation ({OSDI})}, pages 333--348. {USENIX} Association, 2016.
\newblock ISBN 978-1-931971-33-1.
\newblock URL
\url{https://www.usenix.org/conference/osdi16/technical-sessions/presentation/porter}.

[Preda et~al., 2017]
Mila~Dalla Preda, Maurizio Gabbrielli, Saverio Giallorenzo, Ivan Lanese, and
Jacopo Mauro.
\newblock Dynamic choreographies: Theory and implementation.
\newblock \emph{Logical Methods in Computer Science}, 13\penalty0 (2), 2017.
\newblock \doi{10.23638/LMCS-13(2:1)2017}.
\newblock URL \url{https://doi.org/10.23638/LMCS-13(2:1)2017}.

[Rellermeyer et~al., 2007]
Jan~S Rellermeyer, Gustavo Alonso, and Timothy Roscoe.
\newblock {R}-{OSGi}: distributed applications through software modularization.
\newblock In \emph{ACM/IFIP/USENIX International Conference on Distributed
Systems Platforms and Open Distributed Processing}, pages 1--20. Springer,

[Scalas and Yoshida, 2019]
Alceste Scalas and Nobuko Yoshida.
\newblock Less is more: multiparty session types revisited.
\newblock \emph{Proc. {ACM} Program. Lang.}, 3\penalty0 ({POPL}):\penalty0
30:1--30:29, 2019.

[Scalas et~al., 2017]
Alceste Scalas, Ornela Dardha, Raymond Hu, and Nobuko Yoshida.
\newblock A linear decomposition of multiparty sessions for safe distributed
\newblock In \emph{Proceedings of the 31st European Conference on
Object-Oriented Programming (ECOOP)}, volume~74 of \emph{Leibniz
International Proceedings in Informatics (LIPIcs)}, pages 24:1--24:31, 2017.
\newblock \doi{10.4230/LIPIcs.ECOOP.2017.24}.
\newblock URL \url{https://doi.org/10.4230/LIPIcs.ECOOP.2017.24}.

[Visintainer et~al., 2013]
Filippo Visintainer, Leandro D'Orazio, Marco Darin, and Luciano Altomare.
\newblock Cooperative systems in motorway environment: The example of {T}rento
test site in {I}taly.
\newblock In Jan Fischer-Wolfarth and Gereon Meyer, editors, \emph{Advanced
Microsystems for Automotive Applications 2013}, pages 147--158, Heidelberg,
2013. Springer International Publishing.
\newblock ISBN 978-3-319-00476-1.

[Xia et~al., 2012]
Feng Xia, Laurence~T. Yang, Lizhe Wang, and Alexey~V. Vinel.
\newblock Internet of things.
\newblock \emph{International Journal of Communication Systems}, 25\penalty0
(9):\penalty0 1101--1102, 2012.
\newblock \doi{10.1002/dac.2417}.
\newblock URL \url{https://doi.org/10.1002/dac.2417}.

[Yoshida et~al., 2014]
Nobuko Yoshida, Raymond Hu, Rumyana Neykova, and Nicholas Ng.
\newblock The {S}cribble protocol language.
\newblock In \emph{Proceedings of the 8th International Symposium on
Trustworthy Global Computing (TGC)}, volume 8358, pages 22--41. Springer,
\newblock ISBN 978-3-319-05118-5.
\newblock \doi{10.1007/978-3-319-05119-2_3}.
\newblock URL \url{https://doi.org/10.1007/978-3-319-05119-2_3}.

\end{thebibliography}

\newpage

\appendix

\begin{adjustwidth}{-70pt}{-60pt}
\changetext{0pt}{12em}{}{}{}\onecolumn
\nolinenumbers
\section{Global types and projection}\label{appendix:projection}

In this section, we show how global types can be projected into the local types
used in the core formalism. Unlike in classic MPST works, it is not the case
that projection alone guarantees safety and deadlock-freedom in itself.
Rather, projection produces local types,
which can be validated separately as described in the main
body of the paper.

This section is mostly a straightforward adaptation of the
work of~Hu and Yoshida, 2017 to our setting.

\begin{figure}
\small
\header{Meta-level definitions}

\[
\begin{array}{rcl}
\isoutput{L} & \defeq & L \in \{ \localtysend{\prole}{\ell}{A}, \localtyconn{\prole}{\ell}{A} \} \\
\isinput{L} & \defeq & L \in \{ \localtyrecv{\prole}{\ell}{A},  \localtyaccept{\prole}{\ell}{A} \} \\
\subj{\globalsend{\prole}{\qrole}{\ell}{A}},
\subj{\globalconn{\prole}{\qrole}{\ell}{A}},
\subj{\globaldisconn{\prole}{\qrole}} & \defeq & \prole \\
\obj{\globalsend{\prole}{\qrole}{\ell}{A}},
\obj{\globalconn{\prole}{\qrole}{\ell}{A}},
\obj{\globaldisconn{\prole}{\qrole}} & \defeq & \qrole \\
\end{array}
\]

\header{Projection}

\[
\begin{array}{rcl}
\project{G}{\rrole} & = & \hyproject{G}{\rrole}{\emptyset} \\
\hyproject{(\globalsend{\prole}{\qrole}{\ell}{\tya} \then G)}{\rrole}{\recenv} & = &
\begin{cases}
\localtysend{\qrole}{\ell}{\tya} \then (\hyproject{G}{\rrole}{\recenv}) & \rrole = \prole \\
\localtyrecv{\prole}{\ell}{\tya} \then (\hyproject{G}{\rrole}{\recenv}) & \rrole = \qrole \\
\hyproject{G}{\rrole}{\recenv} & \rrole \not\in \{ \prole, \qrole \} \\
\end{cases}
\rowskip
\\
\hyproject{(\globalconn{\prole}{\qrole}{\ell}{\tya} \then G)}{\rrole}{\recenv} & = &
\begin{cases}
\localtyconn{\qrole}{\ell}{\tya} \then (\hyproject{G}{\rrole}{\recenv}) & \rrole = \prole \\
\localtyaccept{\prole}{\ell}{\tya} \then (\hyproject{G}{\rrole}{\recenv}) & \rrole = \qrole \\
\hyproject{G}{\rrole}{\recenv} & \rrole \not\in \{ \prole, \qrole \} \\
\end{cases}
\rowskip
\\
\hyproject{(\globaldisconn{\prole}{\qrole} \then {G})}{\rrole}{\recenv} & = &
\begin{cases}
\localtydisconn{\qrole} & \rrole = \prole \text{ and }
\hyproject{G}{\rrole}{\emptyset} = \localend \\
\localtywait{\prole} \then (\hyproject{G}{\rrole}{\emptyset}) & \rrole = \qrole \\
\hyproject{G}{\rrole}{\recenv} & \rrole \not\in \{ \prole, \qrole \}
\end{cases}
\rowskip
\\
\hyproject{\sumact{i \in I}{G_i}}{\rrole}{\recenv} & = &
\begin{cases}
X & \forall i \in I. (\hyproject{G_i}{\rrole}{\recenv}) = X \\
\localend & \forall i \in I. (\hyproject{G_i}{\rrole}{\recenv}) = \localend \\
\sumact{j \in J \subseteq I}{L_j = \hyproject{G_j}{\rrole}{\recenv}} &
\begin{array}{l}
\size{I} > 1, \size{J} > 0, \text{ and } \\
\forall k \in I \setminus J . \hyproject{G_k}{\rrole}{\recenv} = \localend \text{ or } X \in \recenv, \text{ and } \\
\quad
\text{either }
\begin{cases}
\forall j \in J. \isoutput{L_j} \\
\exists \role{\prole} . \forall j \in J. \isinput{L_j} \wedge \subj{L_j} = \role{\prole}
\end{cases}
\end{array}
\end{cases}
\rowskip
\\
\hyproject{\recty{X}{G}}{\rrole}{\recenv} & = &
\begin{cases}
\localend & \hyproject{G}{\rrole}{\recenv, X} = X' \text{ or } \localend \\
\hyproject{G}{\rrole}{\Delta, X} & \text{otherwise}
\end{cases}
} \rowskip \\
\hyproject{X}{\rrole}{\recenv} & = & X \rowskip \\
\hyproject{\globalend}{\rrole}{\recenv} & = & \localend
\end{array}
\]

\caption{Global types and projection}
\label{fig:appendix:global-types}
\end{figure}

\subparagraph{Syntax of types.}
Similar to the presentation of local types, the key difference between this
presentation of global types and standard MPST systems is that instead of having
branching of the form $\role{r} \rightarrow \role{s} \{ \ell_i : G_i\}_i$, where
a single role makes a choice, this presentation of global types provides
arbitrary summations of \emph{global actions}. The standard sending action is
therefore $\globalsend{\prole}{\qrole}{\ell}{\tya} \then G$ which involves role
$\prole$ sending message $\ell(\tya)$ to $\qrole$.

A key technical innovation is \emph{explicit connection actions}
($\globalconn{\prole}{\qrole}{\ell}{\tya}$) which establish a connection between two roles
$\role{\prole}$ and $\role{\qrole}$ by sending a label $\ell$. Conversely,
\emph{disconnection} $\globaldisconn{\prole}{\qrole}$ is a directed
disconnection where $\prole$ disconnects from $\qrole$, and $\qrole$ waits for
$\prole$'s disconnection.

Instead of assuming that all roles are connected at the start of the the
session, in order to communicate, each role must be connected explicitly. This
allows communication paths where one party isn't involved (as in Hu and
Yoshida's travel agent example).

\subparagraph{Projection.}

Global types can be \emph{projected} at a role in order to obtain a local type.
In standard MPST systems, a global type is well-formed if it is closed,
contractive, and projectable at all roles. A well-formed global type is then
guaranteed to be deadlock-free.

Define $\roles{G}$ to be the set of roles contained within global type $G$.

The projection function
$\hyproject{G}{\rrole}{\recenv}$ projects global type $G$ at role $\rrole$, and is
parameterised by a set of recursion variables $\recenv$. The inclusion of the
$\recenv$ parameter allows the pruning of unguarded recursion variables.

Projection on unary choices, recursive types, type variables, and session
termination are standard. Disconnection ensures that the disconnecting role is
unused in the remainder of the protocol.

Now consider the case of projecting $n$-ary choices for $n > 1$.
Suppose we have $\hyproject{\sumact{i \in I}{G_i}}{\rrole}{\recenv}$.
If $\hyproject{G_i}{\rrole}{\recenv} = \localend$ for all $G_i$, then the result of the
projection is $\localend$ (and similarly for a recursion variable $X$).

Otherwise, there will be some subset $J$ of $I$ such that each $L_j$ for $j \in
J$ is a communication action, and each $L_k \in I \setminus J$ projects to
either $\localend$ or a recursion variable.
For each $j \in J$, there is a further condition: the choice must consist of all
send actions, or all receive actions. If the latter, then the receiver must be
the same in all branches. This will ensure syntactically well-formed local
types used in the paper.

\subparagraph{Unfolding.}
We define the 1-unfolding of a global type $G$, $\unf{G}$, as
$\unf{\recty{X}{G}} = \unf{G\{ \globalend / X \}}$ and defined recursively over
the other constructs.

\subparagraph{Role enabling.}

In order to ensure that projection produces syntactically well-formed local
types, we require global types to satisfy \emph{role enabling}: intuitively,
this means that after a choice occurs, each role must be `activated' by
receiving a message before performing any further communications. In turn, this
avoids mixed choice.

Let $R$ range over sets of roles.

\headersig{Role enabling}{$\enableseq{R}{G}$}
\begin{mathpar}
\inferrule
{ \subj{\globact} \subseteq R \\
\enableseq{R \cup \obj{\globact}}{G} }
{ \enableseq{R}{\globact \then G} }

\inferrule
{ \size{I} > 1 \\
\exists \prole \in R .
\forall i \in I.
\subj{\globact_i} = \{ \prole \} \wedge
\enableseq{\{ \prole \} \cup \obj{\globact_i}}{G_i}
{ \enableseq{R}{\sumact{i \in I}{G_i}} }
\end{mathpar}

\subparagraph{Syntactic validity of projected local types.}

\begin{definition}[Initiator (global type)]
We say that $\prole$ is an \emph{initiator} of $G$ if $\prole \in
\roles{G}$ and $\project{G}{\prole} = \sumact{i \in I}{\globact_i \then G_i}$,
where each $\globact_i$ is a connection action. We say that $\prole$ is the
\emph{unique initiator} of $G$ if it is the only initiator.
\end{definition}

Given the above definitions, we can show that the set of projected local types
are syntactically valid.

\begin{lemma}
Suppose $\prole$ is the unique initiator of $G$.
If $\enableseq{\prole}{\unf{G}}$ and $(\project{G}{\qrole} = L_\qrole)_{\qrole \in \roles{G}}$,
then each $L_\qrole$ is syntactically valid.
\end{lemma}
\begin{proof}[Proof sketch.]
The result can be established by induction on the derivation of

Due to the partiality of the projection operation, disconnection actions
must only occur as unary choices, and role enabling coupled with the
conditions on the projection of non-unary choices preclude mixed choice.
\end{proof}

\clearpage
\section{Proofs for Section~\ref{sec:core-calculus}}\label{appendix:proofs}

\subsection{Preservation}

\begin{lemma}[Preservation (Terms)]\label{lem:term-pres}
If $\tseq{\Gamma}{\loctya}{M}{A}{\loctya'}$ and $M \teval N$, then $\tseq{\Gamma}{\loctya}{N}{A}{\loctya'}$.
\end{lemma}
\begin{proof}
By induction on the derivation of $M \teval N$.
\end{proof}

\begin{lemma}[Preservation (Equivalence)]\label{lem:equiv-pres}
If $\cseq{\Gamma}{\rtenv}{\config{C}}$ and $\config{C} \equiv \config{D}$,
then $\cseq{\Gamma}{\rtenv}{\config{D}}$.
\end{lemma}
\begin{proof}
By induction on the derivation of $\config{C} \equiv \config{D}$.
\end{proof}

\begin{lemma}[Substitution]\label{lem:substitution}
If $\tseq{\Gamma, x : A}{S}{M}{B}{S'}$ and $\vseq{\Gamma}{V}{A}$, then
$\tseq{\Gamma}{S}{M \{ V / x \}}{B}{S'}$.
\end{lemma}
\begin{proof}
By induction on the derivation of $\tseq{\Gamma, x : A}{S}{M}{B}{S'}$.
\end{proof}

\begin{lemma}[Subterm typability]\label{lem:subterm-typability}
Suppose $\deriv{D}$ is a derivation of $\tseq{\Gamma}{S}{E[M]}{A}{S'}$.
Then there exists some subderivation $\deriv{D}'$ of $\deriv{D}$ concluding
$\tseq{\Gamma}{S}{M}{B}{S''}$ for some type $B$ and local type $S''$, where
the position of $\deriv{D}'$ in $\deriv{D}$ corresponds to that of the hole in
\end{lemma}
\begin{proof}
By induction on the structure of $E$.
\end{proof}

\begin{lemma}[Replacement]\label{lem:replacement}

\begin{enumerate}
\item $\deriv{D}$ is a derivation of $\tseq[\loctyc]{\Gamma}{S}{E[M]}{A}{T}$
\item $\deriv{D}'$ is a subderivation of $\deriv{D}$ concluding
$\tseq[\loctyc]{\Gamma}{S}{M}{B}{T'}$, where the position of $\deriv{D}'$ in
$\deriv{D}$ corresponds to that of the hole in $\ep$
\item $\tseq[\loctyc]{\Gamma}{S}{N}{B}{T'}$
\end{enumerate}

Then $\tseq[\loctyc]{\Gamma}{S}{E[N]}{A}{T}$.
\end{lemma}
\begin{proof}
By induction on the structure of $E$.
\end{proof}

Due to the absence of exception handling frames which constrain the
pre-condition to match that of the failure continuation,
pure contexts admit a more liberal replacement lemma.

\begin{lemma}[Replacement (Pure contexts)]\label{lem:pure-replacement}

\begin{enumerate}
\item $\deriv{D}$ is a derivation of $\tseq[\loctyc]{\Gamma}{S}{\ep[M]}{A}{T}$
\item $\deriv{D}'$ is a subderivation of $\deriv{D}$ concluding
$\tseq[\loctyc]{\Gamma}{S}{M}{B}{T'}$, where the position of $\deriv{D}'$ in
$\deriv{D}$ corresponds to that of the hole in $\ep$
\item $\tseq[\loctyc]{\Gamma}{S'}{N}{B}{T'}$
\end{enumerate}

Then $\tseq[\loctyc]{\Gamma}{S'}{\ep[N]}{A}{T}$.
\end{lemma}
\begin{proof}
By induction on the structure of $\ep$, noting that $\loctya$ is not constrained
by exception handling frames.
\end{proof}

\configpres*
\begin{proof}
By induction on the derivation of $\config{C} \ceval \config{C}'$.
Where there is a choice of whether $\connstate = \bot$ or $\connstate =