Multiparty session programming with global protocol combinators
File(s)LIPIcs-ECOOP-2020-9.pdf (925.23 KB)
Published version
Author(s)
Imai, Keigo
Neykova, Rumyana
Yoshida, Nobuko
Yuen, Shoji
Type
Conference Paper
Abstract
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.
Date Issued
2020-11-06
Date Acceptance
2020-04-08
Citation
LIPIcs : Leibniz International Proceedings in Informatics, 2020, 166, pp.9:1-9:30
ISSN
1868-8969
Publisher
Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
Start Page
9:1
End Page
9:30
Journal / Book Title
LIPIcs : Leibniz International Proceedings in Informatics
Volume
166
Copyright Statement
© 2020 Keigo Imai, Rumyana Neykova, Nobuko Yoshida, and Shoji Yuen; licensed under Creative Commons License CC-BY
License URL
Sponsor
Engineering & Physical Science Research Council (E
Engineering & Physical Science Research Council (E
Engineering and Physical Sciences Research Council
Engineering & Physical Science Research Council (EPSRC)
Engineering & Physical Science Research Council (EPSRC)
Engineering & Physical Science Research Council (E
Engineering & Physical Science Research Council (EPSRC)
Engineering & Physical Science Research Council (EPSRC)
Engineering & Physical Science Research Council (EPSRC)
The National Cyber Security Centre (NCSC)
Grant Number
ERI 025567 (EP/K034413/1)
PO 20131167
EP/L00058X/1, PO 20131167
EP/K011715/1
EP/N027833/1
20208624
EP/T006544/1
EP/T014709/1
n/a
4214176 / RFA 20601
Source
34th European Conference on Object-Oriented Programming
Publication Status
Published
Start Date
2020-07-13
Finish Date
2020-07-17
Coverage Spatial
Berlin, Germany
Date Publish Online
2020-11-06