Repository logo
  • Log In
    Log in via Symplectic to deposit your publication(s).
Repository logo
  • Communities & Collections
  • Research Outputs
  • Statistics
  • Log In
    Log in via Symplectic to deposit your publication(s).
  1. Home
  2. Faculty of Engineering
  3. Computing
  4. Computing
  5. Multiparty session programming with global protocol combinators
 
  • Details
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
URI
http://hdl.handle.net/10044/1/79725
DOI
https://www.dx.doi.org/10.4230/LIPIcs.ECOOP.2020.9
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
http://creativecommons.org/licenses/by/4.0/
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
About
Spiral Depositing with Spiral Publishing with Spiral Symplectic
Contact us
Open access team Report an issue
Other Services
Scholarly Communications Library Services
logo

Imperial College London

South Kensington Campus

London SW7 2AZ, UK

tel: +44 (0)20 7589 5111

Accessibility Modern slavery statement Cookie Policy

Built with DSpace-CRIS software - Extension maintained and optimized by 4Science

  • Cookie settings
  • Privacy policy
  • End User Agreement
  • Send Feedback