On Polymorphic Sessions and Functions: A Tale of Two (Fully Abstract) Encodings

Bernardo Toninho, Nobuko Yoshida

Research output: Contribution to journalArticlepeer-review

1 Citation (Scopus)

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 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.

Original languageEnglish
Article number3457884
JournalACM Transactions on Programming Languages and Systems
Volume43
Issue number2
DOIs
Publication statusPublished - 8 Jun 2021

Keywords

  • full abstraction
  • I€-calculus
  • linear logic
  • Session types
  • system F

Cite this