Multiparty Session Programming with Global Protocol Combinators
| Autor: | Imai, Keigo, Neykova, Rumyana, Yoshida, Nobuko, Yuen, Shoji |
|---|---|
| Přispěvatelé: | Engineering & Physical Science Research Council (E, Engineering and Physical Sciences Research Council, Engineering & Physical Science Research Council (EPSRC), The National Cyber Security Centre (NCSC) |
| Rok vydání: | 2020 |
| Předmět: |
FOS: Computer and information sciences
Computer Science - Programming Languages Software and its engineering → Functional languages OCaml Software and its engineering → Concurrent programming structures Communication Protocol Concurrent and Distributed Programming Theory of computation → Type structures Multiparty Session Types Software and its engineering → Polymorphism Programming Languages (cs.PL) |
| Zdroj: | 34th European Conference on Object-Oriented Programming 9:30 9:1 |
| DOI: | 10.48550/arxiv.2005.06333 |
| Popis: | 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. LIPIcs, Vol. 166, 34th European Conference on Object-Oriented Programming (ECOOP 2020), pages 9:1-9:30 |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|