Multiparty GV: Functional Multiparty Session Types With Certified Deadlock Freedom
Session types have recently been integrated with functional languages, bringing message-passing concurrency to functional programming. Channel endpoints then become first-class and can be stored in data structures, captured in closures, and sent along channels. Representatives of the GV family are of particular appeal because they not only assert session fidelity but also deadlock freedom, inspired by a Curry-Howard correspondence to linear logic. A restriction of GV, however, is its focus on binary sessions, limiting concurrent interactions to two participants. This paper introduces Multiparty GV (MPGV), a functional language with multiparty session types, allowing concurrent interactions among several participants. MPGV upholds the strong guarantees of its ancestor GV, including deadlock freedom, despite session interleaving and delegation. Scaling deadlock freedom to the multiparty setting is challenging due to circular and dynamically changing communication topologies—the paper presents the first proof thereof in a proof assistant. MPGV has a novel relabeling construct for modular programming with first-class endpoints. A type-preserving translation from binary session types to MPGV is given using relabeling to show that MPGV is strictly more general than GV.
Tue 13 SepDisplayed time zone: Belgrade, Bratislava, Budapest, Ljubljana, Prague change
10:30 - 12:10 | |||
10:30 20mTalk | Later Credits: Resourceful Reasoning for the Later Modality ICFP Papers and Events Simon Spies MPI-SWS & Saarland University, Lennard Gäher MPI-SWS & Saarland University, Joseph Tassarotti NYU, Ralf Jung MPI-SWS, Robbert Krebbers Radboud University Nijmegen, Lars Birkedal Aarhus University, Derek Dreyer MPI-SWS DOI | ||
10:50 20mTalk | Introduction and Elimination, Left and Right ICFP Papers and Events Klaus Ostermann University of Tübingen, David Binder University of Tübingen, Ingo Skupin University of Tübingen, Tim Süberkrüb University of Tübingen, Paul Downen University of Massachusetts Lowell DOI Pre-print | ||
11:10 20mTalk | Normalization for Fitch-style Modal CalculiDistinguished Paper ICFP Papers and Events Nachiappan Valliappan Chalmers University of Technology, Fabian Ruch Unaffiliated, Carlos Tomé Cortiñas Chalmers University of Technology DOI Media Attached | ||
11:30 20mTalk | Multiparty GV: Functional Multiparty Session Types With Certified Deadlock Freedom ICFP Papers and Events Jules Jacobs Radboud University, Stephanie Balzer Carnegie Mellon University, Robbert Krebbers Radboud University Nijmegen DOI | ||
11:50 20mTalk | Back to futuresJFP Presentation ICFP Papers and Events |