{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:21:57Z","timestamp":1750220517599,"version":"3.41.0"},"reference-count":36,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2021,1,4]],"date-time":"2021-01-04T00:00:00Z","timestamp":1609718400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000181","name":"Air Force Office of Scientific Research","doi-asserted-by":"publisher","award":["FA9550-17-1-0326"],"award-info":[{"award-number":["FA9550-17-1-0326"]}],"id":[{"id":"10.13039\/100000181","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000780","name":"European Commission","doi-asserted-by":"publisher","award":["834146"],"award-info":[{"award-number":["834146"]}],"id":[{"id":"10.13039\/501100000780","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":[[2021,1,4]]},"abstract":"<jats:p>\n            We explore asynchronous programming with algebraic effects. We complement their conventional synchronous treatment by showing how to naturally also accommodate asynchrony within them, namely, by decoupling the execution of operation calls into signalling that an operation\u2019s implementation needs to be executed, and interrupting a running computation with the operation\u2019s result, to which the computation can react by installing interrupt handlers. We formalise these ideas in a small core calculus, called \u03bb\n            <jats:sub>\u00e6<\/jats:sub>\n            . We demonstrate the flexibility of \u03bb\n            <jats:sub>\u00e6<\/jats:sub>\n            \u00a0using examples ranging from a multi-party web application, to preemptive multi-threading, to remote function calls, to a parallel variant of runners of algebraic effects. In addition, the paper is accompanied by a formalisation of \u03bb\n            <jats:sub>\u00e6<\/jats:sub>\n            \u2019s type safety proofs in Agda, and a prototype implementation of \u03bb\n            <jats:sub>\u00e6<\/jats:sub>\n            \u00a0in OCaml.\n          <\/jats:p>","DOI":"10.1145\/3434305","type":"journal-article","created":{"date-parts":[[2021,1,4]],"date-time":"2021-01-04T17:34:24Z","timestamp":1609781664000},"page":"1-28","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":6,"title":["Asynchronous effects"],"prefix":"10.1145","volume":"5","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-6595-2756","authenticated-orcid":false,"given":"Danel","family":"Ahman","sequence":"first","affiliation":[{"name":"University of Ljubljana, Slovenia"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7755-2303","authenticated-orcid":false,"given":"Matija","family":"Pretnar","sequence":"additional","affiliation":[{"name":"University of Ljubljana, Slovenia"}]}],"member":"320","published-online":{"date-parts":[[2021,1,4]]},"reference":[{"key":"e_1_2_1_1_1","unstructured":"D. Ahman. 2020. Agda formalisation of the ae-calculus. Available at https:\/\/github.com\/danelahman\/aef-agda\/releases\/ tag\/popl-2021.  D. Ahman. 2020. Agda formalisation of the ae-calculus. Available at https:\/\/github.com\/danelahman\/aef-agda\/releases\/ tag\/popl-2021."},{"key":"e_1_2_1_2_1","first-page":"29","volume-title":"Proc. of 29th European Symp. on Programming, ESOP 2020 (LNCS","volume":"12075","author":"Ahman D."},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.4072753"},{"volume-title":"Domains and Lambda Calculi","author":"Amadio R. M.","key":"e_1_2_1_4_1","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511983504"},{"volume-title":"Proc. ACM Program. Lang. 3, ICFP ( 2019 ), 109 : 1-109 : 27","author":"Bahr P.","key":"e_1_2_1_5_1"},{"key":"e_1_2_1_6_1","doi-asserted-by":"crossref","unstructured":"A. Bauer and M. Pretnar. 2014. An Efect System for Algebraic Efects and Handlers. Logical Methods in Computer Science 10 4 ( 2014 ).  A. Bauer and M. Pretnar. 2014. An Efect System for Algebraic Efects and Handlers. Logical Methods in Computer Science 10 4 ( 2014 ).","DOI":"10.2168\/LMCS-10(4:9)2014"},{"key":"e_1_2_1_7_1","article-title":"Programming with algebraic efects and handlers","volume":"84","author":"Bauer A.","year":"2015","journal-title":"J. Log. Algebr. Meth. Program."},{"volume-title":"Proc. of 41st Ann. ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages, POPL 2014. ACM, 619-632","author":"Benton N.","key":"e_1_2_1_8_1"},{"volume-title":"Proc. ACM Program. Lang. 3, POPL ( 2019 ), 6 : 1-6 : 28","author":"Biernacki D.","key":"e_1_2_1_9_1"},{"key":"e_1_2_1_10_1","first-page":"1","article-title":"Pyro: Deep Universal Probabilistic Programming","volume":"20","author":"Bingham E.","year":"2019","journal-title":"J. Mach. Learn. Res."},{"key":"e_1_2_1_11_1","doi-asserted-by":"crossref","unstructured":"L. Convent S. Lindley C. McBride and C. McLaughlin. 2020. Doo bee doo bee doo. J. Funct. Program. 30 ( 2020 ) e9.  L. Convent S. Lindley C. McBride and C. McLaughlin. 2020. Doo bee doo bee doo. J. Funct. Program. 30 ( 2020 ) e9.","DOI":"10.1017\/S0956796820000039"},{"volume-title":"Proc. of 18th Int. Sym. Trends in Functional Programming, TFP 2017. Springer, 98-117","author":"Dolan S.","key":"e_1_2_1_12_1"},{"volume-title":"Proc. of 23rd ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages, POPL'96. ACM, 372-385","author":"Fournet C.","key":"e_1_2_1_13_1"},{"key":"e_1_2_1_14_1","doi-asserted-by":"crossref","unstructured":"G. Gierz K. H. Hofmann K. Keimel J. D. Lawson M. Mislove and D. S. Scott. 2003. Continuous Lattices and Domains. Number 93 in Encyclopedia of Mathematics and its Applications. Cambridge University Press.  G. Gierz K. H. Hofmann K. Keimel J. D. Lawson M. Mislove and D. S. Scott. 2003. Continuous Lattices and Domains. Number 93 in Encyclopedia of Mathematics and its Applications. Cambridge University Press.","DOI":"10.1017\/CBO9780511542725"},{"key":"e_1_2_1_15_1","unstructured":"P. Haller A. Prokopec H. Miller V. Klang R. Kuhn and V. Jovanovic. 2020. Scala documentation: Futures and Promises. ( July 2020 ). Available online at https:\/\/docs.scala-lang.org\/overviews\/core\/futures.html.  P. Haller A. Prokopec H. Miller V. Klang R. Kuhn and V. Jovanovic. 2020. Scala documentation: Futures and Promises. ( July 2020 ). Available online at https:\/\/docs.scala-lang.org\/overviews\/core\/futures.html."},{"first-page":"235","volume-title":"Proc. of 3rd Int. Joint Conf. on Artificial Intelligence, IJCAI' 73","author":"Hewitt C.","key":"e_1_2_1_16_1"},{"key":"e_1_2_1_17_1","first-page":"122","volume-title":"Proc. of 7th European Symp. on Programming, ESOP 1998 (LNCS","volume":"1381","author":"Honda K."},{"volume-title":"Proc. of 18th ACM SIGPLAN Int. Conf. on Functional Programming, ICFP 2013. ACM, 145-158","author":"Kammar O.","key":"e_1_2_1_18_1"},{"volume-title":"Proc. of 39th ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages, POPL 2012. ACM, 349-360","author":"Kammar O.","key":"e_1_2_1_19_1"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500588"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3122975.3122977"},{"key":"e_1_2_1_22_1","doi-asserted-by":"crossref","unstructured":"P. B. Levy J. Power and H. Thielecke. 2003. Modelling environments in call-by-value programming languages. Inf. Comput. 185 2 ( 2003 ) 182-210.  P. B. Levy J. Power and H. Thielecke. 2003. Modelling environments in call-by-value programming languages. Inf. Comput. 185 2 ( 2003 ) 182-210.","DOI":"10.1016\/S0890-5401(03)00088-9"},{"volume-title":"Proc. of 44th ACM SIGPLAN Symp. on Principles of Programming Languages, POPL 2017. ACM, 500-514","author":"Lindley S.","key":"e_1_2_1_23_1"},{"key":"e_1_2_1_24_1","doi-asserted-by":"crossref","unstructured":"R. Milner J. Parrow and D. Walker. 1992. A calculus of mobile processes I. Inf. Comput. 100 1 ( 1992 ) 1-40.  R. Milner J. Parrow and D. Walker. 1992. A calculus of mobile processes I. Inf. Comput. 100 1 ( 1992 ) 1-40.","DOI":"10.1016\/0890-5401(92)90008-4"},{"volume-title":"Proc. of 33rd Annual ACM\/IEEE Symp. on Logic in Computer Science, LICS 2018. ACM, 809-818","author":"Pir\u00f3g M.","key":"e_1_2_1_26_1"},{"volume-title":"Conf. on Concurrency Theory, CONCUR","year":"2012","author":"Plotkin G. D.","key":"e_1_2_1_27_1"},{"key":"e_1_2_1_28_1","first-page":"342","volume-title":"Proc. of 5th Int. Conf. on Foundations of Software Science and Computation Structures, FOSSACS 2002 (LNCS","volume":"2303","author":"Plotkin G. D."},{"volume-title":"Proc. of 23th Ann. IEEE Symp. on Logic in Computer Science, LICS 2008. IEEE, 118-129","author":"Plotkin G. D.","key":"e_1_2_1_29_1"},{"key":"e_1_2_1_30_1","doi-asserted-by":"crossref","unstructured":"G. D. Plotkin and M. Pretnar. 2013. Handling Algebraic Efects. Logical Methods in Computer Science 9 4 : 23 ( 2013 ).  G. D. Plotkin and M. Pretnar. 2013. Handling Algebraic Efects. Logical Methods in Computer Science 9 4 : 23 ( 2013 ).","DOI":"10.2168\/LMCS-9(4:23)2013"},{"volume-title":"Asynchronous Efect Handling. Master's thesis. School of Informatics","author":"Poulson L.","key":"e_1_2_1_31_1"},{"key":"e_1_2_1_32_1","doi-asserted-by":"crossref","unstructured":"M. Pretnar. 2015. An Introduction to Algebraic Efects and Handlers. Invited tutorial paper. Electr. Notes Theor. Comput. Sci. 319 ( 2015 ) 19-35.  M. Pretnar. 2015. An Introduction to Algebraic Efects and Handlers. Invited tutorial paper. Electr. Notes Theor. Comput. Sci. 319 ( 2015 ) 19-35.","DOI":"10.1016\/j.entcs.2015.12.003"},{"key":"e_1_2_1_33_1","unstructured":"M. Pretnar. 2020. Programming language \u00c6ff. Available at https:\/\/github.com\/matijapretnar\/aef\/releases\/tag\/popl-2021.  M. Pretnar. 2020. Programming language \u00c6ff. Available at https:\/\/github.com\/matijapretnar\/aef\/releases\/tag\/popl-2021."},{"key":"e_1_2_1_34_1","unstructured":"J. Schwinghammer. 2002. A Concurrent Lambda-Calculus with Promises and Futures. Master's thesis. Programming Systems Lab Universit\u00e4t des Saarlandes.  J. Schwinghammer. 2002. A Concurrent Lambda-Calculus with Promises and Futures. Master's thesis. Programming Systems Lab Universit\u00e4t des Saarlandes."},{"volume-title":"Proc. of 28th Ann. ACM\/IEEE Symp. on Logic in Computer Science, LICS 2013. IEEE, 519-519","year":"2013","author":"Staton S.","key":"e_1_2_1_35_1"},{"volume-title":"Proc. of 42nd Annual ACM SIGPLANSIGACT Symp. on Principles of Programming Languages, POPL 2015. ACM, 395-406","year":"2015","author":"Staton S.","key":"e_1_2_1_36_1"},{"key":"e_1_2_1_37_1","doi-asserted-by":"crossref","unstructured":"A. K. Wright and M. Felleisen. 1994. A Syntactic Approach to Type Soundness. Information and Computation 115 1 ( 1994 ) 38-94.  A. K. Wright and M. Felleisen. 1994. A Syntactic Approach to Type Soundness. Information and Computation 115 1 ( 1994 ) 38-94.","DOI":"10.1006\/inco.1994.1093"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3434305","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3434305","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3434305","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T21:24:35Z","timestamp":1750195475000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3434305"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,1,4]]},"references-count":36,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2021,1,4]]}},"alternative-id":["10.1145\/3434305"],"URL":"https:\/\/doi.org\/10.1145\/3434305","relation":{},"ISSN":["2475-1421"],"issn-type":[{"type":"electronic","value":"2475-1421"}],"subject":[],"published":{"date-parts":[[2021,1,4]]},"assertion":[{"value":"2021-01-04","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}