LFCS Seminar: 27 June 2019 - Peter Thiemann

Title: Label-Dependent Session Types

Abstract:

Session types have emerged as a typing discipline for communication protocols.  Existing calculi with session types come equipped with many different primitives that combine communication with the introduction or elimination of the transmitted value. We present a foundational session type calculus with a lightweight operational semantics.  It fully decouples communication from the introduction and elimination of data and thus features a single communication reduction, which acts as a rendezvous between senders and receivers.  We achieve this decoupling by introducing label-dependent session types, a minimalist value-dependent session type system with subtyping. The system is sufficiently powerful to simulate existing functional session type systems. Compared to such systems, label-dependent session types place fewer restrictions on the code. The new calculus showcases a novel integration of dependent types and linear typing, which has uses beyond session type systems.