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{Parente:2018:10.1007/978-3-319-89884-1_29,
author = {Parente, Coutinho Fernandes Toninho B and Yoshida, N},
doi = {10.1007/978-3-319-89884-1_29},
pages = {827--855},
publisher = {Springer},
title = {On polymorphic sessions and functions: A talk of two (fully abstract) encodings},
url = {http://dx.doi.org/10.1007/978-3-319-89884-1_29},
year = {2018}
}
Download

RIS format (EndNote, RefMan)

TY  - CPAPER
AB  - This work exploits the logical foundation of session types to determine what kind of type discipline for the   π -calculus can exactly capture, and is captured by,   λ -calculus behaviours. Leveraging the proof theoretic content of the soundness and completeness of sequent calculus and natural deduction presentations of linear logic, we develop the first mutually inverse and fully abstract processes-as-functions and functions-as-processes encodings between a polymorphic session   π -calculus and a linear formulation of System F. We are then able to derive results of the session calculus from the theory of the   λ -calculus: (1) we obtain a characterisation of inductive and coinductive session types via their algebraic representations in System F; and (2) we extend our results to account for value and process passing, entailing strong normalisation.
AU  - Parente,Coutinho Fernandes Toninho B
AU  - Yoshida,N
DO  - 10.1007/978-3-319-89884-1_29
EP  - 855
PB  - Springer
PY  - 2018///
SP  - 827
TI  - On polymorphic sessions and functions: A talk of two (fully abstract) encodings
UR  - http://dx.doi.org/10.1007/978-3-319-89884-1_29
UR  - http://hdl.handle.net/10044/1/55659
ER  -
Download