Fri 21 Jan 2022 10:45 - 11:10 at Salon I - Distributed or Network Programs Chair(s): J. Garrett Morris

A binary session is a private communication channel that connects two processes, each adhering to a protocol description called session type. In this work, we study the first type system that ensures the fair termination of binary sessions. A session fairly terminates if all of the infinite executions admitted by its protocol are deemed “unrealistic” because they violate certain fairness assumptions. Fair termination entails the eventual completion of all pending input/output actions, including those that depend on the completion of an unbounded number of other actions in possibly different sessions. This form of lock freedom allows us to address a large family of natural communication patterns that falls outside the scope of existing type systems. Our type system is also the first to adopt fair subtyping, a termination-preserving refinement of the standard subtyping relation for session types that so far has only been studied theoretically. Fair subtyping is surprisingly subtle not only to characterize concisely but also to use appropriately, to the point that the type system must carefully account for all usages of fair subtyping to avoid compromising its termination-preserving properties.

Fri 21 Jan

Displayed time zone: Eastern Time (US & Canada) change

10:20 - 12:00
Distributed or Network ProgramsPOPL at Salon I
Chair(s): J. Garrett Morris The University of Iowa
10:20
25m
Research paper
Pirouette: Higher-Order Typed Functional ChoreographiesDistinguished PaperInPerson
POPL
Andrew K. Hirsch MPI-SWS, Deepak Garg MPI-SWS
DOI Media Attached
10:45
25m
Research paper
Fair Termination of Binary SessionsRemote
POPL
Luca Ciccone University of Turin, Luca Padovani University of Turin
DOI Media Attached
11:10
25m
Research paper
Safe, Modular Packet Pipeline ProgrammingRemote
POPL
Devon Loehr Princeton University, David Walker Princeton University
DOI Media Attached
11:35
25m
Research paper
Dependently-Typed Data Plane ProgrammingRemote
POPL
Matthias Eichholz TU Darmstadt, Eric Campbell Cornell University, Matthias Krebs TU Darmstadt, Nate Foster Cornell University, Mira Mezini TU Darmstadt
DOI Media Attached