2026-07-22T04:53:00Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:13166 2024-03-06T10:49:53Z ddc:004 open_access

Multiparty Session Programming With Global Protocol Combinators Imai, Keigo Neykova, Rumyana Yoshida, Nobuko Yuen, Shoji Multiparty Session Types Communication Protocol Concurrent and Distributed Programming OCaml Multiparty Session Types (MPST) is a typing discipline for communication protocols. It ensures the absence of communication errors and deadlocks for well-typed communicating processes. The state-of-the-art implementations of the MPST theory rely on (1) runtime linearity checks to ensure correct usage of communication channels and (2) external domain-specific languages for specifying and verifying multiparty protocols. To overcome these limitations, we propose a library for programming with global combinators - a set of functions for writing and verifying multiparty protocols in OCaml. Local behaviours for all processes in a protocol are inferred at once from a global combinator. We formalise global combinators and prove a sound realisability of global combinators - a well-typed global combinator derives a set of local types, by which typed endpoint programs can ensure type and communication safety. Our approach enables fully-static verification and implementation of the whole protocol, from the protocol specification to the process implementations, to happen in the same language. We compare our implementation to untyped and continuation-passing style implementations, and demonstrate its expressiveness by implementing a plethora of protocols. We show our library can interoperate with existing libraries and services, implementing DNS (Domain Name Service) protocol and the OAuth (Open Authentication) protocol. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Keigo Imai and Rumyana Neykova and Nobuko Yoshida and Shoji Yuen 2020 Is Part Of LIPIcs, Volume 166, 34th European Conference on Object-Oriented Programming (ECOOP 2020) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ECOOP.2020.9 urn:nbn:de:0030-drops-131662 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2020.9 eng https://creativecommons.org/licenses/by/3.0/legalcode