MobilityReadingGroup

π-calculus, Session Types research at Imperial College

𝝼scr
An implementation of MPST toolchain in OCaml

Multiparty session types (MPST) provide a typing discipline for message-passing concurrency, ensuring deadlock freedom for distributed processes. We present νScr (Nu-Scribble), an extensible toolchain, implemented in OCaml, for MPST-based protocols. The toolchain can convert multiparty protocols in the Scribble protocol description language into global types in the MPST theory; global types are projected into local types, and local types are converted to their corresponding communicating finite state machine (CFSM).

The toolchain also generates OCaml APIs from CFSMs, which implement endpoints in the protocol. Our design allows for language-independent code generation, and opens possibilities to generate APIs for other programming languages. We design our toolchain with modularity and extensibility in mind, so that extensions of core MPST can be easily integrated within our framework.