Publications

BibTex format

@article{Toninho:2021:10.1145/3457884,
author = {Toninho, B and Yoshida, N},
doi = {10.1145/3457884},
journal = {ACM Transactions on Programming Languages and Systems},
pages = {1--55},
title = {On polymorphic sessions and functions: A tale of two (fully abstract) encodings},
url = {http://dx.doi.org/10.1145/3457884},
volume = {43},
year = {2021}
}

Download

RIS format (EndNote, RefMan)

TY  - JOUR
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 theoreticcontent of the soundness and completeness of sequent calculus and natural deduction presentations of linearlogic, we develop the first mutually inverse and fully abstract processes-as-functions and functions-as-processesencodings between a polymorphic session -calculus and a linear formulation of System F. We are then ableto derive results of the session calculus from the theory of the -calculus: (1) we obtain a characterisation ofinductive and coinductive session types via their algebraic representations in System F; and (2) we extend ourresults to account for value and process passing, entailing strong normalisation.
AU  - Toninho,B
AU  - Yoshida,N
DO  - 10.1145/3457884
EP  - 55
PY  - 2021///
SN  - 0164-0925
SP  - 1
TI  - On polymorphic sessions and functions: A tale of two (fully abstract) encodings
T2  - ACM Transactions on Programming Languages and Systems
UR  - http://dx.doi.org/10.1145/3457884
UR  - https://dl.acm.org/doi/10.1145/3457884
UR  - http://hdl.handle.net/10044/1/87071
VL  - 43
ER  -

Download

ProfessorNobukoYoshida

Contact

Location

Summary

Citation

BibTex format

RIS format (EndNote, RefMan)