# Implementing Multiparty Session Types in Rust

Nicolas Lagaillardie, Rumyana Neykova, Nobuko Yoshida

## ► To cite this version:

Nicolas Lagaillardie, Rumyana Neykova, Nobuko Yoshida. Implementing Multiparty Session Types in Rust. 22th International Conference on Coordination Languages and Models (COORDINATION), Jun 2020, Valletta, Malta. pp.127-136, 10.1007/978-3-030-50029-0_8 . hal-03273998

HAL Id: hal-03273998

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

Submitted on 29 Jun 2021

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

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

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

Distributed under a Creative Commons Attribution 4.0 International License
# Implementing Multiparty Session Types in Rust

Nicolas Lagaillardie¹[0000-0002-6431-4100], Rumyana
Neykova²[0000-0002-2755-7728], and Nobuko Yoshida¹[0000-0002-3925-8557]

¹ Imperial College London, London, UK

n.lagaillardie19@imperial.ac.uk, n.yoshida@imperial.ac.uk

² Brunel University London, London, UK

rumyana.neykova@brunel.ac.uk

**Abstract.** Multiparty Session Types (MPST) is a typing discipline for distributed protocols, which ensures communication safety and deadlock-freedom for more than two participants. This paper reports on our research project, implementing multiparty session types in Rust. Current Rust implementations of session types are limited to binary (two-party communications). We extend an existing library for binary session types to MPST. We have implemented a simplified Amazon Prime Video Streaming protocol using our library for both shared and distributed communication transports.

## 1 Introduction

In the last decade, the software industry has seen a shift towards programming languages that promote the coordination of concurrent and/or distributed software components through the exchange of messages over communication channels. Languages with native message-passing primitives (e.g., Go, Elixir and Rust) are becoming increasingly popular. In particular, Rust has been named the most loved programming language in the annual Stack Overflow survey for four consecutive years (2016-19)<fnref n="3" />.

The advantage of message-passing concurrency is well-understood: it allows cheap horizontal scalability at a time when technology providers have to adapt and scale their tools and applications to various devices and platforms. Message-passing based software, however, is as vulnerable to errors as other concurrent programming techniques [16]. Much academic research has been done to develop rigorous theoretical frameworks for verification of message-passing programs. One such framework is *multiparty session types* (MPST) [5] – a type-based discipline that ensures that concurrent and distributed systems are *safe by design*. It guarantees that message-passing processes following a predefined communication protocol, are free from communication errors and deadlocks.

Rust is a particularly appealing language for the practical embedding of session types. Its *affine type system* allows for static typing of linear resources – an essential requirement for the safety of session type systems. Rust combines

<footnote n="3">³ https://insights stackoverflow com / survey / 2019</footnote>
efficiency with message-passing abstractions, thread and memory safety [15], and
has been used for the implementation of large-scale concurrent applications such
as the Mozilla browser, Firefox, and the Facebook blockchain platform, Libra.
Despite the interest in the Rust community for verification techniques handling
multiple communicating processes<fnref n="4" />, the existing Rust implementations [8,9] are
limited to *binary* (two-party) session types.

In this short paper, we present our design and implementation for multi-
party session types in Rust. Our design follows a state-of-the-art encoding of
multiparty into binary session types [13]. We generate local types in Rust, utilis-
ing the Scribble toolchain [18,12]. Our library for MPST programming in Rust,
*mpst-rust*, is implemented as a thin wrapper over an existing binary session
types library [9]. Differently from other MPST implementations that check the
linear usage of channels at runtime (e.g. [13,6]), we rely on the Rust affine type
system to type-check MPST programs. In addition, since we generate the local
types from a readable global specification, errors caused by an affine (and not
linear) usage of channels, a well-known limitation of the previous libraries [8,9],
are easily avoided.

