{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,13]],"date-time":"2025-12-13T11:41:37Z","timestamp":1765626097828,"version":"3.48.0"},"reference-count":91,"publisher":"Association for Computing Machinery (ACM)","issue":"4","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Program. Lang. Syst."],"published-print":{"date-parts":[[2025,12,31]]},"abstract":"<jats:p>\n                    We extend intersection types to a computational\n                    <jats:inline-formula content-type=\"math\/tex\">\n                      <jats:tex-math notation=\"LaTeX\" version=\"MathJax\">\\(\\lambda\\)<\/jats:tex-math>\n                    <\/jats:inline-formula>\n                    -calculus with algebraic operations\n                    <jats:italic toggle=\"yes\">\u00e0 la<\/jats:italic>\n                    Plotkin and Power. We achieve this by considering monadic intersections\u2014whereby computational effects appear not only in the operational semantics but also in the\n                    <jats:italic toggle=\"yes\">type system<\/jats:italic>\n                    . Since in the effectful setting, termination is not anymore the only property of interest, we want to analyze the interactive behavior of typed programs with the environment. Indeed, our type system can characterize the natural notion of observation, both in the finitary and in the infinitary setting. In a second phase, we extend our system with subtyping to incorporate a richer class of effects via monads on preorders instead of sets allowing us to model in particular non-determinism. The main technical tool is a novel combination of syntactic techniques with abstract relational reasoning, which allows us to lift all the required notions, for example, of typability and logical relation, to the monadic setting.\n                  <\/jats:p>","DOI":"10.1145\/3777483","type":"journal-article","created":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T15:49:45Z","timestamp":1763480985000},"page":"1-51","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Monadic Intersection Types, Relationally, and Ordered"],"prefix":"10.1145","volume":"47","author":[{"ORCID":"https:\/\/orcid.org\/0009-0008-6402-3531","authenticated-orcid":false,"given":"Zeinab","family":"Galal","sequence":"first","affiliation":[{"name":"Kyoto University Research Institute for Mathematical Sciences, Kyoto, Japan"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2159-0615","authenticated-orcid":false,"given":"Francesco","family":"Gavazzo","sequence":"additional","affiliation":[{"name":"Universit\u00e0 degli Studi di Padova, Padova, Italy"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9731-1248","authenticated-orcid":false,"given":"Riccardo","family":"Treglia","sequence":"additional","affiliation":[{"name":"Universitas Mercatorum, Rome, Italy"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8762-8674","authenticated-orcid":false,"given":"Gabriele","family":"Vanoni","sequence":"additional","affiliation":[{"name":"IRIF, CNRS, Universit\u00e9 Paris Cit\u00e9, Paris, France"}]}],"member":"320","published-online":{"date-parts":[[2025,12,13]]},"reference":[{"key":"e_1_3_3_2_2","first-page":"1","volume-title":"Handbook of Logic in Computer Science","author":"Abramsky Samson","year":"1994","unstructured":"Samson Abramsky and Achim Jung. 1994. Domain theory. In Handbook of Logic in Computer Science. Samson Abramsky, Dov Gabbay, and T. S. E. Maibaum (Eds.), Clarendon Press, 1\u2013168."},{"key":"e_1_3_3_3_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2015.08.006"},{"key":"e_1_3_3_4_2","doi-asserted-by":"publisher","DOI":"10.1145\/3547650"},{"key":"e_1_3_3_5_2","doi-asserted-by":"publisher","DOI":"10.1017\/S095679682000012X"},{"key":"e_1_3_3_6_2","first-page":"410","volume-title":"Proceedings of the 28th European Symposium on Programming (ESOP \u201919)","author":"Accattoli Beniamino","year":"2019","unstructured":"Beniamino Accattoli, Giulio Guerrieri, and Maico Leberle. 2019. Types by need. In Proceedings of the 28th European Symposium on Programming (ESOP \u201919). Springer, 410\u2013439. DOI: 10.1007\/978-3-030-17184-1_15"},{"key":"e_1_3_3_7_2","first-page":"1","volume-title":"Proceedings of the 37th Annual ACM\/IEEE Symposium on Logic in Computer Science","author":"Ad\u00e1mek Jir\u00ed","year":"2022","unstructured":"Jir\u00ed Ad\u00e1mek. 2022. Varieties of quantitative algebras and their monads. In Proceedings of the 37th Annual ACM\/IEEE Symposium on Logic in Computer Science, 1\u201310."},{"issue":"4","key":"e_1_3_3_8_2","doi-asserted-by":"crossref","first-page":"349","DOI":"10.1017\/S0960129521000463","article-title":"A categorical view of varieties of ordered algebras","volume":"32","author":"Ad\u00e1mek Jir\u00ed","year":"2022","unstructured":"Jir\u00ed Ad\u00e1mek, Matej Dost\u00e1l, and Jir\u00ed Velebil. 2022. A categorical view of varieties of ordered algebras. Mathematical Structures in Computer Science 32, 4 (2022), 349\u2013373.","journal-title":"Mathematical Structures in Computer Science"},{"key":"e_1_3_3_9_2","doi-asserted-by":"crossref","unstructured":"Ji\u0159\u00ed Ad\u00e1mek Stefan Milius Lurdes Sousa and Thorsten Wi\u00dfmann. 2019. On finitary functors. arXiv:1902.05788. Retrieved from https:\/\/arxiv.org\/abs\/1902.05788","DOI":"10.70930\/tac\/vbwlg5ti"},{"key":"e_1_3_3_10_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-39784-4_4"},{"key":"e_1_3_3_11_2","first-page":"1","volume-title":"Proceedings of the 2019 34th Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS)","author":"Avanzini Martin","year":"2019","unstructured":"Martin Avanzini, Ugo Dal Lago, and Alexis Ghyselen. 2019. Type-Based complexity analysis of probabilistic functional programs. In Proceedings of the 2019 34th Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS), 1\u201313. DOI: 10.1109\/LICS.2019.8785725"},{"key":"e_1_3_3_12_2","doi-asserted-by":"crossref","first-page":"102338","DOI":"10.1016\/j.scico.2019.102338","article-title":"On probabilistic term rewriting","volume":"185","author":"Avanzini Martin","year":"2020","unstructured":"Martin Avanzini, Ugo Dal Lago, and Akihisa Yamada. 2020. On probabilistic term rewriting. Science of Computer Program 185 (2020), 102338.","journal-title":"Science of Computer Program"},{"key":"e_1_3_3_13_2","first-page":"303","volume-title":"Algebraic Methodology and Software Technology (AMAST \u201991), Proceedings of the Second International Conference on Methodology and Software Technology, Iowa City, USA, 22\u201325 May 1991 (Workshops in Computing)","author":"Backhouse Roland Carl","year":"1991","unstructured":"Roland Carl Backhouse, Peter J. de Bruin, Paul F. Hoogendijk, Grant Malcolm, Ed Voermans, and Jaap van der Woude. 1991. Polynomial relators (extended abstract). In Algebraic Methodology and Software Technology (AMAST \u201991), Proceedings of the Second International Conference on Methodology and Software Technology, Iowa City, USA, 22\u201325 May 1991 (Workshops in Computing). Maurice Nivat, Charles Rattray, Teodor Rus, and Giuseppe Scollo (Eds.), Springer, 303\u2013326."},{"key":"e_1_3_3_14_2","doi-asserted-by":"crossref","first-page":"39","DOI":"10.1007\/BFb0060439","article-title":"Relational algebras","volume":"137","author":"Barr Michael","year":"1970","unstructured":"Michael Barr. 1970. Relational algebras. Lecture Notes in Mathmatics 137 (1970), 39\u201355.","journal-title":"Lecture Notes in Mathmatics"},{"key":"e_1_3_3_15_2","doi-asserted-by":"crossref","first-page":"115","DOI":"10.1007\/978-3-642-22944-2_9","volume-title":"Algebra and Coalgebra in Computer Science: 4th International Conference, CALCO 2011, Winchester, UK, August 30\u2013September 2, 2011. Proceedings 4","author":"B\u00edlkov\u00e1 Marta","year":"2011","unstructured":"Marta B\u00edlkov\u00e1, Alexander Kurz, Daniela Petri\u015fan, and Ji\u0159\u00ed Velebil. 2011. Relation liftings on preorders and posets. In Algebra and Coalgebra in Computer Science: 4th International Conference, CALCO 2011, Winchester, UK, August 30\u2013September 2, 2011. Proceedings 4. Andrea Corradini, Bartek Klin, and Corina C\u00eerstea (Eds.), Springer, 115\u2013129."},{"key":"e_1_3_3_16_2","article-title":"Relation lifting, with an application to the many-valued cover modality","volume":"9","author":"Bilkova Marta","year":"2013","unstructured":"Marta Bilkova, Alexander Kurz, Daniela Petrisan, and Jiri Velebil. 2013. Relation lifting, with an application to the many-valued cover modality. Logical Methods in Computer Science 9 (2013).","journal-title":"Logical Methods in Computer Science"},{"key":"e_1_3_3_17_2","volume-title":"Algebra of Programming","author":"Bird Richard S.","year":"1997","unstructured":"Richard S. Bird and Oege de Moor. 1997. Algebra of Programming. Prentice Hall."},{"issue":"2","key":"e_1_3_3_18_2","doi-asserted-by":"crossref","first-page":"200","DOI":"10.1016\/S0022-0000(76)80030-X","article-title":"Varieties of ordered algebras","volume":"13","author":"Bloom Stephen L.","year":"1976","unstructured":"Stephen L. Bloom. 1976. Varieties of ordered algebras. Journal of Computer and System 13, 2 (1976), 200\u2013212.","journal-title":"Journal of Computer and System"},{"issue":"1","key":"e_1_3_3_19_2","doi-asserted-by":"crossref","first-page":"13","DOI":"10.1016\/0022-4049(83)90080-4","article-title":"P-varieties\u2014A signature independent characterization of varieties of ordered algebras","volume":"29","author":"Bloom Stephen L.","year":"1983","unstructured":"Stephen L. Bloom and Jesse B. Wright. 1983. P-varieties\u2014A signature independent characterization of varieties of ordered algebras. Journal of Pure and Applied Algebra 29, 1 (1983), 13\u201358.","journal-title":"Journal of Pure and Applied Algebra"},{"key":"e_1_3_3_20_2","doi-asserted-by":"crossref","first-page":"7","DOI":"10.1145\/3373718.3394733","volume-title":"Proceedings of the 35th Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS \u201920","author":"Bono Viviana","year":"2020","unstructured":"Viviana Bono and Mariangiola Dezani-Ciancaglini. 2020. A tale of intersection types. In Proceedings of the 35th Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS \u201920). Holger Hermanns, Lijun Zhang, Naoki Kobayashi, and Dale Miller (Eds.), ACM, 7\u201320. DOI: 10.1145\/3373718.3394733"},{"key":"e_1_3_3_21_2","first-page":"1","volume-title":"Proceedings of the 20th International Symposium on Principles and Practice of Declarative Programming (PPDP \u201918)","author":"Breuvart Flavien","year":"2018","unstructured":"Flavien Breuvart and Ugo Dal Lago. 2018. On intersection types and probabilistic lambda calculi. In Proceedings of the 20th International Symposium on Principles and Practice of Declarative Programming (PPDP \u201918). David Sabel and Peter Thiemann (Eds.), ACM, 1\u201313. DOI: 10.1145\/3236950.3236968"},{"key":"e_1_3_3_22_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0168-0072(00)00056-7"},{"issue":"1","key":"e_1_3_3_23_2","first-page":"47","article-title":"A 2-categorical approach to change of base and geometric morphisms I","volume":"32","author":"Carboni Aurelio","year":"1991","unstructured":"Aurelio Carboni, G. M. Kelly, and R. J. Wood. 1991. A 2-categorical approach to change of base and geometric morphisms I. Cahiers de Topologie et G\u00e9om\u00e9trie Diff\u00e9rentielle Cat\u00e9goriques 32, 1 (1991), 47\u201395.","journal-title":"Cahiers de Topologie et G\u00e9om\u00e9trie Diff\u00e9rentielle Cat\u00e9goriques"},{"issue":"1","key":"e_1_3_3_24_2","doi-asserted-by":"crossref","first-page":"175","DOI":"10.1007\/s40062-013-0063-2","article-title":"The monads of classical algebra are seldom weakly cartesian","volume":"9","author":"Clementino Maria Manuel","year":"2014","unstructured":"Maria Manuel Clementino, Dirk Hofmann, and George Janelidze. 2014. The monads of classical algebra are seldom weakly cartesian. Journal of Homotopy and Related Structures 9, 1 (2014), 175\u2013197.","journal-title":"Journal of Homotopy and Related Structures"},{"key":"e_1_3_3_25_2","first-page":"254","volume-title":"Proceedings of the 24th Italian Conference on Theoretical Computer Science","volume":"3587","author":"Sacerdoti Coen Claudio","year":"2023","unstructured":"Claudio Sacerdoti Coen and Riccardo Treglia. 2023. Properties of a computational lambda calculus for higher-order relational queries. In Proceedings of the 24th Italian Conference on Theoretical Computer Science. Giuseppa Castiglione and Marinella Sciortino (Eds.), Vol. 3587, CEUR-WS.org, 254\u2013267. Retrieved from https:\/\/ceur-ws.org\/Vol-3587\/8059.pdf"},{"key":"e_1_3_3_26_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF02011875"},{"key":"e_1_3_3_27_2","first-page":"241","volume-title":"Proceedings of the Colloquium (Logic Colloquium \u201982)","author":"Coppo Mario","year":"1984","unstructured":"Mario Coppo, Mariangiola Dezani-Ciancaglini, Furio Honsell, and Giuseppe Longo. 1984. Extended type structures and filter lambda models. In Proceedings of the Colloquium (Logic Colloquium \u201982). G. Lolli, G. Longo, and A. Marcja (Eds.), North-Holland, Amsterdam, The Netherlands, 241\u2013262."},{"key":"e_1_3_3_28_2","volume-title":"Proceedings of the ACM on Programming Languages","volume":"5","author":"Dal Lago Ugo","year":"2021","unstructured":"Ugo Dal Lago, Claudia Faggian, and Simona Ronchi Della Rocca. 2021. Intersection types and (positive) almost-sure termination. Proceedings of the ACM on Programming Languages 5, POPL, Article 32 (2021), 32 pages. DOI: 10.1145\/3434313"},{"key":"e_1_3_3_29_2","first-page":"1","volume-title":"Proceedings of the 32nd Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS \u201917)","author":"Dal Lago Ugo","year":"2017","unstructured":"Ugo Dal Lago, Francesco Gavazzo, and Paul Blain Levy. 2017. Effectful applicative bisimilarity: Monads, relators, and Howe\u2019s method. In Proceedings of the 32nd Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS \u201917), 1\u201312."},{"key":"e_1_3_3_30_2","first-page":"87","volume-title":"Proceedings of the 18th Italian Conference on Theoretical Computer Science and the 32nd Italian Conference on Computational Logic Co-located with the 2017 IEEE International Workshop on Measurements and Networking (IEEE M&N \u201917).andVol","volume":"1949","author":"Dal Lago Ugo","year":"2017","unstructured":"Ugo Dal Lago, Francesco Gavazzo, and Ryo Tanaka. 2017. Effectful applicative similarity for call-by-name lambda calculi. In Proceedings of the 18th Italian Conference on Theoretical Computer Science and the 32nd Italian Conference on Computational Logic Co-located with the 2017 IEEE International Workshop on Measurements and Networking (IEEE M&N \u201917). Dario Della Monica, Aniello Murano, Sasha Rubin, and Luigi Sauro (Eds.), Vol. 1949, CEUR-WS.org, 87\u201398. Retrieved from http:\/\/ceur-ws.org\/Vol-1949\/ICTCSpaper06.pdf"},{"key":"e_1_3_3_31_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2019.12.025"},{"key":"e_1_3_3_32_2","doi-asserted-by":"publisher","DOI":"10.1145\/3293605"},{"key":"e_1_3_3_33_2","first-page":"198","volume-title":"Proceedings of the 5th ACM SIGPLAN International Conference on Functional Programming (ICFP \u201900)","author":"Davies Rowan","year":"2000","unstructured":"Rowan Davies and Frank Pfenning. 2000. Intersection types and computational effects. In Proceedings of the 5th ACM SIGPLAN International Conference on Functional Programming (ICFP \u201900). ACM, 198\u2013208. DOI: 10.1145\/351240.351259"},{"key":"e_1_3_3_34_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129516000396"},{"key":"e_1_3_3_35_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2020.09.029"},{"key":"e_1_3_3_36_2","first-page":"1 11","volume-title":"Proceedings of the 23rd International Symposium on Principles and Practice of Declarative Programming (PPDP \u201921)","author":"de\u2019Liguoro Ugo","year":"2021","unstructured":"Ugo de\u2019Liguoro and Riccardo Treglia. 2021. 2021. Intersection types for a \\(\\lambda\\) -calculus with global store. In Proceedings of the 23rd International Symposium on Principles and Practice of Declarative Programming (PPDP \u201921). Niccol\u00f2 Veltri, Nick Benton, and Silvia Ghilezan (Eds.), ACM, 1\u201311. DOI: 10.1145\/3479394.3479400"},{"key":"e_1_3_3_37_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2023.114082"},{"key":"e_1_3_3_38_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-22348-9_6"},{"key":"e_1_3_3_39_2","unstructured":"Mariangiola Dezani-Ciancaglini and Simona Ronchi Della Rocca. 2007. Intersection and reference types. In Reflections on Type Theory Lambda Calculus and the Mind. E. Barendsen V. Capretta J. H. Geuvers and M. Niqui (Eds.) Radboud University Nijmegen 77\u201386. Retrieved from http:\/\/www.di.unito.it\/\u223cdezani\/papers\/dr.pdf"},{"key":"e_1_3_3_40_2","first-page":"259","volume-title":"Proceedings of the 26th International Workshop\/21st Annual Conference of the EACSL\u2014Computer Science Logic (CSL \u201912)Vol","volume":"16","author":"Ehrhard Thomas","year":"2012","unstructured":"Thomas Ehrhard. 2012. Collapsing non-idempotent intersection types. In Proceedings of the 26th International Workshop\/21st Annual Conference of the EACSL\u2014Computer Science Logic (CSL \u201912). Patrick C\u00e9gielski and Arnaud Durand (Eds.), Vol. 16, Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 259\u2013273. DOI: 10.4230\/LIPIcs.CSL.2012.259"},{"key":"e_1_3_3_41_2","doi-asserted-by":"crossref","first-page":"309","DOI":"10.1145\/2535838.2535865","volume-title":". In Proceedings of the 41th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL \u201914)","author":"Ehrhard Thomas","year":"2014","unstructured":"Thomas Ehrhard, Michele Pagani, and Christine Tasson. 2014. Probabilistic coherence spaces are fully abstract for probabilistic PCF. In Proceedings of the 41th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL \u201914). Peter Sewell (Ed.), ACM, 309\u2013320."},{"key":"e_1_3_3_42_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129522000433"},{"key":"e_1_3_3_43_2","doi-asserted-by":"crossref","first-page":"268","DOI":"10.1145\/113445.113468","volume-title":"Proceedings of the ACM SIGPLAN 1991 Conference on Programming Language Design and Implementation (PLDI \u201991)","author":"Freeman Timothy S.","year":"1991","unstructured":"Timothy S. Freeman and Frank Pfenning. 1991. Refinement types for ML. In Proceedings of the ACM SIGPLAN 1991 Conference on Programming Language Design and Implementation (PLDI \u201991). David S. Wise (Ed.), ACM, 268\u2013277. DOI: 10.1145\/113445.113468"},{"key":"e_1_3_3_44_2","doi-asserted-by":"publisher","DOI":"10.1145\/1391289.1391293"},{"key":"e_1_3_3_45_2","doi-asserted-by":"crossref","first-page":"107081","DOI":"10.1016\/j.aim.2020.107081","article-title":"Stochastic order on metric spaces and the ordered Kantorovich monad","volume":"366","author":"Fritz Tobias","year":"2020","unstructured":"Tobias Fritz and Paolo Perrone. 2020. Stochastic order on metric spaces and the ordered Kantorovich monad. Advances in Mathematics 366 (2020), 107081.","journal-title":"Advances in Mathematics"},{"issue":"3","key":"e_1_3_3_46_2","doi-asserted-by":"crossref","first-page":"117","DOI":"10.1007\/BF01988052","article-title":"The validity of equations of complex algebras","volume":"3","author":"Gautam N. D.","year":"1957","unstructured":"N. D. Gautam. 1957. The validity of equations of complex algebras. Archiv F\u00fcr Mathematische Logik Und Grundlagenforschung 3, 3 (1957), 117\u2013124.","journal-title":"Archiv F\u00fcr Mathematische Logik Und Grundlagenforschung"},{"key":"e_1_3_3_47_2","first-page":"1","volume-title":"Proceedings of the 36th Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS \u201921)","author":"Gavazzo Francesco","year":"2021","unstructured":"Francesco Gavazzo and Claudia Faggian. 2021. A relational theory of monadic rewriting systems, part I. In Proceedings of the 36th Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS \u201921). IEEE, 1\u201314. DOI: 10.1109\/LICS52264.2021.9470633"},{"key":"e_1_3_3_48_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-57262-3_2"},{"key":"e_1_3_3_49_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90045-4"},{"issue":"2","key":"e_1_3_3_50_2","first-page":"103","article-title":"Relations et carr\u00e9s exacts","volume":"4","author":"Guitart Ren\u00e9","year":"1980","unstructured":"Ren\u00e9 Guitart. 1980. Relations et carr\u00e9s exacts. Annales math\u00e9matiques du Qu\u00e9bec 4, 2 (1980), 103\u2013125.","journal-title":"Annales math\u00e9matiques du Qu\u00e9bec"},{"issue":"1","key":"e_1_3_3_51_2","first-page":"113","article-title":"A cottage industry of lax extensions","volume":"3","author":"Hoffman Dirk","year":"2015","unstructured":"Dirk Hoffman and Gavin J. Seal. 2015. A cottage industry of lax extensions. Categories and General Algebraic Structures with Applications 3, 1 (2015), 113\u2013151.","journal-title":"Categories and General Algebraic Structures with Applications"},{"key":"e_1_3_3_52_2","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781107517288","volume-title":"Monoidal Topology: A Categorical Approach to Order, Metric and Topology","author":"Hofmann D.","year":"2014","unstructured":"D. Hofmann, G. J. Seal, and W. Tholen. 2014. Monoidal Topology: A Categorical Approach to Order, Metric and Topology. Cambridge University Press."},{"issue":"1","key":"e_1_3_3_53_2","doi-asserted-by":"crossref","first-page":"71","DOI":"10.1016\/j.tcs.2004.07.022","article-title":"Simulations in coalgebra","volume":"327","author":"Hughes Jesse","year":"2004","unstructured":"Jesse Hughes and Bart Jacobs. 2004. Simulations in coalgebra. Theoretical Computer Science 327, 1\u20132 (2004), 71\u2013108.","journal-title":"Theoretical Computer Science"},{"key":"e_1_3_3_54_2","first-page":"186","volume-title":"Proceedings of the 4th Annual Symposium on Logic in Computer Science","author":"Jones Claire","year":"1989","unstructured":"Claire Jones and Gordon D. Plotkin. 1989. A probabilistic powerdomain of evaluations. In Proceedings of the 4th Annual Symposium on Logic in Computer Science. IEEE Computer Society, 186\u2013187."},{"issue":"2","key":"e_1_3_3_55_2","doi-asserted-by":"crossref","first-page":"275","DOI":"10.2206\/kyushumfs.27.275","article-title":"Notes on the universality of relational functors","volume":"27","author":"Kawahara Yasuo","year":"1973","unstructured":"Yasuo Kawahara. 1973. Notes on the universality of relational functors. Memoirs of the Faculty of Science, Kyushu University. Series A, Mathematics 27, 2 (1973), 275\u2013289.","journal-title":"Memoirs of the Faculty of Science, Kyushu University. Series A, Mathematics"},{"key":"e_1_3_3_56_2","first-page":"1","article-title":"Basic concepts of enriched category theory","volume":"10","author":"Kelly Gregory M.","year":"2005","unstructured":"Gregory M. Kelly. 2005. Basic concepts of enriched category theory. Reprints in Theory and Applications of Categories 10 (2005), 1\u2013136.","journal-title":"Reprints in Theory and Applications of Categories"},{"issue":"1","key":"e_1_3_3_57_2","doi-asserted-by":"crossref","first-page":"163","DOI":"10.1016\/0022-4049(93)90092-8","article-title":"Adjunctions whose counits are coequalizers, and presentations of finitary enriched monads","volume":"89","author":"Kelly G. Maxwell","year":"1993","unstructured":"G. Maxwell Kelly and A. John Power. 1993. Adjunctions whose counits are coequalizers, and presentations of finitary enriched monads. Journal of Pure and Applied Algebra 89, 1\u20132 (1993), 163\u2013179.","journal-title":"Journal of Pure and Applied Algebra"},{"key":"e_1_3_3_58_2","volume-title":"Proceedings of the 7th International Workshop on Trends in Linear Logic and Applications","author":"Kesner Delia","year":"2023","unstructured":"Delia Kesner, Miguel Ramos, and Riccardo Treglia. 2023. A quantitative understanding of exceptions. In Proceedings of the 7th International Workshop on Trends in Linear Logic and Applications."},{"key":"e_1_3_3_59_2","doi-asserted-by":"publisher","DOI":"10.23638\/LMCS-16(1:3)2020"},{"key":"e_1_3_3_60_2","first-page":"416","volume-title":"Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL \u201909)","author":"Kobayashi Naoki","year":"2009","unstructured":"Naoki Kobayashi. 2009. Types and higher-order recursion schemes for verification of higher-order programs. In Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL \u201909). Zhong Shao and Benjamin C. Pierce (Eds.), ACM, 416\u2013428. DOI: 10.1145\/1480881.1480933"},{"issue":"4","key":"e_1_3_3_61_2","first-page":"2:1","article-title":"On the termination problem for probabilistic higher-order recursive programs","volume":"16","author":"Kobayashi Naoki","year":"2020","unstructured":"Naoki Kobayashi, Ugo Dal Lago, and Charles Grellois. 2020. On the termination problem for probabilistic higher-order recursive programs. Logical Methods in Computer Science 16, 4 (2020), 2:1\u20132:57.","journal-title":"Logical Methods in Computer Science"},{"key":"e_1_3_3_62_2","first-page":"179","volume-title":"Proceedings of the 24th Annual IEEE Symposium on Logic in Computer Science (LICS \u201909)","author":"Kobayashi Naoki","year":"2009","unstructured":"Naoki Kobayashi and C.-H. Luke Ong. 2009. A type system equivalent to the modal mu-calculus model checking of higher-order recursion schemes. In Proceedings of the 24th Annual IEEE Symposium on Logic in Computer Science (LICS \u201909). IEEE Computer Society, 179\u2013188. DOI: 10.1109\/LICS.2009.29"},{"key":"e_1_3_3_63_2","volume-title":"Lambda-Calculus, Types and Models","author":"Krivine Jean-Louis","year":"1993","unstructured":"Jean-Louis Krivine. 1993. Lambda-Calculus, Types and Models. Masson."},{"issue":"7","key":"e_1_3_3_64_2","doi-asserted-by":"crossref","first-page":"1153","DOI":"10.1017\/S096012951500050X","article-title":"Quasivarieties and varieties of ordered algebras: Regularity and exactness","volume":"27","author":"Kurz Alexander","year":"2017","unstructured":"Alexander Kurz and Ji\u0159\u00ed Velebil. 2017. Quasivarieties and varieties of ordered algebras: Regularity and exactness. Mathematical Structures in Computer Science 27, 7 (2017), 1153\u20131194.","journal-title":"Mathematical Structures in Computer Science"},{"key":"e_1_3_3_65_2","doi-asserted-by":"crossref","first-page":"736","DOI":"10.70930\/tac\/5bdk760i","article-title":"Lax distributive laws for topology, II","volume":"32","author":"Lai Hongliang","year":"2017","unstructured":"Hongliang Lai, Lili Shen, and Walter Tholen. 2017. Lax distributive laws for topology, II. Theory and Applications of Categories 32 (2017), 736\u2013768.","journal-title":"Theory and Applications of Categories"},{"key":"e_1_3_3_66_2","volume-title":"Categories for the Working Mathematician","author":"MacLane Saunders","year":"1971","unstructured":"Saunders MacLane. 1971. Categories for the Working Mathematician. Springer-Verlag."},{"key":"e_1_3_3_67_2","doi-asserted-by":"crossref","first-page":"700","DOI":"10.1145\/2933575.2934518","volume-title":"Proceedings of the 31st Annual ACM\/IEEE Symposium on Logic in Computer Science","author":"Mardare Radu","year":"2016","unstructured":"Radu Mardare, Prakash Panangaden, and Gordon Plotkin. 2016. Quantitative algebraic reasoning. In Proceedings of the 31st Annual ACM\/IEEE Symposium on Logic in Computer Science, 700\u2013709."},{"key":"e_1_3_3_68_2","first-page":"14","volume-title":"Proceedings of the 4th Annual Symposium on Logic in Computer Science (LICS \u201989)","author":"Moggi Eugenio","year":"1989","unstructured":"Eugenio Moggi. 1989. Computational Lambda-Calculus and monads. In Proceedings of the 4th Annual Symposium on Logic in Computer Science (LICS \u201989). IEEE Computer Society, 14\u201323. DOI: 10.1109\/LICS.1989.39155"},{"key":"e_1_3_3_69_2","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90052-4"},{"key":"e_1_3_3_70_2","first-page":"81","volume-title":"Proceedings of the 21th IEEE Symposium on Logic in Computer Science (LICS \u201906)","author":"Ong C.-H. Luke","year":"2006","unstructured":"C.-H. Luke Ong. 2006. On model-checking trees generated by higher-order recursion schemes. In Proceedings of the 21th IEEE Symposium on Logic in Computer Science (LICS \u201906). IEEE Computer Society, 81\u201390. DOI: 10.1109\/LICS.2006.38"},{"key":"e_1_3_3_71_2","doi-asserted-by":"publisher","unstructured":"Benjamin C. Pierce. 1997. Intersection types and bounded polymorphism. Mathematical Structures in Computer Science 7 2 (1997) 129\u2013193. DOI: 10.1017\/S096012959600223X","DOI":"10.1017\/S096012959600223X"},{"key":"e_1_3_3_72_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(75)90017-1"},{"key":"e_1_3_3_73_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45315-6_1"},{"key":"e_1_3_3_74_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45931-6_24"},{"key":"e_1_3_3_75_2","doi-asserted-by":"publisher","DOI":"10.1023\/A:1023064908962"},{"key":"e_1_3_3_76_2","first-page":"275","volume-title":"Higher Order Operational Techniques in Semantics","author":"Sands David","year":"1998","unstructured":"David Sands. 1998. Improvement theory and its applications. In Higher Order Operational Techniques in Semantics. Andrew D. Gordon and Andrew M. Pitts (Eds.), Cambridge University Press, 275\u2013306."},{"key":"e_1_3_3_77_2","volume-title":"A Course in Universal Algebra. Graduate Texts Math","author":"Sankappanavar Hanamantagouda P.","year":"1981","unstructured":"Hanamantagouda P. Sankappanavar and Stanley Burris. 1981. A Course in Universal Algebra. Graduate Texts Math. Vol. 78. Springer."},{"key":"e_1_3_3_78_2","volume-title":"Relational Mathematics. Encyclopedia of Mathematics and Its Applications","author":"Schmidt Gunther","year":"2011","unstructured":"Gunther Schmidt. 2011. Relational Mathematics. Encyclopedia of Mathematics and Its Applications, Vol. 132. Cambridge University Press."},{"key":"e_1_3_3_79_2","doi-asserted-by":"publisher","DOI":"10.1145\/3363518"},{"key":"e_1_3_3_80_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF02413910"},{"key":"e_1_3_3_81_2","doi-asserted-by":"crossref","first-page":"25","DOI":"10.1016\/j.fss.2016.04.013","article-title":"The double power monad is the composite power monad","volume":"313","author":"Stubbe Isar","year":"2017","unstructured":"Isar Stubbe. 2017. The double power monad is the composite power monad. Fuzzy Sets and Systems 313 (2017), 25\u201342.","journal-title":"Fuzzy Sets and Systems"},{"key":"e_1_3_3_82_2","first-page":"347","volume-title":"Proceedings of the Workshop on Membrane Computing","author":"Syropoulos Apostolos","year":"2000","unstructured":"Apostolos Syropoulos. 2000. Mathematics of multisets. In Proceedings of the Workshop on Membrane Computing. Springer, 347\u2013358."},{"key":"e_1_3_3_83_2","volume-title":"Simulation and Fixpoint Semantics","author":"Thijs Albert M.","year":"1996","unstructured":"Albert M. Thijs. 1996. Simulation and Fixpoint Semantics. Rijksuniversiteit Groningen."},{"key":"e_1_3_3_84_2","first-page":"180","volume-title":"Foundations of Software Science and Computation Structures\u201417th International Conference, FOSSACS 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5\u201313, 2014, Proceedings","volume":"8412","author":"Tsukada Takeshi","year":"2014","unstructured":"Takeshi Tsukada and Naoki Kobayashi. 2014. Complexity of model-checking call-by-value programs. In Foundations of Software Science and Computation Structures\u201417th International Conference, FOSSACS 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5\u201313, 2014, Proceedings. Anca Muscholl (Ed.), Lecture Notes in Computer Science, Vol. 8412, Springer, 180\u2013194. DOI: 10.1007\/978-3-642-54830-7_12"},{"key":"e_1_3_3_85_2","doi-asserted-by":"publisher","DOI":"10.23638\/LMCS-14(1:2)2018"},{"key":"e_1_3_3_86_2","unstructured":"Daniele Varacca. 2003. Probability Nondeterminism and Concurrency: Two Denotational Models for Probabilistic Computation. Ph.D. Dissertation. Aarhus University."},{"issue":"1","key":"e_1_3_3_87_2","doi-asserted-by":"crossref","first-page":"87","DOI":"10.1017\/S0960129505005074","article-title":"Distributing probability over non-determinism","volume":"16","author":"Varacca Daniele","year":"2006","unstructured":"Daniele Varacca and Glynn Winskel. 2006. Distributing probability over non-determinism. Mathematical Structures in Computer Science 16, 1 (2006), 87\u2013113.","journal-title":"Mathematical Structures in Computer Science"},{"key":"e_1_3_3_88_2","first-page":"1","volume-title":"Proceedings of the 32nd Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS \u201917)","author":"Vial Pierre","year":"2017","unstructured":"Pierre Vial. 2017. Infinitary intersection types as sequences: A new answer to Klop\u2019s problem. In Proceedings of the 32nd Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS \u201917). IEEE Computer Society, 1\u201312."},{"key":"e_1_3_3_89_2","doi-asserted-by":"crossref","first-page":"899","DOI":"10.1145\/3209108.3209133","volume-title":"Proceedings of the 33rd Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS \u201918)","author":"Vial Pierre","year":"2018","unstructured":"Pierre Vial. 2018. Every \\(\\lambda\\) -term is meaningful for the infinitary relational model. In Proceedings of the 33rd Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS \u201918). Anuj Dawar and Erich Gr\u00e4del (Eds.), ACM, 899\u2013908. DOI: 10.1145\/3209108.3209133."},{"key":"e_1_3_3_90_2","first-page":"24","volume-title":"Advanced Functional Programming, First International Spring School on Advanced Functional Programming Techniques. Lecture Notes in Computer Science","volume":"925","author":"Wadler P.","year":"1995","unstructured":"P. Wadler. 1995. Monads for functional programming. In Advanced Functional Programming, First International Spring School on Advanced Functional Programming Techniques. Lecture Notes in Computer Science. Johan Jeuring and Erik Meijer (Eds.), Vol. 925, Springer, 24\u201352. DOI: 10.1007\/3-540-59451-5_2"},{"issue":"14","key":"e_1_3_3_91_2","doi-asserted-by":"crossref","first-page":"191","DOI":"10.70930\/tac\/p68r8xve","article-title":"Generic morphisms, parametric representations and weakly cartesian monads","volume":"13","author":"Weber Mark","year":"2004","unstructured":"Mark Weber. 2004. Generic morphisms, parametric representations and weakly cartesian monads. Theory and Applications of Categories 13, 14 (2004), 191\u2013234.","journal-title":"Theory and Applications of Categories"},{"key":"e_1_3_3_92_2","doi-asserted-by":"crossref","first-page":"337","DOI":"10.1016\/S1571-0661(05)80356-1","article-title":"Coinduction for recursive data types: Partial orders, metric spaces and","volume":"33","author":"Worrell James","year":"2000","unstructured":"James Worrell. 2000. Coinduction for recursive data types: Partial orders, metric spaces and \\(\\Omega\\) -categories. Electronic Notes in Theoretical Computer Science 33 (2000), 337\u2013356.","journal-title":"Electronic Notes in Theoretical Computer Science"}],"container-title":["ACM Transactions on Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3777483","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,12,13]],"date-time":"2025-12-13T11:39:50Z","timestamp":1765625990000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3777483"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,12,13]]},"references-count":91,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2025,12,31]]}},"alternative-id":["10.1145\/3777483"],"URL":"https:\/\/doi.org\/10.1145\/3777483","relation":{},"ISSN":["0164-0925","1558-4593"],"issn-type":[{"type":"print","value":"0164-0925"},{"type":"electronic","value":"1558-4593"}],"subject":[],"published":{"date-parts":[[2025,12,13]]},"assertion":[{"value":"2024-04-27","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-10-06","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-12-13","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}