Keywords

1 Introduction

In the modern era of distributed and concurrent programming, how to achieve safety with minimal effort (i.e. lightweight formal methods) becomes a hot area of research. Session types [19] provide a typing discipline for message passing concurrency, by assigning session types to communication channels, in terms of a sequence of actions over a channel. Session types, initially only able to describe communications between two ends of a channel, are later extended to multiparty [20, 21], giving rise to the multiparty session types (MPST) theory. The MPST typing discipline guarantees that a set of well-typed communicating processes are free from deadlocks or communication mismatches.

1.1 Communicating Finite State Machines and Session Types

Motivation: Why CFSMs? Communicating Automata [2], also known as Communicating Finite State Machines (CFSMs), are a classical model for protocol specification and verification. Before being used in many industrial contexts, CFSMs have been a pioneer theoretical formalism, in which distributed safety properties could be formalised and studied.

Establishing a formal connection between CFSMs and session types allows the use of CFSMs to build theoretically well-founded tools for MPST. The first work that utilised CFSMs in practice is Demangeon et al. [11], a toolchain for monitoring multiparty communications at runtime for large scientific cyber-infrastructures developed by the Ocean Observatories Initiative [41].

From the theoretical side, the CFSM framework offers canonical justifications for session types to answer open questions which have been asked since [20]. The 1st question is about expressiveness: to which class of CFSMs do session types correspond? The 2nd question concerns the semantic correspondence between session types and CFSMs: how do the safety properties that session types guarantee relate to those of CFSMs? The 3rd question is about efficiency: why do session types provide efficient algorithms for type-checking or verifying distributed programs, while general CFSMs are undecidable? CFSMs can be also seen as generalised endpoint specifications, therefore an excellent target for a common ground for comparing protocol specification languages.

To answer the three questions above, we need to identify a sound and complete subset of CFSMs that corresponds to MPST behaviour, which we explain below.

Fig. 1.
figure 1

Two dual communicating automata: the buyer and the seller

Full size image

Binary Session Types as CFSMs. The subclass that fully characterises binary session types [19] was actually proposed by Gouda, Manning and Yu [16] in a pure automata context (independently from the discovery of session types [45]). Consider a simple business protocol between a Buyer and a Seller. From the Buyer’s viewpoint, the Buyer sends the title of a book, then the Seller answers with a quote. If the Buyer is satisfied by the quote, then they send their address and the Seller sends back the delivery date; otherwise they retry the same conversation. This can be specified by the two machines of the Buyer and the Seller in Fig. 1. We can observe that these CFSMs satisfy three conditions: First, the communications are deterministic: messages that are part of the same choice, ok and retry here, are distinct. Secondly, there is no mixed state (each state has either only sending actions, or only receiving actions). Third, these two machines have compatible traces (i.e. dual): the Seller machine can be defined by exchanging sending and receiving actions of the Buyer machine. Breaking one of these conditions allows deadlock situations and breaking one of the first two conditions makes the compatibility checking undecidable [16].

Essentially, the same characterisation is given in binary session types [19]. Consider the following session type of the Buyer.

(1)

The session type above describes the communication pattern using several constructs. The operator denotes an output of the title, whereas denotes an input of a quote. The output choice features the two options ok and retry and . denotes sequencing. \(\texttt {end}\) represents the termination of the session, and \(\mu \mathbf {t}\) is recursion. The simplicity and tractability of binary sessions come from the notion of duality in interactions [15], which corresponds to compatibility of CFSMs. In (1), not only the Buyer’s behaviour, but also the whole conversation structure is already represented in this single type: the interaction pattern of the Seller is fully given as the dual of the type in (1) (exchanging input \(\oplus \) and output &). When composing two parties, we only have to check they have mutually dual types, and the resulting communication is guaranteed to be deadlock-free.