This paper is organised as follows: § 2 gives an overview of our framework with a usecase; § 3 shows our implementation and discusses the advantages of our approach; and § 4 concludes with related and future work. Our library is available from https://github.com/NicolasLagaillardie/mpst_rust_github.

## 2 From Binary to Multiparty Sessions in Rust

**Framework overview: MPST in Rust.** Our design resembles the top-down methodology of multiparty session types, as illustrated in Figure 1. It follows three main steps [17,5]. First, a *global type*, also called a *global protocol*, is defined as a shared contract between communicating endpoint processes. A global protocol is then *projected* to each endpoint process, resulting in a *local type*. A local type involves only the interactions specific to a given endpoint. Finally, each endpoint process is type-checked against its projected local type.

The specific parts of our framework that distinguish it from other state-
of-the-art MPST works are highlighted in red, which corresponds to our new
library for MPST programming in Rust, mpst-rust. It is realised as a thin
wrapper on top of an existing Rust library for validation of binary (2-party-only)
session types. Developers use the MPST primitives provided by mpst-rust to
implement endpoint programs. Also, our framework allows the types for each
communication primitive to be either (1) generated from the Scribble toolchain;
or (2) written by the developers. The Scribble toolchain [18] provides facilities
for writing, verifying and projecting global protocols. Our framework guarantees
that processes implemented using mpst-rust primitives with Scribble-generated
types are free from deadlocks, reception errors, and protocol deviations. Next,
we explain, via an example, how the framework of MPST can be applied to Rust.

<footnote n="4">⁴ https://users.rust-lang.org/t/anybody-working-on-multiparty-session-types-for-rust/10610</footnote>
<figure><img src="image_2.png" /><figcaption>Fig. 1: MPST Workflow (left) and Amazon Prime Video usecase (right)</figcaption></figure>

**Example: Amazon Prime Video Streaming.** The Amazon Prime Video streaming service is a usecase which can take full advantage of multiparty session types. Each streaming application connects to servers, and possibly other devices, to access services, and follows some specific protocol. To present our design, we use a simplified version of the protocol, illustrated in the diagram in Figure 1 (right). The diagram should be read from top to bottom. The protocol involves three services – an **Authenticator** service, a **Server** and a **Client**. At first, **Client** connects to **Authenticator** by providing an identifying **id**. If the **id** is accepted, the session continues with a choice on **Client** to either request a video or end the session. The first branch is, *a priori*, the main service provided by Amazon Prime Video. **Client** cannot directly request videos from **Server**, and has to go through **Authenticator** instead. On the diagram, the choice is denoted as the frame **alt** and the choices are separated with the horizontal dotted line. The protocol is recursive, and **Client** can request new videos as many times as needed. The arrow going back on **Client** side in Figure 1 represents this recursive behaviour. To end the session, **Client** first sends **Close** message to **Authenticator**, which then subsequently sends a **Close** message to **Server**.

**Implementing the Authenticator role using mpst-rust.** Due to space limitations, we only show the implementation of the **Authenticator** role (hereafter **role A**), the implementations of the other roles (role **B** for the **Server** and role **C** for the **Client**) are similar. The Rust code for role **A** using the **mpst-rust** library is given in Figure 2 (left). It closely follows the local protocol in Figure 2 (right), that is projected from the global protocol by the Scribble toolchain. First, line 1 declares a function **authenticator** that is parametric in a multiparty channel **s** of type **VideoP_A**. The type **VideoP_A** specifies which operations are allowed on **s**. This type can either be written by the developer, or generated by Scribble (cf. Listing 1).

On line 3, **A** receives an identifying **id** from **C**. The function **recv mpst a to c**, provided by **mpst-rust** library returns the received value (the **id**) and the new multiparty channel, to be used in subsequent communications. Line 3 rebinds the multiparty channel **s** with the new channel that is returned. Then, on line 4, we send back the answer to **C**, by utilising another **mpst-rust** communication primitive, **send mpst a to c**. The variable **s** is rebound again to the newly returned multiparty channel. Note that although the name of the function, **send mpst a to c**, suggests a binary communication, the function operates
<figure><img src="image_3.png" /><figcaption>Fig. 2: Rust implementation of role A (left) and its local Scribble protocol (right)</figcaption></figure>

