Verifying Multiparty Communication Protocols using ML Type Systems
We show ocaml-mpst, a library for safe concurrent programming in OCaml based on Multiparty Session Types (MPST). The key feature is global combinators, a typed, embedded DSL for specifying the protocol of a system of interacting processes. Such protocols are checked statically; thus, unsafe concurrent behaviour can be detected as a type error by the OCaml compiler. Until now, most MPST implementations use external domain-specific protocol description languages and tools (e.g. the Scribble toolchain), as MPST protocols are considered far from the types of a mainstream programming language. We utilise parametric polymorphism in ML and row polymorphism in OCaml in particular, achieving the one-stop platform for concurrent programming in a general-purpose language with industrial strength. The library ocaml-mpst is first presented at ECOOP 2020. This manuscript also introduces a use-case of protocol reuse utilising row polymorphism and shows recent development of ocaml-mpst, discussing the effectiveness of the approach and future work.
Extended Abstract (ml2021-submitted.pdf) | 416KiB |
Slides (ml2021-slides.pdf) | 1.17MiB |
Thu 26 AugDisplayed time zone: Seoul change
23:30 - 01:00 | |||
23:30 30mTalk | A metalanguage for multi-phase modularity ML File Attached | ||
00:00 30mTalk | Unfolding ML datatype declarations without loops ML Pre-print Media Attached | ||
00:30 30mTalk | Verifying Multiparty Communication Protocols using ML Type Systems ML Keigo Imai Gifu University, Rumyana Neykova Brunel University London, Nobuko Yoshida Imperial College London, Shoji Yuen Nagoya University File Attached |