TL;DR
This paper introduces a simplified, label-dependent session type calculus with a single communication reduction, enabling more flexible protocol descriptions and integrating dependent types with linear typing.
Contribution
It presents a foundational session type calculus with label-dependent types, decoupling communication from data manipulation, and introduces type-level recursion for protocol behaviors.
Findings
Decouples communication from data manipulation in session types
Supports type-level recursion for protocol-dependent behaviors
Proves equivalence of algorithmic and declarative type checking
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. We further introduce primitive recursion over…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Code & Models
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
