Imperial College London
Professor Nobuko Yoshida

ProfessorNobukoYoshida

Faculty of Engineering, Department of Computing

Academic Visitor
 
 
 
//

Contact

 

+44 (0)20 7594 8240n.yoshida Website

 
 
//

Location

 

556Huxley BuildingSouth Kensington Campus

//

Summary

 

Publications

Citation

BibTex format

@inproceedings{Imai:2020:10.4230/LIPIcs.ECOOP.2020.9,
author = {Imai, K and Neykova, R and Yoshida, N and Yuen, S},
doi = {10.4230/LIPIcs.ECOOP.2020.9},
pages = {9:1--9:30},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik},
title = {Multiparty session programming with global protocol combinators},
url = {http://dx.doi.org/10.4230/LIPIcs.ECOOP.2020.9},
year = {2020}
}
Download

RIS format (EndNote, RefMan)

TY  - CPAPER
AB  - 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.
AU  - Imai,K
AU  - Neykova,R
AU  - Yoshida,N
AU  - Yuen,S
DO  - 10.4230/LIPIcs.ECOOP.2020.9
EP  - 1
PB  - Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
PY  - 2020///
SN  - 1868-8969
SP  - 9
TI  - Multiparty session programming with global protocol combinators
UR  - http://dx.doi.org/10.4230/LIPIcs.ECOOP.2020.9
UR  - http://hdl.handle.net/10044/1/79725
ER  -
Download