Multiparty Session Types and CFSMs. The notion of duality is no longer effective in multiparty communication, where the whole conversation cannot be reconstructed from only the behaviour of a single machine. Instead of directly trying to decide whether the communication of a system satisfies safety (which is undecidable in the general case), we devise a compatible, decidable condition of a set of machines, which forces them to collaborate together. We define a complete characterisation of global type behaviours into CFSMs: a set of CFSMs satisfy some compatible conditions, if and only if the CFSMs can mimic the expected behaviour of a given global type. A good global type means the global type can only generate safe CFSMs by endpoint projection, which satisfies realisability.

Fig. 2.
figure 2

CFSMs for the commit protocol

Full size image

We give a simple example to illustrate the proposal. The Commit protocol in Fig. 2 involves three machines: Alice, Bob and Carol. Alice orders Bob to act or quit. If act is sent, Bob sends a signal to Carol, and Alice sends a commitment to Carol and continues. Otherwise Bob informs Carol to save the data, and Alice gives the final notification to Carol to finish the protocol.

Deniélou and Yoshida [12] present a decidable notion of multiparty compatibility as a generalisation of duality of binary sessions, for a given set of (more than two) CFSMs. The idea is that any single machine can see the rest of the machines as a single machine, up to unobservable actions (like a \(\tau \)-transition in CCS). Therefore, we check the duality between each automaton and the rest, up to internal communications (1-bounded executions in the terminology of CFSMs) that the other machines will independently perform. For example, in Fig. 2, to check the compatibility of trace \(\texttt {AB}!\texttt {quit}\cdot \texttt {AC}!\texttt {finish}\) in Alice, we observe the dual trace \(\texttt {AB}?\texttt {quit}\cdot \texttt {AC}?\texttt {finish}\) from Bob and Carol, executing the internal communication between Bob and Carol: \(\texttt {BC}!\texttt {save}\cdot \texttt {BC}?\texttt {save}\). If this extended duality is valid for all the machines from any 1-bounded reachable state, then they satisfy multiparty compatibility and can characterise a well-formed global type.

Our motivation to study this general compatibility comes from the need for using global types to develop tools for choreographic distributed testing in web service software [44] and distributed monitoring for large cyber-infrastructures [41], where local specifications are often updated independently and one needs to refine the original global specification according to the local updates.

The 1-boundedness and multiparty compatibility conditions are extended to the k-bounded condition in [28] (called k-multiparty compatibility). Another flexible form of safe and more asynchronous CFSMs (which do not rely on duality or buffer bounds) is studied in [7, 14] (called asynchronous subtyping). Unfortunately, the asynchronous subtyping relation is undecidable, even if limited to only two machines; currently its decidable sound algorithms are restricted to either binary session types [3] or finite MPSTs [6].

Practically, a direct analysis based on CFSMs is computationally expensive, even if the shapes of CFSMs are limited. For building a toolchain for practical programming languages, we take the safe-by-construction approaches—we start from specifying a global type, and project it to endpoint types or CFSMs, for code generation into various programming languages, and/or other purposes. Interestingly, multiparty compatibility also helps enlarge the well-formedness condition of global types [23]. See Sect. 5.

1.2 \(\nu \text {S}\textsc {cr}\): An Extensible Toolchain for Multiparty Session Types

We present a new toolchain for multiparty protocols, \(\nu \text {S}\textsc {cr}\) (NuScr), for handling protocols written in the Scribble language. The implementation of MPST has three main aspects: (1) a language for specifying global interactions—specifically, the Scribble protocol description language [18]; (2) a tool to manipulate specifications and generate implementable APIs (Scribble  [44] is already a mature industrial-strength tool able to generate APIs in multiple programming languages); and (3) a theory backing the safety guarantees, such as Featherweight Scribble  [35], which minds the gap between the practical Scribble protocol description language, and the theoretical MPST specifications [21].