on a multiparty channel s. Our implementation follows the encoding, presented in [13], which encodes a multiparty channel as an indexed tuple of binary channels. Internally, `send mpst a to c` extracts from s the binary channel established between A and C and uses it for sending.

Lines 9–26 proceeds by implementing the recursive part of the protocol. The implementation of `authenticator recurs` realises an internal choice – A can either receive a `VideoRequest` or a `Close`. This behaviour is realised by the `mpst-rust` macro `offer mpst a to c!` (line 12), which is applied to a multiparty channel s of a sum type between `ChoiceA::Video` and `ChoiceA::End`. The behaviour of each branch in the protocol is implemented as an anonymous function. For example, code in lines 13–21 supplies an anonymous function that implements the behaviour when C sends a `VideoRequest`, while lines 22–26 handle the `Close` request. Finally, `close mpst(s)` closes all binary channels stored inside s. The types of the multiparty channel, as well as the generic types in the declaration of the `mpst-rust` communication functions, enable compile-time detection of protocol violations, such as swapping line 3 and line 4, using another communication primitive or using the wrong payload type.

**Typing the Authenticator role.** The types for the Authenticator role, used in Figure 2 (left), are given in Listing 1. These types can be either written by the developer or generated from a global protocol, written in Scribble. Reception error safety is ensured since the underlying `mpst-rust` library checks statically that all pairs of binary types are dual to each other. Deadlock-freedom is ensured only if types are generated from Scribble since this guarantees that types are projected from a well-formed global protocol.
<table><caption>Listing 1: Local Rust types for role A</caption><thead><tr><th></th><th></th><th></th></tr></thead><tbody><tr><td>1</td><td>/// Binary session types for A and C</td><td>20 /// Declare usage order of channels</td></tr><tr><td>2</td><td>type InitA&lt;N&gt; = Recv&lt;N, Send&lt;N,</td><td>21 type QueueAVideo =</td></tr><tr><td>3</td><td>RecvChoice&lt;N&gt;&gt;&gt;;</td><td>22 RoleAtoC&lt;RoleAtoB&lt;RoleAtoB&lt;</td></tr><tr><td>4</td><td>type RecvChoice&lt;N&gt; =</td><td>23 RoleAtoC&lt;RoleAtoC&lt;RoleEnd&gt;&gt;&gt;&gt;;</td></tr><tr><td>5</td><td>Recv&lt;ChoiceA&lt;N&gt;, End&gt;;</td><td>24 type QueueAClose = RoleEnd;</td></tr><tr><td>6</td><td>type AtoCVideo&lt;N&gt; =</td><td>25</td></tr><tr><td>7</td><td>Recv&lt;N, Send&lt;N, RecvChoice&lt;N&gt;&gt;</td><td>26 /// Declare MPST</td></tr><tr><td>8</td><td>type AtoCClose = End;</td><td>27 type VideoP_A&lt;N&gt; = SessionMpst&lt;End,</td></tr><tr><td>9</td><td></td><td>28 InitA&lt;N&gt;, QueueAInit&gt;;</td></tr><tr><td>10</td><td></td><td>29</td></tr><tr><td>11</td><td>/// Binary session types for A and B</td><td>30 type VideoPRec_A&lt;N&gt; = SessionMpst&lt;</td></tr><tr><td>12</td><td>type AtoBVideo&lt;N&gt; =</td><td>31 End, RecvChoice&lt;N&gt;, QueueAChoice&gt;;</td></tr><tr><td>13</td><td>Send&lt;N, Recv&lt;N, End&gt;&gt;;</td><td>32</td></tr><tr><td>14</td><td>type AtoBClose = End;</td><td>33 enum ChoiceA&lt;N&gt; {</td></tr><tr><td>15</td><td></td><td>34 Video sessio nMpst&lt;AtoBVideo&lt;N&gt;</td></tr><tr><td>16</td><td>/// Declare usage order of channels</td><td>35 AtoCVideo&lt;N&gt;, QueueAVideo&gt;,</td></tr><tr><td>17</td><td>type QueueAInit = RoleAtoC&lt;RoleAtoC&lt;</td><td>36 End sessio nMpst&lt;AtoBClose,</td></tr><tr><td>18</td><td>RoleAtoC&lt;RoleEnd&gt;&gt;&gt;;</td><td>37 AtoCClose, QueueAClose&gt;</td></tr><tr><td>19</td><td>type QueueAChoice = RoleAtoC&lt;RoleEnd&gt;;</td><td>38 }</td></tr></tbody></table>

