Multiparty Session Programming with Global Protocol Combinators
Sun 15 Nov 2020 17:40 - 18:00 at SPLASH-I - S-6 Chair(s): Shigeru Chiba, Tiark Rompf
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 of 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.
Sun 15 Nov Times are displayed in time zone: Central Time (US & Canada) change
17:00 - 18:20: S-6Research Papers at SPLASH-I +12h Chair(s): Shigeru ChibaThe University of Tokyo, Tiark RompfPurdue University | |||
17:00 - 17:20 Talk | Static Race Detection and Mutex Safety and Liveness for Go Programs Research Papers Link to publication DOI Media Attached | ||
17:20 - 17:40 Talk | Reference immutability for DOT Research Papers Link to publication DOI Media Attached | ||
17:40 - 18:00 Talk | Multiparty Session Programming with Global Protocol Combinators Research Papers Keigo ImaiGifu University, Rumyana NeykovaBrunel University London, Nobuko YoshidaImperial College London, Shoji YuenNagoya University Link to publication DOI Media Attached | ||
18:00 - 18:20 Talk | Scala with Explicit Nulls Research Papers Abel NietoAarhus University, Yaoyu ZhaoUniversity of Waterloo, Ondřej LhotákUniversity of Waterloo, Angela ChangUniversity of Waterloo, Justin PuUniversity of Waterloo Link to publication DOI Pre-print Media Attached |
Mon 16 Nov Times are displayed in time zone: Central Time (US & Canada) change
05:00 - 06:20: S-6Research Papers at SPLASH-I Chair(s): Jeremy GibbonsDepartment of Computer Science, University of Oxford, Olivier FlückigerNortheastern University | |||
05:00 - 05:20 Talk | Static Race Detection and Mutex Safety and Liveness for Go Programs Research Papers Link to publication DOI Media Attached | ||
05:20 - 05:40 Talk | Reference immutability for DOT Research Papers Link to publication DOI Media Attached | ||
05:40 - 06:00 Talk | Multiparty Session Programming with Global Protocol Combinators Research Papers Keigo ImaiGifu University, Rumyana NeykovaBrunel University London, Nobuko YoshidaImperial College London, Shoji YuenNagoya University Link to publication DOI Media Attached | ||
06:00 - 06:20 Talk | Scala with Explicit Nulls Research Papers Abel NietoAarhus University, Yaoyu ZhaoUniversity of Waterloo, Ondřej LhotákUniversity of Waterloo, Angela ChangUniversity of Waterloo, Justin PuUniversity of Waterloo Link to publication DOI Pre-print Media Attached |