On polymorphic sessions and functions: A tale of two (fully abstract) encodings
File(s)
Accepted version
Author(s)
Toninho, Bernardo
Yoshida, Nobuko
Type
Journal Article
Abstract
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.
𝜋-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.
Date Issued
2021-07
Date Acceptance
2021-03-17
Citation
ACM Transactions on Programming Languages and Systems, 2021, 43 (2), pp.1-55
ISSN
0164-0925
Publisher
Association for Computing Machinery (ACM)
Start Page
1
End Page
55
Journal / Book Title
ACM Transactions on Programming Languages and Systems
Volume
43
Issue
2
Copyright Statement
© 2021 Association for Computing Machinery.
Sponsor
Engineering & Physical Science Research Council (E
Engineering & Physical Science Research Council (E
Engineering & Physical Science Research Council (EPSRC)
Engineering & Physical Science Research Council (E
Engineering and Physical Sciences Research Council
Engineering & Physical Science Research Council (EPSRC)
Engineering & Physical Science Research Council (EPSRC)
Engineering & Physical Science Research Council (EPSRC)
Engineering and Physical Sciences Research Council
Engineering & Physical Science Research Council (E
The National Cyber Security Centre (NCSC)
Identifier
https://dl.acm.org/doi/10.1145/3457884
Grant Number
20208624
ERI 025567 (EP/K034413/1)
EP/K011715/1
PO 20131167
EP/L00058X/1, PO 20131167
EP/N027833/1
EP/T006544/1
EP/T014709/1
EP/V000462/1
EP/V000462/1
4214176 / RFA 20601
Subjects
Science & Technology
Technology
Computer Science, Software Engineering
Computer Science
Session types
pi-calculus
system F
linear logic
full abstraction
LINEAR LOGICAL RELATIONS
EXPRESSIVENESS
PARAMETRICITY
PROPOSITIONS
POLARITIES
CALCULUS
LIBRARY
OCAML
Software Engineering
0803 Computer Software
0806 Information Systems
Publication Status
Published
Date Publish Online
2021-07