Next, we explain a type declaration for the `Authenticator` role. Lines 27–37 specify the three `SessionMpst` types which correspond to the types of the session channels used in Figure 2 (left) – types `VideoP_A` (line 1), `VideoPRec_A` (line 9), and the types used inside the `offer` construct – `ChoiceA::Video` (line 13), and `ChoiceA::End` (line 22).

In the encoding of [13], which underpins `mpst-rust`, a multiparty channel is represented as an indexed tuple of binary channels. This is reflected in the implementation of `SessionMpst`, which is parameterised on the required binary session types. For example, the `VideoP_A&lt;N&gt;` takes as a parameter the binary types between `A` and `C`, and between `A` and `B`. At the beginning of the protocol (lines 1-7 in Figure 2 (left)) `B` and `A` do not interact, hence the binary type for `B` is `End`. The type `InitA&lt;N&gt;` (line 2 in Listing 1) specifies the behaviour between `A` and `C`, notably that `A` first receives a message, then it sends a message, and later it continues as the type `RecvChoice&lt;N&gt;`. The binary session types between `A` and `B`, and between `A` and `C` are given in lines 12–14 and lines 2–9 respectively; we use the primitives declared in the existing binary session types library [9]. The generic parameter `N` refers to a trait such as `i32`.

The third parameter for `VideoP_A&lt;N&gt;` (line 27) is a queue-like data structure, `QueueAInit` (line 17), that codifies the order of usage of each binary channel inside a multiparty session channel. This is needed to preserve the causality, imposed by the global protocol. The queues for the other `SessionMpst` types are given in lines 21–24. For instance, the queue for the `ChoiceA::Video` branch of the protocol is `QueueAVideo`. Note that, according to the protocol, `A` first has to receive a `VideoRequest` message from `C`, and then it has to forward that message to `B`. Hence, swapping of lines 17 and 18 from Figure 2 is a protocol violation error. We can detect such violations since the queue for the type `ChoiceA::Video`, `QueueAVideo` (line 21), is specified as `RoleAtoC&lt;RoleAtoB ...&gt;`, which codifies that first the channel for `C` and then the channel for `B` should be used. Note that none
of the defined queues is recursive. Recursion is implicitly specified on binary
types, while each queue is related to a SessionMpst type.

**Distributed Execution Environment.** The default transport of `mpst-rust` is the built-in Rust communication channels (crossbeam_channel). Also, to test our example in a more realistic distributed environment, we have also connected each process through MQTT (MQ Telemetry Transport) [7]. MQTT is a messaging middleware for exchanging messages between devices, predominantly used in IoT networks. At the start of the protocol, each process connects to a public MQTT channel, and a session is established. Therefore, we have mapped binary channels to MQTT sockets, in addition to the built-in Rust channels.

## 3 Design and Implementation of mpst-rust

