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{Toninho:2016:10.1016/j.jlamp.2016.11.005,
author = {Toninho, B and Yoshida, N},
doi = {10.1016/j.jlamp.2016.11.005},
journal = {Journal of Logical and Algebraic Methods in Programming},
pages = {61--83},
title = {Certifying data in multiparty session types},
url = {http://dx.doi.org/10.1016/j.jlamp.2016.11.005},
volume = {90},
year = {2016}
}
Download

RIS format (EndNote, RefMan)

TY  - JOUR
AB  - Multiparty session types (MPST) are a typing discipline for ensuring the coordination of multi-agent communication in concurrent and distributed programs. The original MPST framework mainly focuses on the communication aspects of concurrency, unable to capture important data invariants in communicating programs. This work introduces value dependent types to the MPST framework in order to increase its expressiveness for certifying invariants of data exchanged among multiple participants. The key idea is to impose constraints on the exchanged data, which is explicitly witnessed at runtime by proof objects. The enriched MPST framework provides programmers with a precise global description of the interaction and data dependent patterns, from which local (data dependent) descriptions can be automatically generated for each endpoint, faithfully capturing at a local level the global data constraints. The framework ensures the absence of communication errors and guarantees communication progress in well-typed multiparty sessions. We also develop an extension of value dependencies based on proof irrelevance that enables the selective erasure of proof objects at runtime.
AU  - Toninho,B
AU  - Yoshida,N
DO  - 10.1016/j.jlamp.2016.11.005
EP  - 83
PY  - 2016///
SN  - 2352-2208
SP  - 61
TI  - Certifying data in multiparty session types
T2  - Journal of Logical and Algebraic Methods in Programming
UR  - http://dx.doi.org/10.1016/j.jlamp.2016.11.005
UR  - http://hdl.handle.net/10044/1/43200
VL  - 90
ER  -
Download