{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,8]],"date-time":"2025-11-08T17:52:51Z","timestamp":1762624371824,"version":"3.40.3"},"publisher-location":"Cham","reference-count":36,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030449131"},{"type":"electronic","value":"9783030449148"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2020,4,18]],"date-time":"2020-04-18T00:00:00Z","timestamp":1587168000000},"content-version":"vor","delay-in-days":108,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Runners of algebraic effects, also known as comodels, provide a mathematical model of resource management. We show that they also give rise to a programming concept that models top-level external resources, as well as allows programmers to modularly define their own intermediate \u201cvirtual machines\u201d. We capture the core ideas of programming with runners in an equational calculus <jats:inline-formula><jats:alternatives><jats:tex-math>$$\\lambda _{\\mathsf {coop}}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:msub>\n                    <mml:mi>\u03bb<\/mml:mi>\n                    <mml:mi>coop<\/mml:mi>\n                  <\/mml:msub>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula>, which we equip with a sound and coherent denotational semantics that guarantees the linear use of resources and execution of finalisation code. We accompany <jats:inline-formula><jats:alternatives><jats:tex-math>$$\\lambda _{\\mathsf {coop}}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:msub>\n                    <mml:mi>\u03bb<\/mml:mi>\n                    <mml:mi>coop<\/mml:mi>\n                  <\/mml:msub>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula> with examples of runners in action, provide a prototype language implementation in <jats:sc>OCaml<\/jats:sc>, as well as a <jats:sc>Haskell<\/jats:sc> library based on <jats:inline-formula><jats:alternatives><jats:tex-math>$$\\lambda _{\\mathsf {coop}}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:msub>\n                    <mml:mi>\u03bb<\/mml:mi>\n                    <mml:mi>coop<\/mml:mi>\n                  <\/mml:msub>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula>.<\/jats:p>","DOI":"10.1007\/978-3-030-44914-8_2","type":"book-chapter","created":{"date-parts":[[2020,4,17]],"date-time":"2020-04-17T10:02:53Z","timestamp":1587117773000},"page":"29-55","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":8,"title":["Runners in Action"],"prefix":"10.1007","author":[{"given":"Danel","family":"Ahman","sequence":"first","affiliation":[]},{"given":"Andrej","family":"Bauer","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2020,4,18]]},"reference":[{"key":"2_CR1","unstructured":"Ahman, D.: Library Haskell-Coop. Available at https:\/\/github.com\/danelahman\/haskell-coop (2019)"},{"key":"2_CR2","doi-asserted-by":"crossref","unstructured":"Ahman, D., Fournet, C., Hritcu, C., Maillard, K., Rastogi, A., Swamy, N.: Recalling a witness: foundations and applications of monotonic state. PACMPL 2(POPL), 65:1\u201365:30 (2018)","DOI":"10.1145\/3158153"},{"key":"2_CR3","doi-asserted-by":"crossref","unstructured":"Bauer, A., Pretnar, M.: An effect system for algebraic effects and handlers. Logical Methods in Computer Science 10(4) (2014)","DOI":"10.2168\/LMCS-10(4:9)2014"},{"key":"2_CR4","doi-asserted-by":"crossref","unstructured":"Bauer, A., Pretnar, M.: Programming with algebraic effects and handlers. J. Log. Algebr. Meth. Program. 84(1), 108\u2013123 (2015)","DOI":"10.1016\/j.jlamp.2014.02.001"},{"key":"2_CR5","unstructured":"Bauer, A.: What is algebraic about algebraic effects and handlers? CoRR abs\/1807.05923 (2018)"},{"key":"2_CR6","unstructured":"Bauer, A.: Programming language coop. Available at https:\/\/github.com\/andrejbauer\/coop (2019)"},{"key":"2_CR7","doi-asserted-by":"crossref","unstructured":"Benton, N., Kennedy, A.: Exceptional syntax. Journal of Functional Programming 11(4), 395\u2013410 (2001)","DOI":"10.1017\/S0956796801004099"},{"key":"2_CR8","doi-asserted-by":"crossref","unstructured":"Delignat-Lavaud, A., Fournet, C., Kohlweiss, M., Protzenko, J., Rastogi, A., Swamy, N., Zanella-Beguelin, S., Bhargavan, K., Pan, J., Zinzindohoue, J.K.: Implementing and proving the tls 1.3 record layer. In: 2017 IEEE Symp. on Security and Privacy (SP). pp. 463\u2013482 (2017)","DOI":"10.1109\/SP.2017.58"},{"key":"2_CR9","doi-asserted-by":"crossref","unstructured":"Dolan, S., Eliopoulos, S., Hillerstr\u00f6m, D., Madhavapeddy, A., Sivaramakrishnan, K.C., White, L.: Concurrent system programming with effect handlers. In: Wang, M., Owens, S. (eds.) Trends in Functional Programming. pp. 98\u2013117. Springer International Publishing, Cham (2018)","DOI":"10.1007\/978-3-319-89719-6_6"},{"key":"2_CR10","doi-asserted-by":"crossref","unstructured":"Foster, J.N., Greenwald, M.B., Moore, J.T., Pierce, B.C., Schmitt, A.: Combinators for bidirectional tree transformations: A linguistic approach to the view-update problem. ACM Trans. Program. Lang. Syst. 29(3) (2007)","DOI":"10.1145\/1232420.1232424"},{"key":"2_CR11","doi-asserted-by":"crossref","unstructured":"Hyland, M., Plotkin, G., Power, J.: Combining effects: Sum and tensor. Theor. Comput. Sci. 357(1\u20133), 70\u201399 (2006)","DOI":"10.1016\/j.tcs.2006.03.013"},{"key":"2_CR12","doi-asserted-by":"crossref","unstructured":"Kammar, O., Lindley, S., Oury, N.: Handlers in action. In: Proc. of 18th ACM SIGPLAN Int. Conf. on Functional Programming, ICFP 2013. ACM (2013)","DOI":"10.1145\/2500365.2500590"},{"key":"2_CR13","doi-asserted-by":"crossref","unstructured":"Katsumata, S., Rivas, E., Uustalu, T.: Interaction laws of monads and comonads. CoRR abs\/1912.13477 (2019)","DOI":"10.1145\/3373718.3394808"},{"key":"2_CR14","doi-asserted-by":"crossref","unstructured":"Kiselyov, O., Ishii, H.: Freer monads, more extensible effects. In: Proc. of 2015 ACM SIGPLAN Symp. on Haskell. pp. 94\u2013105. Haskell \u201915, ACM (2015)","DOI":"10.1145\/2804302.2804319"},{"key":"2_CR15","unstructured":"Koopman, P., Fokker, J., Smetsers, S., van Eekelen, M., Plasmeijer, R.: Functional Programming in Clean. University of Nijmegen (1998), draft"},{"key":"2_CR16","doi-asserted-by":"crossref","unstructured":"Leijen, D.: Structured asynchrony with algebraic effects. In: Proceedings of the 2nd ACM SIGPLAN International Workshop on Type-Driven Development, TyDe@ICFP 2017, Oxford, UK, September 3, 2017. pp. 16\u201329. ACM (2017)","DOI":"10.1145\/3122975.3122977"},{"key":"2_CR17","unstructured":"Leijen, D.: Algebraic effect handlers with resources and deep finalization. Tech. Rep. MSR-TR-2018-10, Microsoft Research (April 2018)"},{"key":"2_CR18","unstructured":"Leijen, D.: Programming with implicit values, functions, and control (or, implicit functions: Dynamic binding with lexical scoping). Tech. Rep. MSR-TR-2019-7, Microsoft Research (March 2019)"},{"key":"2_CR19","unstructured":"Levy, P.B.: Call-By-Push-Value: A Functional\/Imperative Synthesis, Semantics Structures in Computation, vol. 2. Springer (2004)"},{"key":"2_CR20","doi-asserted-by":"crossref","unstructured":"Miltner, A., Maina, S., Fisher, K., Pierce, B.C., Walker, D., Zdancewic, S.: Synthesizing symmetric lenses. Proc. ACM Program. Lang. 3(ICFP), 95:1\u201395:28 (2019)","DOI":"10.1145\/3341699"},{"key":"2_CR21","doi-asserted-by":"crossref","unstructured":"M\u00f8gelberg, R.E., Staton, S.: Linear usage of state. Logical Methods in Computer Science 10(1) (2014)","DOI":"10.2168\/LMCS-10(1:17)2014"},{"key":"2_CR22","unstructured":"Moggi, E.: Computational lambda-calculus and monads. In: Proc. of 4th Ann. Symp. on Logic in Computer Science, LICS 1989. pp. 14\u201323. IEEE (1989)"},{"key":"2_CR23","doi-asserted-by":"crossref","unstructured":"Moggi, E.: Notions of computation and monads. Inf. Comput. 93(1), 55\u201392 (1991)","DOI":"10.1016\/0890-5401(91)90052-4"},{"key":"2_CR24","unstructured":"O\u2019Connor, R.: Functor is to lens as applicative is to biplate: Introducing multiplate. CoRR abs\/1103.2841 (2011)"},{"key":"2_CR25","doi-asserted-by":"crossref","unstructured":"Plotkin, G., Power, J.: Semantics for algebraic operations. In: Proc. of 17th Conf. on the Mathematical Foundations of Programming Semantics, MFPS XVII. ENTCS, vol. 45, pp. 332\u2013345. Elsevier (2001)","DOI":"10.1016\/S1571-0661(04)80970-8"},{"key":"2_CR26","doi-asserted-by":"crossref","unstructured":"Plotkin, G., Power, J.: Algebraic operations and generic effects. Appl. Categor. Struct. (1), 69\u201394 (2003)","DOI":"10.1023\/A:1023064908962"},{"key":"2_CR27","doi-asserted-by":"crossref","unstructured":"Plotkin, G., Power, J.: Tensors of comodels and models for operational semantics. In: Proc. of 24th Conf. on Mathematical Foundations of Programming Semantics, MFPS XXIV. ENTCS, vol. 218, pp. 295\u2013311. Elsevier (2008)","DOI":"10.1016\/j.entcs.2008.10.018"},{"key":"2_CR28","doi-asserted-by":"crossref","unstructured":"Plotkin, G.D., Power, J.: Notions of computation determine monads. In: Proc. of 5th Int. Conf. on Foundations of Software Science and Computation Structures, FOSSACS 2002. LNCS, vol. 2303, pp. 342\u2013356. Springer (2002)","DOI":"10.1007\/3-540-45931-6_24"},{"key":"2_CR29","doi-asserted-by":"crossref","unstructured":"Plotkin, G.D., Pretnar, M.: A logic for algebraic effects. In: Proc. of 23th Ann. IEEE Symp. on Logic in Computer Science, LICS 2008. pp. 118\u2013129. IEEE (2008)","DOI":"10.1109\/LICS.2008.45"},{"key":"2_CR30","doi-asserted-by":"crossref","unstructured":"Plotkin, G.D., Pretnar, M.: Handling algebraic effects. Logical Methods in Computer Science 9(4:23) (2013)","DOI":"10.2168\/LMCS-9(4:23)2013"},{"key":"2_CR31","doi-asserted-by":"crossref","unstructured":"Power, J., Shkaravska, O.: From comodels to coalgebras: State and arrays. Electr. Notes Theor. Comput. Sci. 106, 297\u2013314 (2004)","DOI":"10.1016\/j.entcs.2004.02.041"},{"key":"2_CR32","unstructured":"Power, J.: Enriched Lawvere theories. Theory Appl. Categ 6(7), 83\u201393 (1999)"},{"key":"2_CR33","unstructured":"Pretnar, M.: The Logic and Handling of Algebraic Effects. Ph.D. thesis, School of Informatics, University of Edinburgh (2010)"},{"key":"2_CR34","doi-asserted-by":"crossref","unstructured":"Saleh, A.H., Karachalias, G., Pretnar, M., Schrijvers, T.: Explicit effect subtyping. In: Proc. of 27th European Symposium on Programming, ESOP 2018. pp. 327\u2013354. LNCS, Springer (2018)","DOI":"10.1007\/978-3-319-89884-1_12"},{"key":"2_CR35","doi-asserted-by":"crossref","unstructured":"Uustalu, T.: Stateful runners of effectful computations. Electr. Notes Theor. Comput. Sci. 319, 403\u2013421 (2015)","DOI":"10.1016\/j.entcs.2015.12.024"},{"key":"2_CR36","doi-asserted-by":"crossref","unstructured":"Wadler, P.: The essence of functional programming. In: Sethi, R. (ed.) Proc. of 19th Ann. ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages, POPL 1992. pp. 1\u201314. ACM (1992)","DOI":"10.1145\/143165.143169"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-44914-8_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,6,30]],"date-time":"2022-06-30T17:08:20Z","timestamp":1656608900000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-44914-8_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030449131","9783030449148"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-44914-8_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"18 April 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ESOP","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"European Symposium on Programming","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Dublin","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Ireland","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 April 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30 April 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"esop2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.etaps.org\/2020\/esop","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"87","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"27","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"31% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3,3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"11-12","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"The conference could not take place due to the COVID-19 pandemic. There was an online event on July 2, 2020.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}