Write a Blog >>

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 Jan
Times are displayed in 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 SarkarUniversity of St. Andrews
11:45 - 12:07
Label-Dependent Session Types
Research Papers
Peter ThiemannUniversity of Freiburg, Germany, Vasco T. VasconcelosUniversity of Lisbon, Portugal
Link to publication DOI Media Attached
12:07 - 12:30
Par means Parallel: Multiplicative Linear Logic Proofs as Concurrent Functional Programs
Research Papers
Federico AschieriTU Wien, Francesco A. GencoIHPST, Université Paris 1
Link to publication DOI Media Attached