Embedding session types in Haskell

Sam Lindley; J. Garrett Morris

doi:10.1145/2976002.2976018

Back

Conference proceeding

Open access

Embedding session types in Haskell

Sam Lindley and J. Garrett Morris

Haskell 2016 - Proceedings of the 9th International Symposium on Haskell, co-located with ICFP 2016, pp.133-145

09/08/2016

DOI: 10.1145/2976002.2976018

Files and links (1)

url

https://www.pure.ed.ac.uk/ws/files/27373454/gvhs.pdfView

Open Access

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.

Details

Title: Subtitle: Embedding session types in Haskell
Creators: Sam Lindley - University of Edinburgh
J. Garrett Morris - University of Edinburgh
Resource Type: Conference proceeding
Publication Details: Haskell 2016 - Proceedings of the 9th International Symposium on Haskell, co-located with ICFP 2016, pp.133-145
DOI: 10.1145/2976002.2976018
Grant note: DOI: 10.13039/501100000266, name: Engineering and Physical Sciences Research Council, award: EP/K034413/1
Language: English
Date published: 09/08/2016
Academic Unit: Computer Science
Record Identifier: 9984259480302771

Metrics

143 Record Views

39 Times Cited - Web of Science