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 Sep (GMT+09:00) Osaka, Sapporo, Tokyo change
|10:35 - 11:00|
|11:00 - 11:25|