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

@inproceedings{Yoshida:2018:10.1007/978-3-319-89366-2_7,
author = {Yoshida, N and Parente, Coutinho Fernandes Toninho B},
doi = {10.1007/978-3-319-89366-2_7},
pages = {128--145},
publisher = {Springer},
title = {Depending on session typed process},
url = {http://dx.doi.org/10.1007/978-3-319-89366-2_7},
year = {2018}
}
Download

RIS format (EndNote, RefMan)

TY  - CPAPER
AB  - This work proposes a dependent type theory that combines functions and session-typed processes (with value dependencies) through a contextual monad, internalising typed processes in a dependently-typed   λ -calculus. The proposed framework, by allowing session processes to depend on functions and vice-versa, enables us to specify and statically verify protocols where the choice of the next communication action can depend on specific values of received data. Moreover, the type theoretic nature of the framework endows us with the ability to internally describe and prove predicates on process behaviours. Our main results are type soundness of the framework, and a faithful embedding of the functional layer of the calculus within the session-typed layer, showcasing the expressiveness of dependent session types.
AU  - Yoshida,N
AU  - Parente,Coutinho Fernandes Toninho B
DO  - 10.1007/978-3-319-89366-2_7
EP  - 145
PB  - Springer
PY  - 2018///
SP  - 128
TI  - Depending on session typed process
UR  - http://dx.doi.org/10.1007/978-3-319-89366-2_7
UR  - http://hdl.handle.net/10044/1/55658
ER  -
Download