The aim of this implementation is to be lightweight and extensible. Whilst the Scribble language describes more expressive protocols than the original MPST theory [21], \(\nu \text {S}\textsc {cr}\) handler a core, well-defined subset of Scribble protocols that have a corresponding MPST global type, following the formalisation of [35]. We do so in anticipation that further extensions of the MPST theory can be easily implemented in \(\nu \text {S}\textsc {cr}\), and a researcher can smoothly integrate their own MPST design/theory in \(\nu \text {S}\textsc {cr}\). For this purpose, we use a modular design that does not only enable future extensions, but also makes them easy to implement.

The rest of the paper is structured as follows: Sect. 2 introduces multiparty session types, the theoretical foundation of our tool; Sect. 3 introduces the \(\nu \text {S}\textsc {cr}\) toolchain; Sect. 4 presents a case study of extending \(\nu \text {S}\textsc {cr}\) with nested protocols [10]; and Sect. 5 summarises related work and concludes this paper. \(\nu \text {S}\textsc {cr}\) is publicly available at https://github.com/nuscr/nuscr/ under the GPLv3 license.

2 Multiparty Session Types (MPST)

In this section, we introduce the theoretical foundation of our tool—Multiparty Session Types (MPST) [21], a typing discipline for concurrent processes.

Fig. 3.
figure 3

Top-down methodology

Full size image

The main design philosophy of MPST follows a top-down approach (see Fig. 3): a global type describes a global view of a communication protocol between a number of participants. Each participant has their own perspective of the protocol, prescribed by their local type, which are obtained via an operation called projection. A local type for a participant can be used for code generation or type-checking to ensure that the participating process follows the local type. If all participating processes follow their corresponding local types, obtained via projection from a global type, these processes are free from communication mismatches or deadlocks, guaranteed by the MPST typing discipline.

Global and Local Types. We show the syntax of global types and local types in Fig. 4. The global type \(\texttt {p} \rightarrow \texttt {q}\left\{ l_i(S_i). G_i\right\} _{i \in I}\) is a message from \(\texttt {p}\) to \(\texttt {q}\), where \(\texttt {p} \ne \texttt {q}\) and \(I \ne \emptyset \). The message carries a label \(l_i\) and payload type \(S_i\), selected from a non-empty index set I, and the protocol continues as \(G_i\). We write \(\texttt {p} \rightarrow \texttt {q}:l(S).G\) when \(|I| = 1\). \(\texttt {end}\) denotes a type that is terminated. The local type (resp. ) denotes an external choice (resp. internal choice), where participant carrying this local type will receive (resp. send) a message from (resp. to) the participant \(\texttt {p}\), among the index set I. Recursive types are realised by \(\mu \mathbf {t}{.}G\) (resp. ) and \(\mathbf {t}\), by taking a equi-recursive view (However, we require types to be contractive, e.g. \(\mu \mathbf {t}{.}\mathbf {t}\) is not allowed).

We can obtain local types by projecting a global type upon a participant. Projection is defined as a partial function, since not all global types are implementable—these types might be unable to be implemented in a type-safe way. We say a global type is well-formed, if the projection of the global type upon all participants are defined. Well-formed global types can be implemented by a collection of concurrent processes, each implementing their projected local type. Well-typed processes will enjoy the benefit of the MPST typing discipline, are free from deadlocks or communication mismatches. Curious readers may refer to [48] for more details.

Fig. 4.
figure 4

Syntax of multiparty session types, in the style of [48]

Full size image

From Local Types to Communicating Finite State Machines. A local type describes the behaviour of a specific role in a given global type, which can be represented by a communicating finite state machineFootnote 1 (CFSM) [2]. As shown by Deniélou and Yoshida [12] and Neykova and Yoshida [35], there is an algorithm to construct a CFSM that is trace-equivalent to the local type.

