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

@article{Scalas:2018:10.1016/j.jlamp.2018.01.001,
author = {Scalas, A and Yoshida, N},
doi = {10.1016/j.jlamp.2018.01.001},
journal = {Journal of Logical and Algebraic Methods in Programming},
pages = {55--84},
title = {Multiparty session types, beyond duality},
url = {http://dx.doi.org/10.1016/j.jlamp.2018.01.001},
volume = {97},
year = {2018}
}
Download

RIS format (EndNote, RefMan)

TY  - JOUR
AB  - Multiparty Session Types (MPST) are a well-established typing discipline for message-passing processes interacting on sessions involving two or more participants. Session typing can ensure desirable properties: absence of communication errors and deadlocks, and protocol conformance.We propose a novel MPST theory based on a rely/guarantee typing system, that checks (1) the guaranteed behaviour of the process being typed, and (2) the relied upon behaviour of other processes. Crucially, our theory achieves type safety by enforcing a typing context liveness invariant throughout typing derivations.Unlike “classic” MPST works, our typing system does not depend on global session types, and does not use syntactic duality checks. As a result, our new theory can prove type safety for processes that implement protocols with complex inter-role dependencies, thus sidestepping an intrinsic limitation of “classic” MPST.
AU  - Scalas,A
AU  - Yoshida,N
DO  - 10.1016/j.jlamp.2018.01.001
EP  - 84
PY  - 2018///
SN  - 2352-2208
SP  - 55
TI  - Multiparty session types, beyond duality
T2  - Journal of Logical and Algebraic Methods in Programming
UR  - http://dx.doi.org/10.1016/j.jlamp.2018.01.001
UR  - http://hdl.handle.net/10044/1/56777
VL  - 97
ER  -
Download