TY - JOUR
T1 - On Polymorphic Sessions and Functions
T2 - A Tale of Two (Fully Abstract) Encodings
AU - Toninho, Bernardo
AU - Yoshida, Nobuko
N1 - Funding Information:
info:eu-repo/grantAgreement/FCT/5876/147279/PT#
The work is supported by NOVA LINCS ( UIDB/04516/2020), EPSRC EP/N028201/1, EP/K034413/1, EP/K011715/1, EP/L00058X/1, EP/N027833/1, EP/T006544/1, EP/T014709/1 and EP/V000462/1, and EPSRC/NCSC/GCHQ VeTSS. Authors’ addresses: B. Toninho, Departamento de Informática, Faculdade de Ciências e Tecnologia, Universidade Nova de Lisboa, Quinta da Torre, 2829-516 CAPARICA, Portugal; email: [email protected]; N. Yoshida, Department of Computing, Imperial College London, 180 Queen’s Gate, South Kensington Campus, London SW7 2AZ; email: [email protected]. Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]. © 2021 Association for Computing Machinery. 0164-0925/2021/06-ART7 $15.00 https://doi.org/10.1145/3457884
Publisher Copyright:
© 2021 ACM.
PY - 2021/6/8
Y1 - 2021/6/8
N2 - 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 I€-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.
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 I€-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.
KW - full abstraction
KW - I€-calculus
KW - linear logic
KW - Session types
KW - system F
UR - http://www.scopus.com/inward/record.url?scp=85111456477&partnerID=8YFLogxK
U2 - 10.1145/3457884
DO - 10.1145/3457884
M3 - Article
AN - SCOPUS:85111456477
SN - 0164-0925
VL - 43
JO - ACM Transactions on Programming Languages and Systems
JF - ACM Transactions on Programming Languages and Systems
IS - 2
M1 - 3457884
ER -