Relation to Scribble. Scribble  [44, 49] is a toolchain for implementing multiparty protocols. In particular, the syntax of the Scribble protocol description language correlates closely to the theory of MPST. Neykova and Yoshida [35] give a formal description of the Scribble protocol description language, known as Featherweight Scribble, and establish a correspondence between global protocols in Featherweight Scribble and global types in the MPST theory (Sect. 4).

3 \(\nu \text {S}\textsc {cr}\): An Extensible Implementation of Multiparty Session Types in OCaml

In this section, we describe the structure of \(\nu \text {S}\textsc {cr}\) and highlight the correspondence to the multiparty session type theory. \(\nu \text {S}\textsc {cr}\) is written in OCaml in around 8000 lines of code, implementing the core part of the Scribble language, with various extensions to the original MPST. \(\nu \text {S}\textsc {cr}\) also has a web interface (https://nuscr.dev/), so that users can perform quick prototyping in browsers, saving the need for installation (see Fig. 5 for a screenshot).

Fig. 5.
figure 5

A screenshot of the \(\nu \text {S}\textsc {cr}\) web interface, showing an Adder protocol

Full size image

Overview. \(\nu \text {S}\textsc {cr}\) is designed to be extensible, so that researchers working on MPST theories can find it easy to implement their extensions upon the code base of \(\nu \text {S}\textsc {cr}\). Inspired by Haskell, we use language pragmas to control language extensions, so that users do not need to download different versions of the software for different language extensions. Currently, two major extensions are implemented, namely nested protocols [10, 13] and refinement types [51]. Protocols in the Scribble description language are accepted by \(\nu \text {S}\textsc {cr}\), and then converted into an MPST global type.

From a global type, \(\nu \text {S}\textsc {cr}\) is able to project upon a specified participant to obtain their local type, and subsequently obtain the corresponding CFSM. Moreover, \(\nu \text {S}\textsc {cr}\) is able to generate code for implementing the participant in various programming languages, from their local type or CFSM. \(\nu \text {S}\textsc {cr}\) can be used either as a standalone command line application, or as an OCaml library for manipulating multiparty protocols.

Code Layout. The codebase of \(\nu \text {S}\textsc {cr}\) can be briefly split into 4 components: syntax, mpst, codegen and utils. We introduce the components in detail.

Syntax. The syntax component handles the syntax of the Scribble protocol description language, the core part of which is shown in Fig. 6. We use OCamllex and Menhir to generate the lexer and parser respectively. A Scribble module consists of multiple protocol declarations P. In the syntax, protocol names are represented by p, role names by r, label names by l, and recursion variable names by X. The four kinds of names range over string identifiers. They are separated in distinct name spaces in \(\nu \text {S}\textsc {cr}\), and appropriately distinguished.

Fig. 6.
figure 6

Syntax of core Scribble language

Full size image
Fig. 7.
figure 7

Adder protocol and its corresponding global type

Full size image

As a running example, we show a simple Scribble protocol describing an Adder protocol in Fig. 7a, where a Client is able to make various requests to add two ints, before they decide to finish the protocol with a bye message.

Multiparty Session Types. We show the key pipeline of handling multiparty session types in Fig. 8, implemented in the mpst component. An input file is parsed into a Scribblemodule, by the syntaxtree component described in the previous paragraph. The protocols are then converted into a global type (defined in Gtype module), which describes an overall protocol between multiple roles. A global type is projected into a local type (defined in Ltype module), given a specified role, which describes the local communication behaviour. We construct a corresponding communicating finite state machine (CFSM) [2] (defined in Efsm module) for the local type, and it can be used for API generation.

To obtain a global type, we extract it from the syntax tree of the Scribble protocol file. During this extraction process, we perform syntactic checks on the protocol, e.g. validating whether role names, recursion variables, and protocol names have been defined before they are used. We show the global type of the Adder protocol in Fig. 7b.

It is important to note that, syntactically correct protocols may fall out of the expressiveness of the original MPST theory, e.g. the protocol shown in Fig. 9. The role A makes a choice of sending Foo to B first, or sending Bar to C first, which has no corresponding construct in the syntax (Fig. 4). Whilst some protocols fall out of the scope of the core MPST theory, an extension to the core theory may accept such protocols with non-directed choices.

Fig. 8.
figure 8

Workflow of \(\nu \text {S}\textsc {cr}\)

Full size image
Fig. 9.
figure 9

Non-directed choice in Scribble

Full size image

The projection from global types upon participants is implemented in the Ltype module, and the projected local types can be converted into their corresponding communicating automata, using the technique described in [12]. We use the graph library OCamlgraph [8], to represent the CFSM as a directed graph. We show the local type for Client in Fig. 10a, and its corresponding CFSM in Fig. 10b. Both local types and communicating automata can be used for code generation purposes, which will be introduced in the next paragraph.

Code Generation. The codegen component generates APIs for implementing distributed processes using the MPST theory. Following the MPST design methodology, processes should follow the projected local type from the prescribed global type. By the means of code generation, the processes implemented using generated APIs will be correct by construction.

Currently, \(\nu \text {S}\textsc {cr}\) supports code generation in OCaml, Go (with the nested protocol extension [13]) and F\(\star \) (with the refinement type extension [51]). Moreover, \(\nu \text {S}\textsc {cr}\) can export the CFSM as a GraphViz Dot file, and code generation backends can be implemented separately from \(\nu \text {S}\textsc {cr}\). This approach has been used to support code generation in Rust [9], Scala and TypeScript [31].

To generate code in OCaml, we use a CFSM-based generation technique, as proposed in [22]; however, we do not follow the class-based APIs, i.e. states in the CFSMs are classes, and state transitions are methods on classes in [22]. While it would be possible to implement a similar object oriented approach in OCaml, it does not fit well in the functional programming paradigm. \(\nu \text {S}\textsc {cr}\) uses a callback-based approach [51] for API generation, and generates functions for transitions and maintains the state internally in a finite state machine runner.

Fig. 10.
figure 10

Local type and CFSM for role C in the Adder protocol

Full size image
Fig. 11.
figure 11

Generated module type in OCaml for role C

Full size image

API Style. The generated API separates the program logic and communication aspects of the endpoint program, in contrast to existing approaches of code generation [22]. We generate type signatures of callback functions, corresponding to state transitions in the CFSM, for handling the program logic. The signatures are collected in the form of a module type, named Callbacks. We show the generated module signature in Fig. 11, for implement the Client in the Adder protocol (Fig. 10). Since we use a graph representation for CFSMs, the generation process is done by iterating through the edges of the graph.

For a complete endpoint, We generate an OCaml functor taking a module of type Callbacks to an implementation module. The module exposes a runner, which executes the CFSM when provided connections to other communicating roles. The runner handles the communication with other roles, so that the callback module does not need to involve any sending and receiving primitives.

Optional Monadic APIs. To enable asynchronous execution, we optionally generate code compatible with monadic communication primitives. This allows users to implement the endpoint program with popular asynchronous execution libraries in OCaml, such as Lwt [40].

Utilities. The utils component contain miscellaneous modules fulfilling various utility functions. A few notable modules in this component, relevant to future extensions of \(\nu \text {S}\textsc {cr}\), include:

  • Names module defines separated namespaces for all kinds of names occurring in global and local types, e.g. payload type names, payload label names, recursion variable names, etc.

  • Err module defines all kinds of errors that occur throughout all components.

  • Pragma module defines language pragmas, controlling the enabled extensions.

4 Extending \(\nu \text {S}\textsc {cr}\)

The modular design of \(\nu \text {S}\textsc {cr}\) allows extensions of the MPST theory to be implemented easily. The language pragmas, implemented as a special comment at the beginning of an input file, control which extensions are enabled when handling the protocols. So far, two major extensions have been added to \(\nu \text {S}\textsc {cr}\): nested protocols implemented by Echarren Serrano [13], and refinement types implemented by Zhou et al. [51]; and additional extensions are being implemented: choreography automata [1] by Neil Sayers, parallel types by Francisco Ferreira, and crash handling by Adam D. Barwell.

We use the nested protocol extension by Echarren Serrano [13] as a case study to demonstrate how an extension can be implemented in \(\nu \text {S}\textsc {cr}\). Nested protocols [10] allow dynamic creation of participants and sub-sessions in a protocol, extending the expressiveness of global types. In Fig. 12, we show a fork join protocol, described in Scribble with the nested protocol extension.

Fig. 12.
figure 12

A nested fork join protocol in Scribble  [13, Fig. 7.3]

Full size image

Creating a New Pragma. The first line of Fig. 12 enables the nested protocols extension using the pragma NestedProtocols (wrapped in (*# #*)). New pragmas are added in the Pragma module in the utils component, including a new constructor for the new pragma, and functions to get and set whether the extension is toggled. An implementer may also check for conflicting pragmas when processing all pragmas, so that incompatible extensions are not enabled at the same time. In order to preserve the behaviour when the extension is not enabled, it is essential that subsequent implementations of the extension should query whether the extension is enabled before proceeding.

Extending the Syntax. The extension allows nested protocols to be defined using the keyword , with the possibility to dynamically create new participating roles. In addition, a new construct is introduced to create a sub-session that follows a nested protocol, where new roles may be created to participate in the sub-session.

To implement these new syntactic constructs, an implementer should extend the syntaxtree component. To begin with, the concrete syntax tree (in the Syntax module) is to be extended with constructors for the new syntax, e.g. the new calls constructs in protocol body. Additional lexing or parsing rules should be added accordingly in the corresponding module.

Extending the MPST Theory. The crucial part is to implement the theory extension in the mpst component, where global and local types are defined. Within the component, global (resp. local) types are defined using the OCaml type Gtype.t (resp. Ltype.t). We add new constructors for new global types (CallG for protocol calls) and new local types (InviteCreateL for inviting and creating dynamic roles, and AcceptL for accepting invitations). Projection can be extended accordingly in the Ltype module, which we will not explain in detail.

However, extending the global and local types does not complete the extension—the implementer needs to connect the concrete syntax of Scribble global protocols to the abstract syntax of MPST global types. The extraction is defined at Gtype.of_protocol, where a global type is obtained from a global protocol. When processing the new syntactic constructs added by the extension, the implementer should remember to call Pragma.nested_protocol_enabled (which will return true when the pragma is set) to avoid interference with the core MPST, i.e. when the extension is not enabled.

Extending the Code Generation. Section 3 describes OCaml code generation from CFSMs. However, constructing CFSMs for nested protocols is an open problem. Hence, for this extension the Go code generation is instead based on local types. \(\nu \text {S}\textsc {cr}\) code generation backends in the codegen component is free to choose any representation in the mpst component, so implementers may pick whichever representation that suits best their code generation approach.

The generated Go APIs also use callbacks, and the message passing primitives in Go with channels and concurrent execution with goroutines fit the setup of session types very well. The code generator creates type definitions for different channels used in the communication, message exchanges, and callbacks. New participants in the protocol can be spawned when needed using goroutines.

5 Related and Future Work

Non-Scribble-Based MPST Implementations. Scalas and Yoshida [43] (accompanying artefact) implement a toolkit for analysing synchronous multiparty protocols. The underlying theory for this tool is the generalised multiparty session types, where the type system is parameterised on a safety property. The toolkit uses a model checker (mCRL2 [46]) to decide whether the desired safety property holds. A shortcoming of this approach is that (1) the verification power is bound by the model checker—for example, mCRL2 allows to verify only finite-controlled local session types (no parallel compositions under recursion) and cannot verify channel passing; and (2) the approach is not scalable to asynchronous communication with unbounded buffers (as safety becomes undecidable). Several prototype tools that analyse safety of general forms of local types (or CFSMs) are developed in the context of multiparty CFSMs [27, 28] and binary CFSMs [3]. The tool in [27] enables a bottom-up approach, which builds a global type from a set of safe local types. These approaches are, in general, high in complexity (requiring a global analysis to a set of CFSMs), and difficult to integrate with real programming languages because of the need to extract local types from source languages. For example, Ng and Yoshida [38] develop a tool (based on [27]) to build a global graph from local session types extracted from Go source codes, in order to check deadlock-freedom. Only a subset of Go syntax is supported [50].

Our top-down approach is based on the original, less general multiparty session type theory, yet we implement an extensible toolchain with possibilities to generate OCaml code for execution. Imai et al. [24] implement multiparty session types in OCaml with protocol combinators, whereas our approach takes inputs from Scribble protocols. Their tool uses features such as variant and object types in OCaml to encode external and internal choices in the local types, and supports session delegation. Our callback-based approach does not support delegation, but also does not require sophisticated type system features.

For more advanced applications of MPST, global types with motion primitives of Cyber Physical Systems [29, 30] provide a collision freedom guarantee for concurrent robotics applications. Castro-Perez and Yoshida [6] use global types to uniformly predict communication costs of parallel algorithms and distributed protocols implemented in different languages.

Scribble -Based MPST Implementations and Extensions. The Scribble toolchain provides a language-agnostic description language for multiparty protocols, targeting a variety of programming languages: Java [22], Scala [42], Go [4], TypeScript [31], PureScript [25], Rust [9, 26], F\(\sharp \) [32], F\(\star \) [51], Erlang [33], Python [11, 34], MPI-C [36, 37], C [39], etc.

The Scribble toolchain describes multiparty protocols, including some that are not expressible in the MPST theory, e.g. the constructs in Scribble name a role making an internal choice, whereas the MPST global type has form \(\texttt {p} \rightarrow \texttt {q}\left\{ l_i(S_i). G_i\right\} \), where two roles are named. The protocol in Fig. 9 is expressible in Scribble, although not in the core MPST theory we implement.

The Scribble toolchain implements a number of extensions of MPST, e.g. explicit connections [23], interruptible protocols [11]. \(\nu \text {S}\textsc {cr}\) implements the core MPST theory by our design choice, so that extensions of the MPST theory can be easily implemented, with the usual syntactical projections. Whilst the Scribble toolchain uses model checking and other validation techniques to verify the safety of the multiparty protocol to enlarge well-formedness, the same technique might not be applicable when extending the original MPST [21]. \(\nu \text {S}\textsc {cr}\) keeps an underlying core syntax and its validation faithful to the literature, so that other users can easily integrate their own MPST theory. We demonstrate our extensibility via the case study with nested protocols.

Besides the Scribble toolchain itself, Voinea et al. [47] provide a tool, StMungo, to translate a Scribble multiparty protocol to a typestate specification in Java. The typestate specification can be checked via Mungo, a static typechecker for typestates in Java. Developers can use the generated typestate APIs to implement the multiparty protocol safely. Harvey et al. [17] use the Scribble toolchain with explicit connections [23] to develop a tool for affine multiparty session types with adaptations.

Future Work. Recently, Castro-Perez et al. [5] propose Zooid, a domain specific language for certified multiparty communication, embedded in Coq and implemented atop their mechanisation framework of asynchronous MPST. For future work, we would like to produce a certified version of Scribble —CertiScr, extending the Zooid framework, for the core of \(\nu \text {S}\textsc {cr}\). We would like to mechanise the extraction process from Scribble to global types in [5], and the CFSM construction process from local types in Coq, completing the picture of fully mechanised toolchain from Scribble protocols to CFSMs. The Coq code can then be extracted into OCaml to produce a formally verified \(\nu \text {S}\textsc {cr}\) core.