Journal article
Exceptional asynchronous session types: session types without tiers
Proceedings of ACM on programming languages, Vol.3(POPL), pp.1-29
01/02/2019
DOI: 10.1145/3290341
Abstract
Session types statically guarantee that communication complies with a protocol. However, most accounts of session typing do not account for failure, which means they are of limited use in real applications---especially distributed applications---where failure is pervasive. We present the first formal integration of asynchronous session types with exception handling in a functional programming language. We define a core calculus which satisfies preservation and progress properties, is deadlock free, confluent, and terminating. We provide the first implementation of session types with exception handling for a fully-fledged functional programming language, by extending the Links web programming language; our implementation draws on existing work on effect handlers. We illustrate our approach through a running example of two-factor authentication, and a larger example of a session-based chat application where communication occurs over session-typed channels and disconnections are handled gracefully.
Details
- Title: Subtitle
- Exceptional asynchronous session types: session types without tiers
- Creators
- Simon Fowler - University of EdinburghSam Lindley - University of EdinburghJ. Garrett Morris - University of KansasSára Decova - University of Edinburgh
- Resource Type
- Journal article
- Publication Details
- Proceedings of ACM on programming languages, Vol.3(POPL), pp.1-29
- DOI
- 10.1145/3290341
- ISSN
- 2475-1421
- eISSN
- 2475-1421
- Grant note
- DOI: 10.13039/501100000266, name: Engineering and Physical Sciences Research Council, award: EP/L01503X/1, EP/K034413/1
- Language
- English
- Date published
- 01/02/2019
- Academic Unit
- Computer Science
- Record Identifier
- 9984259491902771
Metrics
15 Record Views