**Multiparty channels as an ordered tuple of binary channels.** The main idea of the design of our framework is that a multiparty session can be realised with two ingredients: (1) a list of separate binary sessions (one session for each pair of participants) and (2) a queue that imposes the ordering between the binary channels. Listing 2 (lines 2–3) shows the implementation of a multiparty channel in a 3-party protocol. The `SessionMpst` structure holds two fields, `session1` and `session2`, that are of a binary session type. For an illustration purpose, we show only the implementation of a multiparty channel for three processes. The same approach can be generalised, using our code generation tool, to any number of communicating processes. For example, in case of a protocol with four roles, each multiparty session will have four fields – a field for the binary session between each pair of participants and a field for the queue.

The order of usage of the binary channels of a `SessionMpst` object is stored inside the `queue` field. For instance, the behaviour that role A has to communicate first with role B, then with a role C, and then the session ends can be specified using a queue of type `RoleAtoB<RoleAtoC<RoleEnd>>`. Note that all queue types, such as `RoleAtoB`, `RoleAtoC`, are generated.

**MPST communication primitives as wrappers of binary channels.** As explained in § 2, programming with `mpst-rust` relies on communication primitives, such as `sendpek_a_to_b`, that have the sender and receiver roles baked into their name. To ensure that the binary channels are used as specified by the global protocol, each communication function is parametric on a generic quadruple type `<T, S1, S2, R>` where `T` is a payload type, `S1` and `S2` are binary session types and `R` is a type for a queue (MPST-queue type) that imposes the order in which the binary sessions inside a multiparty session must be used.

Listing 2 (lines 5–9) shows the implementation for `sendpek_a_to_b()`. As clear from the type parameters, the client of the function should supply a MPST-queue type `RoleAtoB<R>`. The binary session type `S1` should be encapsulated in a `Send<T, S1>`. The body of the function sends the message of type `T` on the binary channel stored in the first field, `session1` (corresponding to the binary session
```rust
1 // Basic structure for MPST
2 pub struct SessionMpst< S1: Session, S2: Session, R: Role> {
3 pub session1: S1, pub session2: S, pub queue: R }
4
5 // Implementation of a communication function from the mpst-rust library
6 pub fn send mpst a to b<T, S1, S2, R>(x: T,
7 s: SessionMpst<Send<T, S1>, S2, RoleAtoB<R>>,) -> SessionMpst<S1, S2, R>
8 where T: ..., S1: Session, S2: Session, R: Role,
9 let new_session = send(x, s.session1);
10 let new_queue = next a to b(s.queue); ...
11
12 /// Offer a choice at A from C wrapped in an 'enum'
13 #[macro_export]
14 macro_rules! offer mpst a to c { ($session ... => {
15 let (l, s) = recv mpst a to c ($session)?; // receive a label l
16 cancel(s); // cancel the existing binary channels on s
17 match l { pat i => invoke...} // Call the associated function
18 // with a new SessionMpst
19 }
20
21 #[macro_export]
22 macro_rules! choose mpst c to all (s ...) {
23     ..// test for the choice condition ...and get the label l
24     let s = send mpst c to a (s, l); // send the label to A
25     let s = send mpst c to b (s, l), // send the label to B
26     cancel(s); // cancel the existing binary channels on s
27 // return new SessionMpst channel
28 ...
29
30 }
31
```

<caption>Listing 2: MPST Rust communication primitives</caption>

with role B), of the multiparty session s. Since the communication is on a binary channel, we reuse the binary send primitive from [9].

External and internal choices are implemented as macros that require an argument of type `SessionMpst`. The implementation of `offer mpst a to c` is given in lines 11–14. In essence, a choice is implemented as a broadcast from one role to the others. In our usecase, the active role that makes the choice is C. Hence, the macro `offer mpst a to c` explicitly performs a receive (`recv mpst a to c(s)`) on the session channel s. The received value is pattern matched and passed to any of the functions given as arguments to `offer mpst a to c`. Similarly, `choose-mpst c to all` in lines 19–26 is a macro that performs a select operation. The active role C sends the selected label to all roles in the protocol. In our particular example, C sends the selected label 1 to A and B.

