Sessions as Propositions
Sam Lindley (The University of Edinburgh), J. Garrett Morris (The, University of Edinburgh)
TL;DR
This paper introduces HGV, an extended session-typed language, and demonstrates its expressiveness matches that of the process calculus CP, clarifying the translation and limitations of GV.
Contribution
The paper extends GV to HGV and provides translations proving HGV's expressiveness equals CP, enhancing understanding of session types and process calculus translation.
Findings
HGV is as expressive as CP
New translations clarify GV to CP translation
Highlights limitations in GV's expressiveness
Abstract
Recently, Wadler presented a continuation-passing translation from a session-typed functional language, GV, to a process calculus based on classical linear logic, CP. However, this translation is one-way: CP is more expressive than GV. We propose an extension of GV, called HGV, and give translations showing that it is as expressive as CP. The new translations shed light both on the original translation from GV to CP, and on the limitations in expressiveness of GV.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.