We present a novel embedding of session-typed concurrency in Haskell. We extend an existing HOAS embedding of linear $\lambda$-calculus with a set of core session-typed primitives, using indexed type families to express the constraints of the session typing discipline. We give two interpretations of our embedding, one in terms of GHC's built-in concurrency and another in terms of purely functional continuations. Our safety guarantees, including deadlock freedom, are assured statically and introduce no additional runtime overhead.
Fri 23 SepDisplayed time zone: Osaka, Sapporo, Tokyo change
10:35 - 11:25
|Experience Report: Types for a Relational Algebra Library
|Embedding Session Types in Haskell