**Discussions.** Our implementation, although intuitive, does not resolve the inherent conflict between Rust, which is *affine*, and session types, which are *linear*. The implementation suffers from the same drawback as [9]. However, the MPST methodology is a step forward in terms of usability. Differently than the Rust local types which can get convoluted, the syntax of global protocols is user-friendly and readable. Developers can use the global protocol as guidance, and hence avoid errors such as prematurely ending of a session. Moreover, as observed in Kokke's library [9], most of the errors are caused by misuse of methods and functions. Since we are code-generating the local types, the chance of mis-
spelling is significantly reduced. Another viable option for our framework is to
take the bottom-up approach: to check directly whether a set of manually-written
Rust local types satisfy safety/liveness properties by a model checker [14] or the
multiparty compatibility (a property which guarantees deadlock-freedom of com-
municating automata, which are equivalent to local session types) [11,2].

4 Related and Future Work

The Rust library in [8] implements binary session types, following [4]. It checks
at compile-time that the behaviours of two endpoint processes are dual, i.e the
processes are compatible. The library in [9], based on the EGV calculus by Fowler
et al [3], provides constructs for writing and checking binary session types, and
additionally supports exception handling constructs. We build on top of the
library in [9] since it offers several improvements in comparison to [8]. Most
importantly, the treatment of closing a channel prematurely in [8] may lead to
memory leaks. Both libraries suffer from a well-known limitation of binary session
types<fnref n="5" />. Notably, since deadlock-freedom is ensured only inside a session, a Rust
endpoint process, that communicates with more than one other process, is prone
to deadlocks and communication errors. Our framework solves that limitation
by expanding the scope of a session to multiple participants.

