Embedding session types in Haskell

Sam Lindley, J. Garrett Morris

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

We present a novel embedding of session-typed concurrency in Haskell. We extend an existing HOAS embedding of linear λ-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.
Original languageEnglish
Title of host publicationHaskell 2016 Proceedings of the 9th International Symposium on Haskell
PublisherACM
Pages133-145
Number of pages13
ISBN (Electronic)978-1-4503-4434-0
DOIs
Publication statusPublished - 8 Sep 2016
Event2016 Proceedings of the 9th International Symposium on Haskell - Nara, Japan
Duration: 18 Sep 201624 Sep 2016
https://conf.researchr.org/home/icfp-2016/

Publication series

NameACM SIGPLAN Notices
PublisherACM
Number12
Volume51
ISSN (Print)0362-1340
ISSN (Electronic)1558-1160

Conference

Conference2016 Proceedings of the 9th International Symposium on Haskell
Abbreviated titleICFP'16
CountryJapan
CityNara
Period18/09/1624/09/16
Internet address

Cite this