{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:34:28Z","timestamp":1767929668124,"version":"3.49.0"},"reference-count":71,"publisher":"Association for Computing Machinery (ACM)","issue":"ICFP","license":[{"start":{"date-parts":[[2023,8,30]],"date-time":"2023-08-30T00:00:00Z","timestamp":1693353600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["EP\/S028129\/1"],"award-info":[{"award-number":["EP\/S028129\/1"]}],"id":[{"id":"10.13039\/501100000266","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":[[2023,8,30]]},"abstract":"<jats:p>Inspired by algebraic effects and the principle of notions of computations as monoids, we study a categorical framework for equational theories and models of monoids equipped with operations.  \nThe framework covers not only algebraic operations but also scoped and variable-binding operations.  \nAppealingly, in this framework both theories and models can be modularly composed.  \nTechnically, a general monoid-theory correspondence is shown, saying that the category of theories of algebraic operations is equivalent to the category of monoids.  \nMoreover, more complex forms of operations can be coreflected into algebraic operations, in a way that preserves initial algebras.  \nOn models, we introduce modular models of a theory, which can interpret  \nabstract syntax in the presence of other operations.   \nWe show constructions of modular models (i) from monoid transformers, (ii) from free algebras, (iii) by composition, and (iv) in symmetric monoidal categories.<\/jats:p>","DOI":"10.1145\/3607850","type":"journal-article","created":{"date-parts":[[2023,8,31]],"date-time":"2023-08-31T17:40:31Z","timestamp":1693503631000},"page":"566-603","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":6,"title":["Modular Models of Monoids with Operations"],"prefix":"10.1145","volume":"7","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-5573-3357","authenticated-orcid":false,"given":"Zhixuan","family":"Yang","sequence":"first","affiliation":[{"name":"Imperial College London, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4161-985X","authenticated-orcid":false,"given":"Nicolas","family":"Wu","sequence":"additional","affiliation":[{"name":"Imperial College London, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2023,8,31]]},"reference":[{"key":"e_1_2_1_1_1","first-page":"589","article-title":"Free Algebras and Automata Realizations in the Language of Categories","volume":"015","author":"Ad\u00e1mek Ji\u0159\u00ed","year":"1974","unstructured":"Ji\u0159\u00ed Ad\u00e1mek. 1974. Free Algebras and Automata Realizations in the Language of Categories. Commentationes Mathematicae Universitatis Carolinae, 015, 4 (1974), 589\u2013602. http:\/\/eudml.org\/doc\/16649","journal-title":"Commentationes Mathematicae Universitatis Carolinae"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511600579"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1017\/S095679680900728X"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571255"},{"key":"e_1_2_1_5_1","volume-title":"Proceedings of the Conference on Category Theory and Computer Science. https:\/\/doi.org\/10","author":"Cenciarelli Pietro","year":"1993","unstructured":"Pietro Cenciarelli and Eugenio Moggi. 1993. A Syntactic Approach to Modularity in Denotational Semantics. In Proceedings of the Conference on Category Theory and Computer Science. https:\/\/doi.org\/10.1.1.41.7807"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","unstructured":"Paul M. Cohn. 1981. Universal Algebra. Springer Dordrecht. https:\/\/doi.org\/10.1007\/978-94-009-8399-1 10.1007\/978-94-009-8399-1","DOI":"10.1007\/978-94-009-8399-1"},{"key":"e_1_2_1_7_1","volume-title":"Reports of the Midwest Category Seminar IV","author":"Day Brian","unstructured":"Brian Day. 1970. On Closed Categories of Functors. In Reports of the Midwest Category Seminar IV, S. MacLane, H. Applegate, M. Barr, B. Day, E. Dubuc, Phreilambud, A. Pultr, R. Street, M. Tierney, and S. Swierczkowski (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 1\u201338. isbn:978-3-540-36292-0"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/174675.178047"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/292540.292557"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2008.38"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73420-8_53"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2008.12.052"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","unstructured":"Marcelo Fiore and Ola Mahmoud. 2014. Functorial Semantics of Second-Order Algebraic Theories. https:\/\/doi.org\/10.48550\/ARXIV.1401.4697","DOI":"10.48550\/ARXIV.1401.4697"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1999.782615"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.FSCD.2017.16"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/2603088.2603163"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498715"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796807006314"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1051\/ita:2004016"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","unstructured":"Neil Ghani Tarmo Uustalu and Makoto Hamana. 2006. Explicit Substitutions and Higher-Order Syntax. Higher-Order and Symbolic Computation https:\/\/doi.org\/10.1007\/s10990-006-8748-4 10.1007\/s10990-006-8748-4","DOI":"10.1007\/s10990-006-8748-4"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-16912-0_1"},{"key":"e_1_2_1_22_1","unstructured":"Andy Gill and Edward Kmett. 2012. mtl: Monad classes using functional dependencies. https:\/\/hackage.haskell.org\/package\/mtl"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/165180.165214"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1006\/aima.1999.1877"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31113-0_16"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(86)90059-1"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0167-6423(99)00023-4"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129515000377"},{"key":"e_1_2_1_29_1","volume-title":"Categorical Logic and Type Theory (Studies in Logic and the Foundations of Mathematics). North Holland","author":"Jacobs Bart","unstructured":"Bart Jacobs. 1999. Categorical Logic and Type Theory (Studies in Logic and the Foundations of Mathematics). North Holland, Amsterdam."},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796809007308"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2010.09.011"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535846"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3547654"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-4049(93)90092-8"},{"key":"e_1_2_1_35_1","first-page":"3","article-title":"Structures defined by finite limits in the enriched context","volume":"23","author":"Kelly G. M.","year":"1982","unstructured":"G. M. Kelly. 1982. Structures defined by finite limits in the enriched context, I. Cahiers de Topologie et G\u00e9om\u00e9trie Diff\u00e9rentielle Cat\u00e9goriques, 23, 1 (1982), 3\u201342.","journal-title":"I. Cahiers de Topologie et G\u00e9om\u00e9trie Diff\u00e9rentielle Cat\u00e9goriques"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3473577"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/2887747.2804319"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01304852"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-45231-5_21"},{"key":"e_1_2_1_40_1","unstructured":"J. Lambek and P. J. Scott. 1986. Introduction to Higher Order Categorical Logic. Cambridge University Press. isbn:978-0-521-35653-4"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1073\/pnas.50.5.869"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/199448.199528"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-99902-4_3"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","unstructured":"Fosco Loregian. 2021. (Co)end Calculus. Cambridge University Press. https:\/\/doi.org\/10.1017\/9781108778657 10.1017\/9781108778657","DOI":"10.1017\/9781108778657"},{"key":"e_1_2_1_45_1","volume-title":"Categories for the Working Mathematician","author":"Lane Saunders Mac","unstructured":"Saunders Mac Lane. 1998. Categories for the Working Mathematician, 2nd edn. Springer, Berlin.","edition":"2"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796807006326"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-16912-0_4"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.360.6"},{"key":"e_1_2_1_49_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_1_50_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1989.39155"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90052-4"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236774"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31113-0_15"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796820000106"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209166"},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(04)80970-8"},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45931-6_24"},{"key":"e_1_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1023064908962"},{"key":"e_1_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2004.08.008"},{"key":"e_1_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.2168\/lmcs-9(4:23)2013"},{"key":"e_1_2_1_61_1","first-page":"83","article-title":"Enriched Lawvere Theories","volume":"6","author":"Power John","year":"1999","unstructured":"John Power. 1999. Enriched Lawvere Theories. Theory and Applications of Categories, 6, 7 (1999), 83\u201393.","journal-title":"Theory and Applications of Categories"},{"key":"e_1_2_1_62_1","volume-title":"Abstraction and Parametric Polymorphism. In IFIP Congress.","author":"Reynolds John C.","year":"1983","unstructured":"John C. Reynolds. 1983. Types, Abstraction and Parametric Polymorphism. In IFIP Congress."},{"key":"e_1_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796817000132"},{"key":"e_1_2_1_64_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2007.09.024"},{"key":"e_1_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796808006758"},{"key":"e_1_2_1_66_1","volume-title":"Semantics of programming languages. 1","author":"Tennent Robert D","unstructured":"Robert D Tennent. 1991. Semantics of programming languages. 1, Prentice Hall New York."},{"key":"e_1_2_1_67_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70594-9_20"},{"key":"e_1_2_1_68_1","doi-asserted-by":"publisher","DOI":"10.5555\/647698.734146"},{"key":"e_1_2_1_69_1","doi-asserted-by":"publisher","DOI":"10.1145\/2633357.2633358"},{"key":"e_1_2_1_70_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99336-8_17"},{"key":"e_1_2_1_71_1","doi-asserted-by":"publisher","DOI":"10.1145\/3473578"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3607850","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3607850","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:37:06Z","timestamp":1750178226000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3607850"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,8,30]]},"references-count":71,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2023,8,30]]}},"alternative-id":["10.1145\/3607850"],"URL":"https:\/\/doi.org\/10.1145\/3607850","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,8,30]]},"assertion":[{"value":"2023-08-31","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}