{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,18]],"date-time":"2026-06-18T15:53:46Z","timestamp":1781798026429,"version":"3.54.5"},"reference-count":75,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2026,1,8]]},"abstract":"<jats:p>This paper studies the design of programming languages with handlers of higher-order effectful operations \u2013 effectful operations that may take in computations as arguments or return computations as output. We present and analyse a core calculus with higher-kinded impredicative polymorphism, handlers of higher-order effectful operations, and optionally general recursion. The distinctive design choice of this calculus is that handlers are carried by lawless raw monads, while the computation judgements still satisfy the monadic laws judgementally. We present the calculus with a logical framework and give denotational models of the calculus using realizability semantics. We prove closed-term canonicity and parametricity for the recursion-free fragment of the language using synthetic Tait computability and a novel form of the \u22a4\u22a4-lifting technique.<\/jats:p>","DOI":"10.1145\/3776678","type":"journal-article","created":{"date-parts":[[2026,1,8]],"date-time":"2026-01-08T18:59:43Z","timestamp":1767898783000},"page":"1036-1065","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Handling Higher-Order Effectful Operations with Judgemental Monadic Laws"],"prefix":"10.1145","volume":"10","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-5573-3357","authenticated-orcid":false,"given":"Zhixuan","family":"Yang","sequence":"first","affiliation":[{"name":"Imperial College London, London, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4161-985X","authenticated-orcid":false,"given":"Nicolas","family":"Wu","sequence":"additional","affiliation":[{"name":"Imperial College London, London, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2026,1,8]]},"reference":[{"key":"e_1_2_2_1_1","unstructured":"Agda Developers. 2025. Agda. https:\/\/agda.readthedocs.io\/"},{"key":"e_1_2_2_2_1","doi-asserted-by":"crossref","unstructured":"Thorsten Altenkirch Martin Hofmann and Thomas Streicher. 1995. Categorical reconstruction of a reduction free normalization proof. In Category Theory and Computer Science David Pitt David E. Rydeheard and Peter Johnstone (Eds.). Springer Berlin Heidelberg 182\u2013199.","DOI":"10.1007\/3-540-60164-3_27"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571255"},{"key":"e_1_2_2_4_1","unstructured":"Andrej Bauer. 2022. Notes on Realizability. https:\/\/github.com\/andrejbauer\/notes-on-realizability Lecture notes for the Midlands Graduate School 2022 lecture series on realizability"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-10(4:9)2014"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(85)90088-x"},{"key":"e_1_2_2_7_1","volume-title":"Handbook of Categorical Algebra","author":"Borceux Francis","unstructured":"Francis Borceux. 1994. Handbook of Categorical Algebra: Volume 3, Sheaf Theory. 3, Cambridge University Press."},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.46298\/lmcs-20(4:17)2024"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209197"},{"key":"e_1_2_2_10_1","unstructured":"Tom de Jong. 2024. Categorical Realizability. https:\/\/github.com\/andrejbauer\/notes-on-realizability Lecture notes for the course on Categorical Realizability at the Midlands Graduate School 2024"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500582"},{"key":"e_1_2_2_12_1","unstructured":"Marcelo Fiore. 2022. Semantic Analysis of Normalisation by Evaluation for Typed Lambda Calculus. arxiv:2207.08777. 10.48550\/arXiv.2207.08777"},{"key":"e_1_2_2_13_1","unstructured":"Peter Freyd. 1978. On proving that 1 is an indecomposable projective in various free categories. Manuscript."},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632854"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2034773.2034777"},{"key":"e_1_2_2_16_1","unstructured":"Jean-Yves Girard. 1972. Interpr\u00e9tation fonctionelle et \u00e9limination des coupures de l\u2019arithm\u00e9tique d\u2019ordre sup\u00e9rieur. Universit\u00e9 Paris VII."},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(86)90044-7"},{"key":"e_1_2_2_18_1","volume-title":"Proofs and types","author":"Girard Jean-Yves","unstructured":"Jean-Yves Girard. 1989. Proofs and types. Cambridge University Press."},{"key":"e_1_2_2_19_1","unstructured":"Daniel Gratzer Michael Shulman and Jonathan Sterling. 2022. Strict universes for Grothendieck topoi. arxiv:2202.12012. arxiv:2202.12012"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632852"},{"key":"e_1_2_2_21_1","volume-title":"Practical Foundations for Programming Languages","author":"Harper Robert","unstructured":"Robert Harper. 2016. Practical Foundations for Programming Languages (2nd ed.). Cambridge University Press, Cambridge.","edition":"2"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/138027.138060"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511526619.004"},{"key":"e_1_2_2_24_1","unstructured":"Xu Huang. 2023. Synthetic Tait Computability the Hard Way. arxiv:2310.02051. arxiv:2310.02051"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0084217"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00590-9_6"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2010.09.011"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1017\/s0956796806006034"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103698"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796820000271"},{"key":"e_1_2_2_31_1","volume-title":"Relational Reasoning about Functions and Nondeterminism. Ph. D. Dissertation","author":"Lassen S\u00f8ren B\u00f8gh","unstructured":"S\u00f8ren B\u00f8gh Lassen. 1998. Relational Reasoning about Functions and Nondeterminism. Ph. D. Dissertation. Aarhus University. https:\/\/www.brics.dk\/DS\/98\/2\/ Series: BRICS Dissertation Series"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/1411204.1411245"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0890-5401(03)00088-9"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/11417170_20"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129597002387"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/73560.73564"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1093\/oso\/9780198538356.001.0001"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2012.10.020"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-0927-0"},{"key":"e_1_2_2_40_1","volume-title":"Studies in Logic and the Foundations of Mathematics. 82","author":"Martin-L\u00f6f Per","unstructured":"Per Martin-L\u00f6f. 1975. About models for intuitionistic type theories and the notion of definitional equality. In Studies in Logic and the Foundations of Mathematics. 82, Elsevier, 81\u2013109."},{"key":"e_1_2_2_41_1","volume-title":"An Intuitionistic Theory of Types: Predicative Part. In Logic Colloquium 73 Proceedings of the Logic Colloquium, H. E. Rose and J. C. Shepherdson (Eds.). Elsevier, 73\u2013118","author":"Martin-L\u00f6f Per","year":"1975","unstructured":"Per Martin-L\u00f6f. 1975. An Intuitionistic Theory of Types: Predicative Part. In Logic Colloquium 73 Proceedings of the Logic Colloquium, H. E. Rose and J. C. Shepherdson (Eds.). Elsevier, 73\u2013118."},{"key":"e_1_2_2_42_1","volume-title":"Laboratory for Foundations of Computer Science","author":"Martin-L\u00f6f Per","year":"1987","unstructured":"Per Martin-L\u00f6f. 1987. The Logic of Judgements. https:\/\/raw.githubusercontent.com\/michaelt\/martin-lof\/master\/pdfs\/The-logic-of-judgements-typeset-1987.pdf Talk at Workshop on General Logic, Laboratory for Foundations of Computer Science, University of Edinburgh, 23-27 February 1987"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/3731678"},{"key":"e_1_2_2_44_1","volume-title":"An Abstract View of Programming Languages","author":"Moggi Eugenio","unstructured":"Eugenio Moggi. 1989. An Abstract View of Programming Languages. Edinburgh University, Department of Computer Science."},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498670"},{"key":"e_1_2_2_46_1","volume-title":"Domain Theory in Realizability Toposes. Ph. D. Dissertation","author":"Phoa Wesley","unstructured":"Wesley Phoa. 1991. Domain Theory in Realizability Toposes. Ph. D. Dissertation. University of Edinburgh. https:\/\/www.lfcs.inf.ed.ac.uk\/reports\/91\/ECS-LFCS-91-171\/"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209166"},{"key":"e_1_2_2_48_1","volume-title":"Lambda Definability and Logical Relations","author":"Plotkin Gordon","year":"1973","unstructured":"Gordon Plotkin. 1973. Lambda Definability and Logical Relations. University of Edinburgh. https:\/\/homepages.inf.ed.ac.uk\/gdp\/publications\/logical_relations_1973.pdf"},{"key":"e_1_2_2_49_1","volume-title":"To H. B. Curry: Essays in Combinatory Logic, Lambda Calculus, and Formalism","author":"Plotkin Gordon","unstructured":"Gordon Plotkin. 1980. Lambda-Definability in the Full Type Hierarchy. In To H. B. Curry: Essays in Combinatory Logic, Lambda Calculus, and Formalism, J. P. Seldin and J. R. Hindley (Eds.). Academic Press, 363\u2013373. https:\/\/homepages.inf.ed.ac.uk\/gdp\/publications\/Lambda_Definability.pdf"},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(04)80970-8"},{"key":"e_1_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45931-6_24"},{"key":"e_1_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1023064908962"},{"key":"e_1_2_2_53_1","doi-asserted-by":"publisher","unstructured":"Gordon Plotkin and Matija Pretnar. 2009. Handlers of Algebraic Effects. In Programming Languages and Systems Giuseppe Castagna (Ed.). Springer Berlin Heidelberg 80\u201394. https:\/\/doi.org\/10.1007\/978-3-642-00590-9_7 10.1007\/978-3-642-00590-9_7","DOI":"10.1007\/978-3-642-00590-9_7"},{"key":"e_1_2_2_54_1","doi-asserted-by":"publisher","DOI":"10.2168\/lmcs-9(4:23)2013"},{"key":"e_1_2_2_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498693"},{"key":"e_1_2_2_56_1","volume-title":"Continuity and effectiveness in topoi. Ph. D. Dissertation","author":"Rosolini Giuseppe","unstructured":"Giuseppe Rosolini. 1986. Continuity and effectiveness in topoi. Ph. D. Dissertation. University of Oxford."},{"key":"e_1_2_2_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/3331545.3342595"},{"key":"e_1_2_2_58_1","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(90)90056-J"},{"key":"e_1_2_2_59_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0019-9958(85)80001-2"},{"key":"e_1_2_2_60_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.6990769"},{"key":"e_1_2_2_61_1","unstructured":"Jonathan Sterling. 2022. Na\u00efve logical relations in synthetic Tait computability. June Unpublished manuscript"},{"key":"e_1_2_2_62_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS52264.2021.9470719"},{"key":"e_1_2_2_63_1","doi-asserted-by":"publisher","DOI":"10.1145\/3474834"},{"key":"e_1_2_2_64_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.FSCD.2022.5"},{"key":"e_1_2_2_65_1","unstructured":"Thomas Streicher. 2017. Realizability. https:\/\/www2.mathematik.tu-darmstadt.de\/~streicher\/REAL\/REAL.pdf Lecture notes"},{"key":"e_1_2_2_66_1","doi-asserted-by":"publisher","DOI":"10.2307\/2271658"},{"key":"e_1_2_2_67_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2024.103086"},{"key":"e_1_2_2_68_1","volume-title":"Casper Bach Poulsen, and Nicolas Wu","author":"van den Berg Birthe","year":"2021","unstructured":"Birthe van den Berg, Tom Schrijvers, Casper Bach Poulsen, and Nicolas Wu. 2021. Latent Effects for Reusable Language Components. In Programming Languages and Systems, Hakjoo Oh (Ed.). Springer International Publishing, Cham. 182\u2013201."},{"key":"e_1_2_2_69_1","volume-title":"Realizability: an introduction to its categorical side","author":"van Oosten Jaap","unstructured":"Jaap van Oosten. 2008. Realizability: an introduction to its categorical side (1st ed.). Elsevier, Oxford.","edition":"1"},{"key":"e_1_2_2_70_1","doi-asserted-by":"publisher","DOI":"10.1145\/2633357.2633358"},{"key":"e_1_2_2_71_1","unstructured":"Zhixuan Yang. 2025. Revisiting the Logical Framework for Locally Cartesian Closed Categories. https:\/\/yangzhixuan.github.io\/pdf\/lcclf.pdf Manuscript"},{"key":"e_1_2_2_72_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99336-8_17"},{"key":"e_1_2_2_73_1","doi-asserted-by":"publisher","DOI":"10.1145\/3473578"},{"key":"e_1_2_2_74_1","doi-asserted-by":"publisher","DOI":"10.1145\/3607850"},{"key":"e_1_2_2_75_1","doi-asserted-by":"publisher","unstructured":"Zhixuan Yang and Nicolas Wu. 2025. Handling Higher-Order Effectful Operations with Judgemental Monadic Laws. arxiv:2511.05739. https:\/\/doi.org\/10.48550\/arXiv.2511.05739 10.48550\/arXiv.2511.05739","DOI":"10.48550\/arXiv.2511.05739"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3776678","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,6,18]],"date-time":"2026-06-18T15:17:53Z","timestamp":1781795873000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3776678"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,1,8]]},"references-count":75,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2026,1,8]]}},"alternative-id":["10.1145\/3776678"],"URL":"https:\/\/doi.org\/10.1145\/3776678","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,1,8]]},"assertion":[{"value":"2025-07-09","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-11-06","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2026-01-08","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}