{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:04:42Z","timestamp":1767927882548,"version":"3.49.0"},"reference-count":49,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2019,11,21]],"date-time":"2019-11-21T00:00:00Z","timestamp":1574294400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000181","name":"Air Force Office of Scientific Research","doi-asserted-by":"crossref","award":["FA9550-17-1-0326"],"award-info":[{"award-number":["FA9550-17-1-0326"]}],"id":[{"id":"10.13039\/100000181","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100004329","name":"Slovenian Research Agency","doi-asserted-by":"crossref","award":["P1 0294"],"award-info":[{"award-number":["P1 0294"]}],"id":[{"id":"10.13039\/501100004329","id-type":"DOI","asserted-by":"crossref"}]},{"name":"European Union's Horizon 2020 research and innovation programme"},{"name":"Marie Sk\u0142odowska-Curie","award":["731143"],"award-info":[{"award-number":["731143"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Program. Lang. Syst."],"published-print":{"date-parts":[[2020,3,31]]},"abstract":"<jats:p>\n            The article investigates behavioural equivalence between programs in a call-by-value functional language extended with a signature of (algebraic) effect-triggering operations. Two programs are considered as being behaviourally equivalent if they enjoy the same behavioural properties. To formulate this, we define a logic whose formulas specify behavioural properties. A crucial ingredient is a collection of\n            <jats:italic>modalities<\/jats:italic>\n            expressing effect-specific aspects of behaviour. We give a general theory of such modalities. If two conditions,\n            <jats:italic>openness<\/jats:italic>\n            and\n            <jats:italic>decomposability<\/jats:italic>\n            , are satisfied by the modalities, then the logically specified behavioural equivalence coincides with a modality-defined notion of applicative bisimilarity, which can be proven to be a congruence by a generalisation of Howe\u2019s method. We show that the openness and decomposability conditions hold for several examples of algebraic effects: nondeterminism, probabilistic choice, global store, and input\/output.\n          <\/jats:p>","DOI":"10.1145\/3363518","type":"journal-article","created":{"date-parts":[[2019,11,21]],"date-time":"2019-11-21T13:35:22Z","timestamp":1574343322000},"page":"1-45","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":13,"title":["Behavioural Equivalence via Modalities for Algebraic Effects"],"prefix":"10.1145","volume":"42","author":[{"given":"Alex","family":"Simpson","sequence":"first","affiliation":[{"name":"University of Ljubljana, Jadranska, Ljubljana, Slovenia"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Niels","family":"Voorneveld","sequence":"additional","affiliation":[{"name":"University of Ljubljana, Jadranska, Ljubljana, Slovenia"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2019,11,21]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480887"},{"key":"e_1_2_1_2_1","volume-title":"Research Topics in Functional Programming, David A","author":"Abramsky Samson","unstructured":"Samson Abramsky. 1990. The lazy lambda calculus. In Research Topics in Functional Programming, David A. Turner (Ed.). Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 65--116."},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(91)90065-T"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009878"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535869"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2013.33"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/237721.237807"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2015.03.047"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2455.2460"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-15545-6_7"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1989.39174"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1996.0008"},{"key":"e_1_2_1_13_1","volume-title":"Introduction to Coalgebra: Towards Mathematics of States and Observation","author":"Jacobs Bart","unstructured":"Bart Jacobs. 2016. Introduction to Coalgebra: Towards Mathematics of States and Observation. Cambridge University Press, Cambridge, UK."},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2010.29"},{"key":"e_1_2_1_15_1","volume-title":"Relating computational effects by TT-lifting","unstructured":"Shin-ya Katsumata. 2011. Relating computational effects by TT-lifting. In Automata, Languages and Programming, Luca Aceto, Monika Henzinger, and Ji\u0159\u00ed Sgall (Eds.). Springer Berlin, Berlin, 174--185."},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2011.09.023"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2017.8005117"},{"key":"e_1_2_1_18_1","volume-title":"Higher Order Operational Techniques in Semantics, Andrew D","author":"Lassen S\u00f8ren B\u00f8gh","unstructured":"S\u00f8ren B\u00f8gh Lassen. 1998. Relational reasoning about contexts. In Higher Order Operational Techniques in Semantics, Andrew D. Gordon and Andrew M. Pitts (Eds.). Cambridge University Press, New York, 91--136. http:\/\/dl.acm.org\/citation.cfm?id&equals;309656.309665"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10990-006-0480-6"},{"key":"e_1_2_1_21_1","series-title":"Lecture Notes in Computer Science","volume-title":"Similarity quotients as final coalgebras","author":"Levy Paul Blain","unstructured":"Paul Blain Levy. 2011. Similarity quotients as final coalgebras. Lecture Notes in Computer Science, vol. 6604. Springer, Berlin, 27--41."},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0890-5401(03)00088-9"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CSL.2018.29"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341708"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jsc.2010.08.004"},{"key":"e_1_2_1_26_1","volume-title":"A Calculus of Communicating Systems","author":"Milner Robin","unstructured":"Robin Milner. 1982. A Calculus of Communicating Systems. Springer-Verlag New York, Inc., Secaucus, NJ."},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90052-4"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-010-0153-4"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796808006953"},{"key":"e_1_2_1_30_1","first-page":"275","article-title":"Non-determinism in a functional setting. In Symposium on Logic in Computer Science, Montreal, Ont","volume":"8","author":"Luke Ong C.-H.","year":"1993","unstructured":"C.-H. Luke Ong. 1993. Non-determinism in a functional setting. In Symposium on Logic in Computer Science, Montreal, Ont., Canada. 8 (1993), 275--286.","journal-title":"Canada."},{"key":"e_1_2_1_31_1","series-title":"Lecture Notes in Computer Science","volume-title":"Concurrency and automata on infinite sequences","author":"Park David","unstructured":"David Park. 1981. Concurrency and automata on infinite sequences. Lecture Notes in Computer Science, vol. 154. Springer, Berlin, 561--572."},{"key":"e_1_2_1_32_1","volume-title":"modular and compositional verification of the input\/output behavior of programs","author":"Penninckx Willem","unstructured":"Willem Penninckx, Bart Jacobs, and Frank Piessens. 2015. Sound, modular and compositional verification of the input\/output behavior of programs. In Programming Languages and Systems, Jan Vitek (Ed.). Springer Berlin, Berlin, 158--182."},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4471-3182-3_11"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129500003066"},{"key":"e_1_2_1_35_1","volume-title":"Advanced Topics in Types and Programming Languages","author":"Pitts A. M.","unstructured":"A. M. Pitts. 2005. Typed operational reasoning. In Advanced Topics in Types and Programming Languages, B. C. Pierce (Ed.). The MIT Press, London, UK, Chapter 7, 245--289."},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(77)90044-5"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.5555\/1812941.1812943"},{"key":"e_1_2_1_38_1","volume-title":"Foundations of Software Science and Computation Structures","author":"Plotkin Gordon","unstructured":"Gordon Plotkin and John Power. 2001. Adequacy for algebraic effects. In Foundations of Software Science and Computation Structures. Springer Berlin, Berlin, 1--24."},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.5555\/646794.704856"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2008.45"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-9(4:23)2013"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1977.32"},{"key":"e_1_2_1_43_1","volume-title":"Introduction to Bisimulation and Coinduction","author":"Sangiorgi Davide","unstructured":"Davide Sangiorgi. 2011. Introduction to Bisimulation and Coinduction. Cambridge University Press, Cambridge, UK."},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/1889997.1890002"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","unstructured":"Davide Sangiorgi and Jan Rutten (Eds.). 2011. Advanced Topics in Bisimulation and Coinduction. Cambridge University Press Cambridge UK. DOI:https:\/\/doi.org\/10.1017\/CBO9780511792588","DOI":"10.1017\/CBO9780511792588"},{"key":"e_1_2_1_46_1","volume-title":"Programming Languages and Systems","author":"Simpson Alex","unstructured":"Alex Simpson and Niels Voorneveld. 2018. Behavioural equivalence via modalities for algebraic effects. In Programming Languages and Systems. Springer International Publishing, Cham, 300--326."},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837655"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/2499370.2491978"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-84882-912-1_15"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2019.09.015"}],"container-title":["ACM Transactions on Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3363518","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3363518","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3363518","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:44:25Z","timestamp":1750203865000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3363518"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,11,21]]},"references-count":49,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2020,3,31]]}},"alternative-id":["10.1145\/3363518"],"URL":"https:\/\/doi.org\/10.1145\/3363518","relation":{},"ISSN":["0164-0925","1558-4593"],"issn-type":[{"value":"0164-0925","type":"print"},{"value":"1558-4593","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,11,21]]},"assertion":[{"value":"2018-05-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2019-07-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2019-11-21","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}