Personal tools
You are here: Home Events LFCS Seminars-Folder LFCS Seminars LFCS seminar: Peter Thiemann: Label-Dependent Session Types

LFCS seminar: Peter Thiemann: Label-Dependent Session Types

— filed under: ,

  • LFCS Seminar
  • Upcoming events
When Jun 27, 2019
from 02:30 PM to 04:00 PM
Where IF 4.31/4.33
Add event to calendar vCal

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. 

Document Actions