{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,2]],"date-time":"2026-02-02T11:25:00Z","timestamp":1770031500135,"version":"3.49.0"},"reference-count":80,"publisher":"Cambridge University Press (CUP)","license":[{"start":{"date-parts":[[2026,2,2]],"date-time":"2026-02-02T00:00:00Z","timestamp":1769990400000},"content-version":"unspecified","delay-in-days":397,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["cambridge.org"],"crossmark-restriction":true},"short-container-title":["J. Funct. Prog."],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    Algebraic effects and handlers is an increasingly popular paradigm for programming with effects. A key benefit is modularity: programs with effects are defined against an interface of operations, allowing the implementation of effects to be defined and refined without changing or recompiling programs. The behavior of effects is specified using equational theories, with equational proofs inheriting the same modularity. However, higher-order operations (that take computations as arguments) break this modularity: while they can often be encoded in terms of algebraic effects, this typically breaks modularity as operations defined this way are not encapsulated in an interface, inducing changes to programs and proofs upon refinement of the implementation. In this paper, we show that\n                    <jats:italic>syntactic overloading<\/jats:italic>\n                    is a viable solution to this modularity problem by defining\n                    <jats:italic>hefty algebras<\/jats:italic>\n                    : a formal framework that captures an overloading-based semantics of higher-order effects by defining modular elaborations from higher-order effect trees into primitive algebraic effects. We demonstrate how this approach scales to define a wide range of known higher-order effects from the literature and develop modular higher-order effect theories and modular reasoning principles that build on and extend the state of the art in modular algebraic effect theories. We formalize our contributions in Agda.\n                  <\/jats:p>","DOI":"10.1017\/s0956796825100142","type":"journal-article","created":{"date-parts":[[2026,2,2]],"date-time":"2026-02-02T01:23:44Z","timestamp":1769995424000},"update-policy":"https:\/\/doi.org\/10.1017\/policypage","source":"Crossref","is-referenced-by-count":0,"title":["Hefty algebras: Modular elaboration of higher-order effects"],"prefix":"10.1017","volume":"35","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-0059-5353","authenticated-orcid":false,"given":"CAS","family":"VAN DER REST","sequence":"first","affiliation":[{"name":"Shielded Technologies"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0622-7639","authenticated-orcid":false,"given":"CASPER","family":"BACH","sequence":"additional","affiliation":[{"name":"University of Southern Denmark"},{"name":"Delft University of Technology"}]}],"member":"56","published-online":{"date-parts":[[2026,2,2]]},"reference":[{"key":"S0956796825100142_ref68","doi-asserted-by":"crossref","unstructured":"van den Berg, B. & Schrijvers, T. (2023) A framework for higher-order effects & handlers. CoRR. abs\/2302.01415.","DOI":"10.2139\/ssrn.4383536"},{"key":"S0956796825100142_ref80","doi-asserted-by":"publisher","DOI":"10.1145\/3290318"},{"key":"S0956796825100142_ref23","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44622-2_21"},{"key":"S0956796825100142_ref15","unstructured":"Cenciarelli, P. & Moggi, E. (1993) A syntactic approach to modularity in denotational semantics."},{"key":"S0956796825100142_ref32","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009872"},{"key":"S0956796825100142_ref7","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2014.02.001"},{"key":"S0956796825100142_ref53","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00590-9_7"},{"key":"S0956796825100142_ref58","volume-title":"Denotational Semantics","author":"Schmidt","year":"1986"},{"key":"S0956796825100142_ref40","doi-asserted-by":"publisher","DOI":"10.1007\/3540543961_7"},{"key":"S0956796825100142_ref3","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796820000076"},{"key":"S0956796825100142_ref30","doi-asserted-by":"publisher","DOI":"10.1145\/3632898"},{"key":"S0956796825100142_ref49","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209166"},{"key":"S0956796825100142_ref20","unstructured":"Eisenberg, R. A. (ed.) (2019) Proceedings of the 12th ACM SIGPLAN International Symposium on Haskell, Haskell@ICFP 2019, Berlin, Germany, August 18\u201323, 2019. ACM."},{"key":"S0956796825100142_ref35","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-57262-3_1"},{"key":"S0956796825100142_ref17","first-page":"3127","article-title":"Cubical type theory: A constructive interpretation of the univalence axiom","volume":"4","author":"Cohen","year":"2017","journal-title":"FLAP"},{"key":"S0956796825100142_ref72","doi-asserted-by":"publisher","DOI":"10.1145\/3563355"},{"key":"S0956796825100142_ref52","doi-asserted-by":"publisher","DOI":"10.1023\/A:1023064908962"},{"key":"S0956796825100142_ref10","doi-asserted-by":"publisher","DOI":"10.1145\/3428194"},{"key":"S0956796825100142_ref66","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00053-0"},{"key":"S0956796825100142_ref12","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500581"},{"key":"S0956796825100142_ref24","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-02768-1_22"},{"key":"S0956796825100142_ref2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2005.06.002"},{"key":"S0956796825100142_ref59","doi-asserted-by":"publisher","DOI":"10.1145\/3331545.3342595"},{"key":"S0956796825100142_ref36","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009897"},{"key":"S0956796825100142_ref9","doi-asserted-by":"publisher","DOI":"10.1007\/s001650050047"},{"key":"S0956796825100142_ref43","doi-asserted-by":"publisher","DOI":"10.1145\/3290325"},{"key":"S0956796825100142_ref41","unstructured":"Moggi, E. (1989a) An Abstract View of Programming Languages. Technical Report ECS-LFCS-90-113. Edinburgh University, Department of Computer Science."},{"key":"S0956796825100142_ref21","doi-asserted-by":"publisher","DOI":"10.1145\/292540.292557"},{"key":"S0956796825100142_ref4","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129521000347"},{"key":"S0956796825100142_ref45","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2004.03.008"},{"key":"S0956796825100142_ref1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-36576-1_2"},{"key":"S0956796825100142_ref47","volume-title":"Foundations of Computing","author":"Pierce","year":"1991"},{"key":"S0956796825100142_ref6","volume-title":"Category Theory","author":"Awodey","year":"2010"},{"key":"S0956796825100142_ref62","unstructured":"Staton, S. (2013a) An algebraic presentation of predicate logic - (extended abstract). In Foundations of Software Science and Computation Structures - 16th International Conference, FOSSACS 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16\u201324, 2013. Proceedings. Springer, pp. 401\u2013417."},{"key":"S0956796825100142_ref65","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796808006758"},{"key":"S0956796825100142_ref75","unstructured":"Wadler, P. , Kokke, W. & Siek, J. G. (2020) Programming Language Foundations in Agda."},{"key":"S0956796825100142_ref73","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796821000034"},{"key":"S0956796825100142_ref74","doi-asserted-by":"publisher","DOI":"10.1145\/143165.143169"},{"key":"S0956796825100142_ref34","doi-asserted-by":"publisher","DOI":"10.1145\/199448.199528"},{"key":"S0956796825100142_ref11","doi-asserted-by":"publisher","DOI":"10.1017\/S095679681300018X"},{"key":"S0956796825100142_ref51","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45931-6_24"},{"key":"S0956796825100142_ref8","doi-asserted-by":"publisher","DOI":"10.1145\/3158096"},{"key":"S0956796825100142_ref42","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1989.39155"},{"key":"S0956796825100142_ref70","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.17415938"},{"key":"S0956796825100142_ref39","doi-asserted-by":"publisher","DOI":"10.1145\/3731678"},{"key":"S0956796825100142_ref78","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99336-8_17"},{"key":"S0956796825100142_ref37","doi-asserted-by":"publisher","DOI":"10.1145\/3656393"},{"key":"S0956796825100142_ref25","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.03.013"},{"key":"S0956796825100142_ref5","volume-title":"Arrows, Structures, and Functors: The Categorical Imperative","author":"Arbib","year":"1975"},{"key":"S0956796825100142_ref54","doi-asserted-by":"publisher","DOI":"10.1145\/3571255"},{"key":"S0956796825100142_ref48","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2014.10.015"},{"key":"S0956796825100142_ref44","unstructured":"Morrisett, G. & Uustalu, T. (eds) (2013) ACM SIGPLAN International Conference on Functional Programming, ICFP\u201913, Boston, MA, USA - September 25\u201327, 2013. ACM."},{"key":"S0956796825100142_ref55","doi-asserted-by":"crossref","unstructured":"Pretnar, M. (2015) An introduction to algebraic effects and handlers. invited tutorial paper. In The 31st Conference on the Mathematical Foundations of Programming Semantics, MFPS 2015, Nijmegen, The Netherlands, June 22\u201325, 2015. Elsevier, pp. 19\u201335.","DOI":"10.1016\/j.entcs.2015.12.003"},{"key":"S0956796825100142_ref71","unstructured":"van der Rest, C. & Poulsen, C. B. (2024) GitHub - heft-lang\/hefty-equations: Modular reasoning about (elaborations of) higher-order effects \u2014 github.com. https:\/\/github.com\/heft-lang\/hefty-equations."},{"key":"S0956796825100142_ref79","doi-asserted-by":"publisher","DOI":"10.1145\/3473578"},{"key":"S0956796825100142_ref22","doi-asserted-by":"publisher","DOI":"10.1145\/2603088.2603163"},{"key":"S0956796825100142_ref60","doi-asserted-by":"publisher","DOI":"10.1145\/2643135.2643145"},{"key":"S0956796825100142_ref26","doi-asserted-by":"crossref","unstructured":"Jaskelioff, M. (2008) Monatron: An extensible monad transformer library. In Implementation and Application of Functional Languages - 20th International Symposium, IFL 2008, Hatfield, UK, September 10\u201312, 2008. Revised Selected Papers. Springer, pp. 233\u2013248.","DOI":"10.1007\/978-3-642-24452-0_13"},{"key":"S0956796825100142_ref64","doi-asserted-by":"publisher","DOI":"10.1145\/174675.178068"},{"key":"S0956796825100142_ref13","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796809007205"},{"key":"S0956796825100142_ref19","doi-asserted-by":"publisher","DOI":"10.1145\/3331545.3342589"},{"key":"S0956796825100142_ref63","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2013.58"},{"key":"S0956796825100142_ref28","unstructured":"Jones, M. P. & Duponcheel, L. (1993) Composing Monads. Research Report YALEU\/DCS\/RR-1004. Yale University. New Haven, Connecticut, USA."},{"key":"S0956796825100142_ref67","unstructured":"Thielecke, H. (1997) Categorical Structure of Continuation Passing Style. PhD thesis. University of Edinburgh."},{"key":"S0956796825100142_ref31","doi-asserted-by":"publisher","DOI":"10.1145\/2804302.2804319"},{"key":"S0956796825100142_ref77","doi-asserted-by":"publisher","DOI":"10.1145\/2633357.2633358"},{"key":"S0956796825100142_ref46","doi-asserted-by":"publisher","DOI":"10.1145\/53990.54010"},{"key":"S0956796825100142_ref56","volume-title":"Homotopy Type Theory: Univalent Foundations of Mathematics","author":"Program","year":"2013"},{"key":"S0956796825100142_ref27","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-59451-5_4"},{"key":"S0956796825100142_ref50","first-page":"17","article-title":"A structural approach to operational semantics","volume":"60","author":"Plotkin","year":"2004","journal-title":"J. Log. Algebraic Methods Program."},{"key":"S0956796825100142_ref16","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796899003342"},{"key":"S0956796825100142_ref38","volume-title":"Studies in Proof Theory","volume":"1","author":"Martin-L\u00f6f","year":"1984"},{"key":"S0956796825100142_ref33","doi-asserted-by":"publisher","DOI":"10.1007\/s10990-006-0480-6"},{"key":"S0956796825100142_ref61","doi-asserted-by":"crossref","unstructured":"Sculthorpe, N. , Torrini, P. & Mosses, P. D. (2015) A modular structural operational semantics for delimited continuations. In Proceedings of the Workshop on Continuations, WoC 2016, London, UK, April 12th 2015, pp. 63\u201380.","DOI":"10.4204\/EPTCS.212.5"},{"key":"S0956796825100142_ref76","doi-asserted-by":"crossref","unstructured":"Wu, N. & Schrijvers, T. (2015) Fusion for free - efficient algebraic effect handlers. In Mathematics of Program Construction - 12th International Conference, MPC 2015, K\u00f6nigswinter, Germany, June 29\u2013July 1, 2015. Proceedings. Springer, pp. 302\u2013322.","DOI":"10.1007\/978-3-319-19797-5_15"},{"key":"S0956796825100142_ref29","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500590"},{"key":"S0956796825100142_ref18","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500587"},{"key":"S0956796825100142_ref69","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-89051-3_11"},{"key":"S0956796825100142_ref14","unstructured":"Castagna, G. & Gordon, A. D. (eds) (2017) Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18\u201320, 2017. ACM."},{"key":"S0956796825100142_ref57","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2010.03.012"}],"container-title":["Journal of Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0956796825100142","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,2]],"date-time":"2026-02-02T01:23:48Z","timestamp":1769995428000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0956796825100142\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"references-count":80,"alternative-id":["S0956796825100142"],"URL":"https:\/\/doi.org\/10.1017\/s0956796825100142","relation":{},"ISSN":["0956-7968","1469-7653"],"issn-type":[{"value":"0956-7968","type":"print"},{"value":"1469-7653","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"\u00a9 The Author(s), 2026. Published by Cambridge University Press","name":"copyright","label":"Copyright","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}},{"value":"This is an Open Access article, distributed under the terms of the Creative Commons Attribution licence (https:\/\/creativecommons.org\/licenses\/by\/4.0\/), which permits unrestricted re-use, distribution and reproduction, provided the original article is properly cited.","name":"license","label":"License","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}],"article-number":"e25"}}