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

@unpublished{Zhou:2020,
author = {Zhou, F and Ferreira, F and Hu, R and Neykova, R and Yoshida, N},
publisher = {arXiv},
title = {Statically verified refinements for multiparty protocols},
url = {http://arxiv.org/abs/2009.06541v1},
year = {2020}
}
Download

RIS format (EndNote, RefMan)

TY  - UNPB
AB  - With distributed computing becoming ubiquitous in the modern era, safedistributed programming is an open challenge. To address this, multipartysession types (MPST) provide a typing discipline for message-passingconcurrency, guaranteeing communication safety properties such as deadlockfreedom.  While originally MPST focus on the communication aspects, and employ a simpletyping system for communication payloads, communication protocols in the realworld usually contain constraints on the payload. We introduce refinedmultiparty session types (RMPST), an extension of MPST, that express datadependent protocols via refinement types on the data types.  We provide an implementation of RMPST, in a toolchain called Session, usingScribble, a multiparty protocol description toolchain, and targeting F, averification-oriented functional programming language. Users can describe aprotocol in Scribble and implement the endpoints in F using refinement-typedAPIs generated from the protocol. The F compiler can then statically verifythe refinements. Moreover, we use a novel approach of callback-styled APIgeneration, providing static linearity guarantees with the inversion ofcontrol. We evaluate our approach with real world examples and show that it haslittle overhead compared to a na\"ive implementation, while guaranteeing safetyproperties from the underlying theory.
AU  - Zhou,F
AU  - Ferreira,F
AU  - Hu,R
AU  - Neykova,R
AU  - Yoshida,N
PB  - arXiv
PY  - 2020///
TI  - Statically verified refinements for multiparty protocols
UR  - http://arxiv.org/abs/2009.06541v1
UR  - http://hdl.handle.net/10044/1/82817
ER  -
Download