Label-Dependent Session Types
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. We further introduce primitive recursion over natural numbers at the type level, thus allowing to describe protocols whose behaviour depends on numbers exchanged in messages. An algorithmic type checking system is introduced and proved equivalent to its declarative counterpart.
The new calculus showcases a novel lightweight integration of dependent types and linear typing, with has uses beyond session type systems.
Fri 24 JanDisplayed time zone: Saskatchewan, Central America change
11:45 - 12:30
Concurrent Programming & Session TypesResearch Papers at Ile de France II (IDF II)
Chair(s): Susmit Sarkar University of St. Andrews
|Label-Dependent Session Types|
Peter Thiemann University of Freiburg, Germany, Vasco T. Vasconcelos University of Lisbon, PortugalLink to publication DOI Media Attached
|Par means Parallel: Multiplicative Linear Logic Proofs as Concurrent Functional Programs|
Federico Aschieri TU Wien, Francesco A. Genco IHPST, Université Paris 1Link to publication DOI Media Attached