{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T02:13:45Z","timestamp":1775873625483,"version":"3.50.1"},"reference-count":43,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2019,1,2]],"date-time":"2019-01-02T00:00:00Z","timestamp":1546387200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["EP\/L01503X\/1, EP\/K034413\/1"],"award-info":[{"award-number":["EP\/L01503X\/1, EP\/K034413\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2019,1,2]]},"abstract":"<jats:p>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.<\/jats:p>\n          <jats:p>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.<\/jats:p>\n          <jats:p>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.<\/jats:p>","DOI":"10.1145\/3290341","type":"journal-article","created":{"date-parts":[[2019,1,4]],"date-time":"2019-01-04T13:33:51Z","timestamp":1546608831000},"page":"1-29","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":40,"title":["Exceptional asynchronous session types: session types without tiers"],"prefix":"10.1145","volume":"3","author":[{"given":"Simon","family":"Fowler","sequence":"first","affiliation":[{"name":"University of Edinburgh, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sam","family":"Lindley","sequence":"additional","affiliation":[{"name":"University of Edinburgh, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"J. Garrett","family":"Morris","sequence":"additional","affiliation":[{"name":"University of Kansas, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"S\u00e1ra","family":"Decova","sequence":"additional","affiliation":[{"name":"University of Edinburgh, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2019,1,2]]},"reference":[{"key":"e_1_2_2_1_1","volume-title":"FORTE (Lecture Notes in Computer Science)","author":"Adameit Manuel","unstructured":"Manuel Adameit , Kirstin Peters , and Uwe Nestmann . 2017. Session types for link failures . In FORTE (Lecture Notes in Computer Science) , Vol. 10321 . Springer , 1\u201316. Manuel Adameit, Kirstin Peters, and Uwe Nestmann. 2017. Session types for link failures. In FORTE (Lecture Notes in Computer Science), Vol. 10321. Springer, 1\u201316."},{"key":"e_1_2_2_2_1","volume-title":"The Lambda Calculus Its Syntax and Semantics (revised ed.)","author":"Barendregt H. P.","unstructured":"H. P. Barendregt . 1984. The Lambda Calculus Its Syntax and Semantics (revised ed.) . Vol. 103 . North Holland . H. P. Barendregt. 1984. The Lambda Calculus Its Syntax and Semantics (revised ed.). Vol. 103. North Holland."},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796801004099"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_9"},{"key":"e_1_2_2_5_1","volume-title":"CONCUR (Lecture Notes in Computer Science)","author":"Caires Lu\u00eds","unstructured":"Lu\u00eds Caires and Frank Pfenning . 2010. Session types as intuitionistic linear propositions . In CONCUR (Lecture Notes in Computer Science) , Vol. 10 . Springer , 222\u2013236. Lu\u00eds Caires and Frank Pfenning. 2010. Session types as intuitionistic linear propositions. In CONCUR (Lecture Notes in Computer Science), Vol. 10. Springer, 222\u2013236."},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-43376-8_4"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-85361-9_32"},{"key":"e_1_2_2_8_1","volume-title":"CONCUR (LIPIcs)","volume":"59","author":"Carbone Marco","year":"2016","unstructured":"Marco Carbone , Sam Lindley , Fabrizio Montesi , Carsten Sch\u00fcrmann , and Philip Wadler . 2016 . Coherence generalises duality: A logical explanation of multiparty session types . In CONCUR (LIPIcs) , Vol. 59 . Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 33:1\u201333:15. Marco Carbone, Sam Lindley, Fabrizio Montesi, Carsten Sch\u00fcrmann, and Philip Wadler. 2016. Coherence generalises duality: A logical explanation of multiparty session types. In CONCUR (LIPIcs), Vol. 59. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 33:1\u201333:15."},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-39570-8_7"},{"key":"e_1_2_2_12_1","volume-title":"Links: Web programming without tiers. In FMCO (Lecture Notes in Computer Science)","author":"Cooper Ezra","year":"2007","unstructured":"Ezra Cooper , Sam Lindley , Philip Wadler , and Jeremy Yallop . 2007 . Links: Web programming without tiers. In FMCO (Lecture Notes in Computer Science) . Springer , 266\u2013296. Ezra Cooper, Sam Lindley, Philip Wadler, and Jeremy Yallop. 2007. Links: Web programming without tiers. In FMCO (Lecture Notes in Computer Science). Springer, 266\u2013296."},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2017.06.002"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-32940-1_20"},{"key":"e_1_2_2_15_1","unstructured":"Ian Fette and Alexey Melnikov. 2011. The WebSocket Protocol. RFC 6455. RFC Editor. 70 pages. http:\/\/www.rfc- editor.org\/ rfc\/rfc6455.txt  Ian Fette and Alexey Melnikov. 2011. The WebSocket Protocol. RFC 6455. RFC Editor. 70 pages. http:\/\/www.rfc- editor.org\/ rfc\/rfc6455.txt"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.223.3"},{"key":"e_1_2_2_17_1","doi-asserted-by":"crossref","unstructured":"Simon Fowler Sam Lindley J. Garrett Morris and S\u00e1ra Decova. 2018. Exceptional Asynchronous Session Types: Session Types without Tiers (extended version). http:\/\/www.simonjf.com\/writing\/zap- extended.pdf . (2018).  Simon Fowler Sam Lindley J. Garrett Morris and S\u00e1ra Decova. 2018. Exceptional Asynchronous Session Types: Session Types without Tiers (extended version). http:\/\/www.simonjf.com\/writing\/zap- extended.pdf . (2018).","DOI":"10.1145\/3291617"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796809990268"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2976022.2976033"},{"key":"e_1_2_2_20_1","volume-title":"FSCD (LIPIcs)","volume":"84","author":"Hillerstr\u00f6m Daniel","unstructured":"Daniel Hillerstr\u00f6m , Sam Lindley , Robert Atkey , and K. C. Sivaramakrishnan . 2017. Continuation passing style for effect handlers . In FSCD (LIPIcs) , Vol. 84 . Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 18:1\u201318:19. Daniel Hillerstr\u00f6m, Sam Lindley, Robert Atkey, and K. C. Sivaramakrishnan. 2017. Continuation passing style for effect handlers. In FSCD (LIPIcs), Vol. 84. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 18:1\u201318:19."},{"key":"e_1_2_2_21_1","volume-title":"CONCUR (Lecture Notes in Computer Science)","author":"Honda Kohei","unstructured":"Kohei Honda . 1993. Types for dyadic interaction . In CONCUR (Lecture Notes in Computer Science) . Springer , 509\u2013523. Kohei Honda. 1993. Types for dyadic interaction. In CONCUR (Lecture Notes in Computer Science). Springer, 509\u2013523."},{"key":"e_1_2_2_22_1","volume-title":"ESOP (Lecture Notes in Computer Science)","author":"Honda Kohei","unstructured":"Kohei Honda , Vasco T Vasconcelos , and Makoto Kubo . 1998. Language primitives and type discipline for structured communication-based programming . In ESOP (Lecture Notes in Computer Science) . Springer , 122\u2013138. Kohei Honda, Vasco T Vasconcelos, and Makoto Kubo. 1998. Language primitives and type discipline for structured communication-based programming. In ESOP (Lecture Notes in Computer Science). Springer, 122\u2013138."},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/2827695"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70592-5_22"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/2808098.2808100"},{"key":"e_1_2_2_26_1","volume-title":"10th Anniversary Colloquium of UNU\/IIST (Lecture Notes in Computer Science)","volume":"2757","author":"Kobayashi Naoki","year":"2002","unstructured":"Naoki Kobayashi . 2002 . Type systems for concurrent programs . In 10th Anniversary Colloquium of UNU\/IIST (Lecture Notes in Computer Science) , Vol. 2757 . Springer, 439\u2013453. Naoki Kobayashi. 2002. Type systems for concurrent programs. In 10th Anniversary Colloquium of UNU\/IIST (Lecture Notes in Computer Science), Vol. 2757. Springer, 439\u2013453."},{"key":"e_1_2_2_27_1","unstructured":"Wen Kokke. 2018. rusty-variation : a library for deadlock-free session-typed communication in Rust. https:\/\/github.com\/ wenkokke\/rusty- variation . (2018).  Wen Kokke. 2018. rusty-variation : a library for deadlock-free session-typed communication in Rust. https:\/\/github.com\/ wenkokke\/rusty- variation . (2018)."},{"key":"e_1_2_2_28_1","volume-title":"ESOP (Lecture Notes in Computer Science)","author":"Lindley Sam","unstructured":"Sam Lindley and J. Garrett Morris . 2015. A semantics for propositions as sessions . In ESOP (Lecture Notes in Computer Science) , Vol. 9032 . Springer , 560\u2013584. Sam Lindley and J. Garrett Morris. 2015. A semantics for propositions as sessions. In ESOP (Lecture Notes in Computer Science), Vol. 9032. Springer, 560\u2013584."},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951921"},{"key":"e_1_2_2_30_1","volume-title":"Behavioural Types: from Theory to Tools","author":"Lindley Sam","unstructured":"Sam Lindley and J Garrett Morris . 2017. Lightweight functional session types . In Behavioural Types: from Theory to Tools . River Publishers , 265\u2013286. Sam Lindley and J Garrett Morris. 2017. Lightweight functional session types. In Behavioural Types: from Theory to Tools. River Publishers, 265\u2013286."},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/2663171.2663188"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/1708016.1708027"},{"key":"e_1_2_2_33_1","volume-title":"Communicating and mobile systems: the pi calculus","author":"Milner Robin","unstructured":"Robin Milner . 1999. Communicating and mobile systems: the pi calculus . Cambridge university press . Robin Milner. 1999. Communicating and mobile systems: the pi calculus. Cambridge university press."},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-43376-8_8"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-43376-8_9"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3033019.3033031"},{"key":"e_1_2_2_37_1","volume-title":"Multiparty session actors. Logical Methods in Computer Science 13, 1","author":"Neykova Rumyana","year":"2017","unstructured":"Rumyana Neykova and Nobuko Yoshida . 2017b. Multiparty session actors. Logical Methods in Computer Science 13, 1 ( 2017 ). Rumyana Neykova and Nobuko Yoshida. 2017b. Multiparty session actors. Logical Methods in Computer Science 13, 1 (2017)."},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796816000289"},{"key":"e_1_2_2_39_1","volume-title":"ESOP (Lecture Notes in Computer Science)","author":"P\u00e9rez Jorge A","unstructured":"Jorge A P\u00e9rez , Lu\u00eds Caires , Frank Pfenning , and Bernardo Toninho . 2012. Linear logical relations for session-based concurrency . In ESOP (Lecture Notes in Computer Science) . Springer , 539\u2013558. Jorge A P\u00e9rez, Lu\u00eds Caires, Frank Pfenning, and Bernardo Toninho. 2012. Linear logical relations for session-based concurrency. In ESOP (Lecture Notes in Computer Science). Springer, 539\u2013558."},{"key":"e_1_2_2_40_1","volume-title":"Plotkin and Matija Pretnar","author":"Gordon","year":"2013","unstructured":"Gordon D. Plotkin and Matija Pretnar . 2013 . Handling algebraic effects. Logical Methods in Computer Science 9, 4 (2013). Gordon D. Plotkin and Matija Pretnar. 2013. Handling algebraic effects. Logical Methods in Computer Science 9, 4 (2013)."},{"key":"e_1_2_2_41_1","volume-title":"Theoretical Aspects Of Object-Oriented Programming, Carl A","author":"R\u00e9my Didier","unstructured":"Didier R\u00e9my . 1994. Type inference for records in a natural extension of ML . In Theoretical Aspects Of Object-Oriented Programming, Carl A . Gunter and John C. Mitchell (Eds.). MIT Press , Cambridge, MA , 67\u201395. Didier R\u00e9my. 1994. Type inference for records in a natural extension of ML. In Theoretical Aspects Of Object-Oriented Programming, Carl A. Gunter and John C. Mitchell (Eds.). MIT Press, Cambridge, MA, 67\u201395."},{"key":"e_1_2_2_42_1","volume-title":"ECOOP (LIPIcs)","volume":"74","author":"Scalas Alceste","year":"2017","unstructured":"Alceste Scalas , Ornela Dardha , Raymond Hu , and Nobuko Yoshida . 2017 . A linear decomposition of multiparty sessions for safe distributed programming . In ECOOP (LIPIcs) , Vol. 74 . Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 24:1\u201324:31. Alceste Scalas, Ornela Dardha, Raymond Hu, and Nobuko Yoshida. 2017. A linear decomposition of multiparty sessions for safe distributed programming. In ECOOP (LIPIcs), Vol. 74. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 24:1\u201324:31."},{"key":"e_1_2_2_43_1","volume-title":"ECOOP (LIPIcs)","volume":"56","author":"Scalas Alceste","year":"2016","unstructured":"Alceste Scalas and Nobuko Yoshida . 2016 . Lightweight session programming in scala . In ECOOP (LIPIcs) , Vol. 56 . Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 21:1\u201321:28. Alceste Scalas and Nobuko Yoshida. 2016. Lightweight session programming in scala. In ECOOP (LIPIcs), Vol. 56. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 21:1\u201321:28."},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/1411304.1411307"},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1017\/S095679681400001X"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3290341","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3290341","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T00:58:04Z","timestamp":1750208284000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3290341"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,1,2]]},"references-count":43,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2019,1,2]]}},"alternative-id":["10.1145\/3290341"],"URL":"https:\/\/doi.org\/10.1145\/3290341","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,1,2]]},"assertion":[{"value":"2019-01-02","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}