Title: On Polymorphic Sessions and Functions: A Tale of Two (Fully Abstract) Encodings,
Abstract: This work exploits the logical foundation of session types to determine what
kind of type discipline for the pi-calculus can exactly capture, and is
captured by, lambda-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 pi-calculus and a linear formulation of System F. We are
then able to derive results of the session calculus from the theory of the
lambda-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.