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 language | English |
---|---|
Title of host publication | Haskell 2016: Proceedings of the 9th International Symposium on Haskell |
Editors | Geoffrey Mainland |
Publisher | Association for Computing Machinery |
Pages | 133-145 |
Number of pages | 13 |
ISBN (Print) | 9781450344340 |
DOIs | |
Publication status | Published - Sept 2016 |
Event | 9th International Symposium on Haskell 2016 - Nara, Japan Duration: 22 Sept 2016 → 23 Sept 2016 |
Conference
Conference | 9th International Symposium on Haskell 2016 |
---|---|
Country/Territory | Japan |
City | Nara |
Period | 22/09/16 → 23/09/16 |
Keywords
- Embedded languages
- Linear types
- Session types
ASJC Scopus subject areas
- Computer Graphics and Computer-Aided Design
- Computer Vision and Pattern Recognition
- Computer Science Applications
- Software
- Human-Computer Interaction