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 JanDisplayed time zone: Eastern Time (US & Canada) change
| 10:20 - 12:00 | |||
| 10:2025m Research paper | Pirouette: Higher-Order Typed Functional ChoreographiesDistinguished PaperInPerson POPLDOI Media Attached | ||
| 10:4525m Research paper | Fair Termination of Binary SessionsRemote POPLDOI Media Attached | ||
| 11:1025m Research paper | Safe, Modular Packet Pipeline ProgrammingRemote POPLDOI Media Attached | ||
| 11:3525m 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 DarmstadtDOI Media Attached | ||

