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{Chen:2017:10.23638/LMCS-13(2:12)2017,
author = {Chen, T-C and Dezani-Ciancaglini, M and Scalas, A and Yoshida, N},
doi = {10.23638/LMCS-13(2:12)2017},
journal = {Logical Methods in Computer Science},
title = {On the preciseness of subtyping in session types},
url = {http://dx.doi.org/10.23638/LMCS-13(2:12)2017},
volume = {13},
year = {2017}
}
Download

RIS format (EndNote, RefMan)

TY  - JOUR
AB  - Subtyping in concurrency has been extensively studied since early 1990s asone of the most interesting issues in type theory.  The correctness of subtyping relations hasbeen usually provided as the soundness for type safety.  The converse direction, the com-pleteness, has been largely ignored in spite of its usefulness to de ne the largest subtypingrelation ensuring type safety.  This paper formalises preciseness (i.e.  both soundness andcompleteness) of subtyping for mobile processes and studies it for the synchronous and theasynchronous session calculi.  We  rst prove that the well-known session subtyping,  thebranching-selection subtyping, is sound and complete for the synchronous calculus.  Nextwe show that in the asynchronous calculus, this subtyping is incomplete for type-safety:that is, there exist session typesTandSsuch thatTcan safely be considered as a subtypeofS, butT6Sis not derivable by the subtyping.  We then propose an asynchronous sub-typing system which is sound and complete for the asynchronous calculus.  The methodgives a general guidance to design rigorous channel-based subtypings respecting desiredsafety properties.  Both the synchronous and the asynchronous calculus are  rst consid-ered with linear channels only, and then they are extended with session initialisations andcommunications of expressions (including shared channels).
AU  - Chen,T-C
AU  - Dezani-Ciancaglini,M
AU  - Scalas,A
AU  - Yoshida,N
DO  - 10.23638/LMCS-13(2:12)2017
PY  - 2017///
SN  - 1860-5974
TI  - On the preciseness of subtyping in session types
T2  - Logical Methods in Computer Science
UR  - http://dx.doi.org/10.23638/LMCS-13(2:12)2017
UR  - http://hdl.handle.net/10044/1/43231
VL  - 13
ER  -
Download