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{Carbone:2016:10.1007/s00236-016-0285-y,
author = {Carbone, M and Montesi, F and Schürmann, C and Yoshida, N},
doi = {10.1007/s00236-016-0285-y},
journal = {Acta Informatica},
pages = {243--269},
title = {Multiparty session types as coherence proofs},
url = {http://dx.doi.org/10.1007/s00236-016-0285-y},
volume = {54},
year = {2016}
}
Download

RIS format (EndNote, RefMan)

TY  - JOUR
AB  - We propose a Curry–Howard correspondence between a language for programming multiparty sessions and a generalisation of Classical Linear Logic (CLL). In this framework, propositions correspond to the local behaviour of a participant in a multiparty session type, proofs to processes, and proof normalisation to executing communications. Our key contribution is generalising duality, from CLL, to a new notion of n-ary compatibility, called coherence. Building on coherence as a principle of compositionality, we generalise the cut rule of CLL to a new rule for composing many processes communicating in a multiparty session. We prove the soundness of our model by showing the admissibility of our new rule, which entails deadlock-freedom via our correspondence.
AU  - Carbone,M
AU  - Montesi,F
AU  - Schürmann,C
AU  - Yoshida,N
DO  - 10.1007/s00236-016-0285-y
EP  - 269
PY  - 2016///
SN  - 0001-5903
SP  - 243
TI  - Multiparty session types as coherence proofs
T2  - Acta Informatica
UR  - http://dx.doi.org/10.1007/s00236-016-0285-y
UR  - http://hdl.handle.net/10044/1/43355
VL  - 54
ER  -
Download