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 Times are displayed in time zone: (GMT+09:00) Osaka, Sapporo, Tokyo change
|10:35 - 11:00|
|11:00 - 11:25|