Our proposed design follows the methodology given by [6], which generates
Java communicating APIs from Scribble. This, and other multiparty session
types implementations, exploit the equivalence between local session types and
communicating automata to generate session types APIs for mainstream pro-
gramming languages (e.g., Java [6,10], Go [1], F# [13]). Each state from state
automata is implemented as a class, or in the case of [10], as a type state. To
ensure safety, state automata have to be derived from the same global specifi-
cation. All of the works in this category use the Scribble toolchain to generate
the state classes from a global specification and detect linearity violations at
runtime. This paper proposes the generation of protocol-specific APIs, which
promotes type checking of protocols at compile-time. This is done by projecting
the endpoints’ state space in those protocols to groups of channel types in the
desired language. In the future, we plan to implement the bottom-up approach,
in addition to the top-down approach outlined in this paper, as to compare their
productivity and scalability.

**Acknowledgement** The work has been partially supported by the following funding schemes VeTSS, EPSRC EP/K011715/1, EP/K034413/1, EP/L00058X/1, EP/N027833/1, EP/N028201/1, EP/T006544/1 and EP/T014709/1.

<footnote n="5">5 https://github.com/Munksgaard/session-types/issues/62</footnote>
References

1. Castro, D., Hu, R., Jongmans, S.S., Ng, N., Yoshida, N.: Distributed Programming Using Role Parametric Session Types in Go. In: 46th ACM SIGPLAN Symposium on Principles of Programming Languages. vol. 3, pp. 29:1–29:30. ACM (2019)

2. Deniélou, P.M., Yoshida, N.: Multiparty Compatibility in Communicating Automata: Characterisation and Synthesis of Global Session Types. In: 40th International Colloquium on Automata, Languages and Programming. LNCS, vol. 7966, pp. 174–186. Springer (2013)

3. Fowler, S., Lindley, S., Morris, J.G., Decova, S.: Exceptional asynchronous session types: Session types without tiers. Proc. ACM Program. Lang. 3(POLP), 28:1–28:29 (Jan 2019). https://doi.org/10.1145/3290341

4. Honda, K., Vasconcelos, V.T., Kubo, M.: Language primitives and type discipline for structured communication-based programming. In: European Symposium on Programming. pp. 122–138. Springer (1998)

5. Honda, K., Yoshida, N., Carbone, M.: Multiparty asynchronous session types. POPL 43(1), 273–284 (2008)

6. Hu, R., Yoshida, N.: Hybrid session verification through endpoint API generation. In: Stevens, P., Wasowski, A. (eds.) Fundamental Approaches to Software Engineering, vol. 9633, pp. 401–418. Springer Berlin Heidelberg (2016). https://doi.org/10.1007/978-3-662-49665-7_24, http://link.springer.com/10.1007/978-3-662-49665-7_24

7. Hunkeler, U., Truong, H.L., Stanford-Clark, A.: MQTT-SA publish/subscribe protocol for Wireless Sensor Networks. In: 2008 3rd International Conference on Communication Systems Software and Middleware and Workshops (COMSWARE’08). pp. 791–798. IEEE (2008)

8. Jespersen, T.B.L., Munksgaard, P., Larsen, K.F.: Session types for Rust. In: Proceedings of the 11th ACM SIGPLAN Workshop on Generic Programming. pp. 13–22. ACM (2015). https://doi.org/10.1145/2808098.2808100

9. Kokke, W.: Rusty Variation: Deadlock-free Sessions with Failure in Rust. In: Proceedings 12th Interaction and Concurrency Experience, ICE 2019, Copenhagen, Denmark, 20-21 June 2019. pp. 48–60 (2019). https://doi.org/10.4204/EPTCS.304.4, https://doi.org/10.4204/EPTCS.304.4

10. Kouzapas, D., Dardha, O., Perera, R., Gay, S.J.: Typechecking protocols with Mungo and StMungo. In: PPDP. pp. 146–159 (2016). https://doi.org/10.1145/2967973.2968595, http://doi.acm.org/10.1145/2967973.2968595

11. Lange, J., Yoshida, N.: Verifying Asynchronous Interactions via Communicating Session Automata. In: 31st International Conference on Computer-Aided Verification. LNCS, vol. 11561, pp. 117–97. Springer (2019)

12. Laumann, T.B., Jespersen, T.B.L., Munksgaard, P., Larsen, K.F., of Copenhagen, J.U., of Copenhagen, U., of Copenhagen, P.M.U., of Copenhagen, K.F.L.U.: Session types for rust (Aug 2015), http://dl.acm.org/citation.cfm?doid=2808098.2808100

13. Scalas, A., Dardha, O., Hu, R., Yoshida, N.: A Linear Decomposition of Multiparty Sessions for Safe Distributed Programming. In: 31st European Conference on Object-Oriented Programming. LIPIcs, vol. 74, pp. 24:1–24:31. Schloss Dagstuhl (2017)

14. Scalas, A., Yoshida, N.: Less Is More: Multiparty Session Types Revisited. In: 46th ACM SIGPLAN Symposium on Principles of Programming Languages. vol. 3, pp. 30:1–30:29. ACM (2019)
15. Steve Klabnik and Carol Nichols, with contributions from the Rust Community: The Rust Programming Language. 1.35.0 edn. (2019), https://doc.rust-lang.org/1.35.0/book/

16. Tu, T., Liu, X., Song, L., Zhang, Y.: Understanding real-world concurrency bugs in Go. In: ASPLOS. pp. 865–878. ACM (2019)

17. Yoshida, N., Gheri, L.: A very gentle introduction to multiparty session types. In: Hung, D.V., DSouza, M. (eds.) Distributed Computing and Internet Technology. pp. 73–93. Lecture Notes in Computer Science, Springer International Publishing (2020). https://doi.org/10.1007/978-3-030-36987-3_5

18. Yoshida, N., Hu, R., Neykova, R., Ng, N.: The Scribble protocol language. In: International Symposium on Trustworthy Global Computing. pp. 22–41. Springer (2013)