ATTENTION: The software behind KU ScholarWorks is being upgraded to a new version. Starting July 15th, users will not be able to log in to the system, add items, nor make any changes until the new version is in place at the end of July. Searching for articles and opening files will continue to work while the system is being updated.
If you have any questions, please contact Marianne Reed at mreed@ku.edu .
Exceptional asynchronous session types: Session types without tiers
dc.contributor.author | Fowler, Simon | |
dc.contributor.author | Lindley, Sam | |
dc.contributor.author | Morris, J. Garrett | |
dc.contributor.author | Decova, Sára | |
dc.date.accessioned | 2021-02-09T20:14:07Z | |
dc.date.available | 2021-02-09T20:14:07Z | |
dc.date.issued | 2019-01 | |
dc.identifier.citation | Simon Fowler, Sam Lindley, J. Garrett Morris, and Sára Decova. 2019. Exceptional asynchronous session types: session types without tiers. Proc. ACM Program. Lang. 3, POPL, Article 28 (January 2019), 29 pages. DOI:https://doi.org/10.1145/3290341 | en_US |
dc.identifier.uri | http://hdl.handle.net/1808/31399 | |
dc.description | This work is licensed under a Creative Commons Attribution 4.0 International License. | en_US |
dc.description.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. | en_US |
dc.publisher | Association for Computing Machinery (ACM) | en_US |
dc.rights | © 2019 Copyright held by the owner/author(s). | en_US |
dc.rights.uri | http://creativecommons.org/licenses/by/4.0/ | en_US |
dc.subject | Functional languages | en_US |
dc.subject | Concurrent programming languages | en_US |
dc.subject | Deadlocks | en_US |
dc.subject | Session types | en_US |
dc.subject | Asynchrony | en_US |
dc.subject | Exceptions | en_US |
dc.subject | Web programming | en_US |
dc.title | Exceptional asynchronous session types: Session types without tiers | en_US |
dc.type | Article | en_US |
kusw.kuauthor | Morris, J. Garrett | |
kusw.kudepartment | Electrical Engineering & Computer Science | en_US |
dc.identifier.doi | 10.1145/3290341 | en_US |
kusw.oaversion | Scholarly/refereed, publisher version | en_US |
kusw.oapolicy | This item meets KU Open Access policy criteria. | en_US |
dc.rights.accessrights | openAccess | en_US |