{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T21:05:47Z","timestamp":1763499947004,"version":"3.40.3"},"publisher-location":"Cham","reference-count":71,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031572616"},{"type":"electronic","value":"9783031572623"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,4,5]],"date-time":"2024-04-05T00:00:00Z","timestamp":1712275200000},"content-version":"vor","delay-in-days":95,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We extend intersection types to a computational <jats:inline-formula><jats:alternatives><jats:tex-math>$$\\lambda $$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi>\u03bb<\/mml:mi>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula>-calculus with algebraic operations <jats:italic>\u00e0 la<\/jats:italic> Plotkin and Power. We achieve this by considering monadic intersections\u2014whereby computational effects appear not only in the operational semantics, but also in the <jats:italic>type system<\/jats:italic>. 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 is able to characterize the natural notion of observation, both in the finite and in the infinitary setting, and for a wide class of effects, such as output, cost, pure and probabilistic nondeterminism, and combinations thereof. The main technical tool is a novel combination of syntactic techniques with abstract relational reasoning, which allows us to lift all the required notions, e.g. of typability and logical relation, to the monadic setting.<\/jats:p>","DOI":"10.1007\/978-3-031-57262-3_2","type":"book-chapter","created":{"date-parts":[[2024,4,4]],"date-time":"2024-04-04T07:02:35Z","timestamp":1712214155000},"page":"22-51","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Monadic Intersection Types, Relationally"],"prefix":"10.1007","author":[{"given":"Francesco","family":"Gavazzo","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Riccardo","family":"Treglia","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gabriele","family":"Vanoni","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,4,5]]},"reference":[{"key":"2_CR1","doi-asserted-by":"crossref","unstructured":"Abramsky, S., Jung, A.: Domain theory. In: Handbook of Logic in Computer Science. pp. 1\u2013168. Clarendon Press (1994)","DOI":"10.1093\/oso\/9780198537625.003.0001"},{"key":"2_CR2","doi-asserted-by":"publisher","unstructured":"Accattoli, B.: Proof nets and the call-by-value $$\\lambda $$-calculus. Theor. Comput. Sci. 606, 2\u201324 (2015). https:\/\/doi.org\/10.1016\/j.tcs.2015.08.006, https:\/\/doi.org\/10.1016\/j.tcs.2015.08.006","DOI":"10.1016\/j.tcs.2015.08.006 10.1016\/j.tcs.2015.08.006"},{"key":"2_CR3","doi-asserted-by":"publisher","unstructured":"Accattoli, B., Dal\u00a0Lago, U., Vanoni, G.: Multi types and reasonable space. Proc. ACM Program. Lang. 6(ICFP), 799\u2013825 (2022). https:\/\/doi.org\/10.1145\/3547650","DOI":"10.1145\/3547650"},{"key":"2_CR4","doi-asserted-by":"publisher","unstructured":"Accattoli, B., Graham-Lengrand, S., Kesner, D.: Tight typings and split bounds, fully developed. J. Funct. Program. 30, \u00a0e14 (2020). https:\/\/doi.org\/10.1017\/S095679682000012X","DOI":"10.1017\/S095679682000012X"},{"key":"2_CR5","doi-asserted-by":"publisher","unstructured":"Alves, S., Kesner, D., Ramos, M.: Quantitative global memory. In: Hansen, H.H., Scedrov, A., de\u00a0Queiroz, R.J.G.B. (eds.) Logic, Language, Information, and Computation - 29th International Workshop, WoLLIC 2023, Halifax, NS, Canada, July 11-14, 2023, Proceedings. Lecture Notes in Computer Science, vol. 13923, pp. 53\u201368. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-39784-4_4","DOI":"10.1007\/978-3-031-39784-4_4"},{"key":"2_CR6","doi-asserted-by":"publisher","unstructured":"Avanzini, M., Dal\u00a0Lago, U., Ghyselen, A.: Type-based complexity analysis of probabilistic functional programs. In: 2019 34th Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS). pp. 1\u201313 (2019). https:\/\/doi.org\/10.1109\/LICS.2019.8785725","DOI":"10.1109\/LICS.2019.8785725"},{"key":"2_CR7","doi-asserted-by":"crossref","unstructured":"Avanzini, M., Dal\u00a0Lago, U., Yamada, A.: On probabilistic term rewriting. Sci. Comput. Program. 185 (2020)","DOI":"10.1016\/j.scico.2019.102338"},{"key":"2_CR8","unstructured":"Backhouse, R.C., de\u00a0Bruin, P.J., Hoogendijk, P.F., Malcolm, G., Voermans, E., van\u00a0der Woude, J.: Polynomial relators (extended abstract). In: Nivat, M., Rattray, C., Rus, T., Scollo, G. (eds.) Algebraic Methodology and Software Technology (AMAST \u201991), Proceedings of the Second International Conference on Methodology and Software Technology, Iowa City, USA, 22-25 May 1991. pp. 303\u2013326. Workshops in Computing, Springer (1991)"},{"key":"2_CR9","doi-asserted-by":"publisher","unstructured":"van Bakel, S., Barbanera, F., de\u2019Liguoro, U.: Intersection types for the lambda-mu calculus. Log. Methods Comput. Sci. 14(1) (2018). https:\/\/doi.org\/10.23638\/LMCS-14(1:2)2018, https:\/\/doi.org\/10.23638\/LMCS-14(1:2)2018","DOI":"10.23638\/LMCS-14(1:2)2018 10.23638\/LMCS-14(1:2)2018"},{"key":"2_CR10","doi-asserted-by":"crossref","unstructured":"Barr, M.: Relational algebras. Lect. Notes Math. 137, 39\u201355 (1970)","DOI":"10.1007\/BFb0060439"},{"key":"2_CR11","unstructured":"Bird, R.S., de\u00a0Moor, O.: Algebra of programming. Prentice Hall International series in computer science, Prentice Hall (1997)"},{"key":"2_CR12","doi-asserted-by":"publisher","unstructured":"Bono, V., Dezani-Ciancaglini, M.: A tale of intersection types. In: Hermanns, H., Zhang, L., Kobayashi, N., Miller, D. (eds.) LICS \u201920: 35th Annual ACM\/IEEE Symposium on Logic in Computer Science, Saarbr\u00fccken, Germany, July 8-11, 2020. pp. 7\u201320. ACM (2020). https:\/\/doi.org\/10.1145\/3373718.3394733, https:\/\/doi.org\/10.1145\/3373718.3394733","DOI":"10.1145\/3373718.3394733 10.1145\/3373718.3394733"},{"key":"2_CR13","doi-asserted-by":"publisher","unstructured":"Breuvart, F., Dal\u00a0Lago, U.: On intersection types and probabilistic lambda calculi. In: Sabel, D., Thiemann, P. (eds.) Proceedings of the 20th International Symposium on Principles and Practice of Declarative Programming, PPDP 2018, Frankfurt am Main, Germany, September 03-05, 2018. pp. 8:1\u20138:13. ACM (2018). https:\/\/doi.org\/10.1145\/3236950.3236968, https:\/\/doi.org\/10.1145\/3236950.3236968","DOI":"10.1145\/3236950.3236968 10.1145\/3236950.3236968"},{"key":"2_CR14","unstructured":"Carboni, A., Kelly, G.M., Wood, R.J.: 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), 47\u201395 (1991)"},{"key":"2_CR15","doi-asserted-by":"crossref","unstructured":"Clementino, M.M., Hofmann, D., Janelidze, G.: The monads of classical algebra are seldom weakly cartesian. Journal of Homotopy and Related Structures 9(1), 175\u2013197 (2014)","DOI":"10.1007\/s40062-013-0063-2"},{"key":"2_CR16","doi-asserted-by":"publisher","unstructured":"Coppo, M., Dezani-Ciancaglini, M.: A new type assignment for $$\\lambda $$-terms. Arch. Math. Log. 19(1), 139\u2013156 (1978). https:\/\/doi.org\/10.1007\/BF02011875","DOI":"10.1007\/BF02011875"},{"key":"2_CR17","doi-asserted-by":"crossref","unstructured":"Coppo, M., Dezani-Ciancaglini, M., Honsell, F., Longo, G.: Extended type structures and filter lambda models. In: Lolli, G., Longo, G., Marcja, A. (eds.) Logic Colloquium 82. pp. 241\u2013262. North-Holland, Amsterdam, the Netherlands (1984)","DOI":"10.1016\/S0049-237X(08)71819-6"},{"key":"2_CR18","doi-asserted-by":"publisher","unstructured":"Dal\u00a0Lago, U., Faggian, C., Ronchi Della\u00a0Rocca, S.: Intersection types and (positive) almost-sure termination. Proc. ACM Program. Lang. 5(POPL), 1\u201332 (2021). https:\/\/doi.org\/10.1145\/3434313","DOI":"10.1145\/3434313"},{"key":"2_CR19","doi-asserted-by":"crossref","unstructured":"Dal\u00a0Lago, U., Gavazzo, F., Levy, P.B.: Effectful applicative bisimilarity: Monads, relators, and howe\u2019s method. In: Proc. of LICS 2017. pp. 1\u201312 (2017)","DOI":"10.1109\/LICS.2017.8005117"},{"key":"2_CR20","unstructured":"Dal\u00a0Lago, U., Gavazzo, F., Tanaka, R.: Effectful applicative similarity for call-by-name lambda calculi. In: Monica, D.D., Murano, A., Rubin, S., Sauro, L. (eds.) Joint 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 (2017 IEEE M &N), Naples, Italy, September 26-28, 2017. CEUR Workshop Proceedings, vol.\u00a01949, pp. 87\u201398. CEUR-WS.org (2017), http:\/\/ceur-ws.org\/Vol-1949\/ICTCSpaper06.pdf"},{"key":"2_CR21","doi-asserted-by":"publisher","unstructured":"Dal\u00a0Lago, U., Gavazzo, F., Tanaka, R.: Effectful applicative similarity for call-by-name lambda calculi. Theor. Comput. Sci. 813, 234\u2013247 (2020). https:\/\/doi.org\/10.1016\/j.tcs.2019.12.025, https:\/\/doi.org\/10.1016\/j.tcs.2019.12.025","DOI":"10.1016\/j.tcs.2019.12.025 10.1016\/j.tcs.2019.12.025"},{"key":"2_CR22","doi-asserted-by":"publisher","unstructured":"Dal\u00a0Lago, U., Grellois, C.: Probabilistic termination by monadic affine sized typing. ACM Trans. Program. Lang. Syst. 41(2), 10:1\u201310:65 (2019). https:\/\/doi.org\/10.1145\/3293605, https:\/\/doi.org\/10.1145\/3293605","DOI":"10.1145\/3293605 10.1145\/3293605"},{"key":"2_CR23","doi-asserted-by":"publisher","unstructured":"Davies, R., Pfenning, F.: Intersection types and computational effects. In: Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming (ICFP \u201900). pp. 198\u2013208. ACM (2000). https:\/\/doi.org\/10.1145\/351240.351259","DOI":"10.1145\/351240.351259"},{"key":"2_CR24","doi-asserted-by":"publisher","unstructured":"de Carvalho, D.: Execution time of $$\\lambda $$-terms via denotational semantics and intersection types. Math. Str. in Comput. Sci. 28(7), 1169\u20131203 (2018). https:\/\/doi.org\/10.1017\/S0960129516000396","DOI":"10.1017\/S0960129516000396"},{"key":"2_CR25","doi-asserted-by":"publisher","unstructured":"de\u2019Liguoro, U., Treglia, R.: The untyped computational $$\\lambda $$-calculus and its intersection type discipline. Theor. Comput. Sci. 846, 141\u2013159 (2020). https:\/\/doi.org\/10.1016\/j.tcs.2020.09.029, https:\/\/doi.org\/10.1016\/j.tcs.2020.09.029","DOI":"10.1016\/j.tcs.2020.09.029 10.1016\/j.tcs.2020.09.029"},{"key":"2_CR26","doi-asserted-by":"publisher","unstructured":"de\u2019Liguoro, U., Treglia, R.: Intersection types for a $$\\lambda $$-calculus with global store. In: Veltri, N., Benton, N., Ghilezan, S. (eds.) PPDP 2021: 23rd International Symposium on Principles and Practice of Declarative Programming, Tallinn, Estonia, September 6-8, 2021. pp. 5:1\u20135:11. ACM (2021). https:\/\/doi.org\/10.1145\/3479394.3479400, https:\/\/doi.org\/10.1145\/3479394.3479400","DOI":"10.1145\/3479394.3479400 10.1145\/3479394.3479400"},{"key":"2_CR27","doi-asserted-by":"publisher","unstructured":"de\u2019Liguoro, U., Treglia, R.: From semantics to types: The case of the imperative $$\\lambda $$-calculus. vol.\u00a0973, p. 114082 (2023). https:\/\/doi.org\/10.1016\/j.tcs.2023.114082, https:\/\/doi.org\/10.1016\/j.tcs.2023.114082","DOI":"10.1016\/j.tcs.2023.114082 10.1016\/j.tcs.2023.114082"},{"key":"2_CR28","doi-asserted-by":"publisher","unstructured":"Dezani-Ciancaglini, M., Giannini, P., Venneri, B.: Intersection types in java: Back to the future. In: Margaria, T., Graf, S., Larsen, K.G. (eds.) Models, Mindsets, Meta: The What, the How, and the Why Not? - Essays Dedicated to Bernhard Steffen on the Occasion of His 60th Birthday. Lecture Notes in Computer Science, vol. 11200, pp. 68\u201386. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-030-22348-9_6, https:\/\/doi.org\/10.1007\/978-3-030-22348-9_6","DOI":"10.1007\/978-3-030-22348-9_6 10.1007\/978-3-030-22348-9_6"},{"key":"2_CR29","unstructured":"Dezani-Ciancaglini, M., Ronchi Della\u00a0Rocca, S.: Intersection and Reference Types. In: Reflections on Type Theory, Lambda Calculus, and the Mind. pp. 77\u201386. Radboud University Nijmegen (2007), http:\/\/www.di.unito.it\/~dezani\/papers\/dr.pdf"},{"key":"2_CR30","doi-asserted-by":"publisher","unstructured":"Ehrhard, T.: Collapsing non-idempotent intersection types. In: C\u00e9gielski, P., Durand, A. (eds.) Computer Science Logic (CSL\u201912) - 26th International Workshop\/21st Annual Conference of the EACSL, CSL 2012, September 3-6, 2012, Fontainebleau, France. LIPIcs, vol.\u00a016, pp. 259\u2013273. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2012). https:\/\/doi.org\/10.4230\/LIPIcs.CSL.2012.259, https:\/\/doi.org\/10.4230\/LIPIcs.CSL.2012.259","DOI":"10.4230\/LIPIcs.CSL.2012.259 10.4230\/LIPIcs.CSL.2012.259"},{"key":"2_CR31","doi-asserted-by":"crossref","unstructured":"Ehrhard, T., Pagani, M., Tasson, C.: Probabilistic Coherence Spaces are Fully Abstract for Probabilistic PCF. In: Sewell, P. (ed.) The 41th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL14, San Diego, USA. ACM (2014)","DOI":"10.1145\/2535838.2535865"},{"key":"2_CR32","doi-asserted-by":"publisher","unstructured":"Faggian, C., Guerrieri, G., de\u2019Liguoro, U., Treglia, R.: On reduction and normalization in the computational core. Mathematical Structures in Computer Science p. 1-48 (2023). https:\/\/doi.org\/10.1017\/S0960129522000433","DOI":"10.1017\/S0960129522000433"},{"key":"2_CR33","doi-asserted-by":"publisher","unstructured":"Freeman, T.S., Pfenning, F.: Refinement types for ML. In: Wise, D.S. (ed.) Proceedings of the ACM SIGPLAN\u201991 Conference on Programming Language Design and Implementation (PLDI), Toronto, Ontario, Canada, June 26-28, 1991. pp. 268\u2013277. ACM (1991). https:\/\/doi.org\/10.1145\/113445.113468, https:\/\/doi.org\/10.1145\/113445.113468","DOI":"10.1145\/113445.113468 10.1145\/113445.113468"},{"key":"2_CR34","doi-asserted-by":"publisher","unstructured":"Frisch, A., Castagna, G., Benzaken, V.: Semantic subtyping: Dealing set-theoretically with function, union, intersection, and negation types. J. ACM 55(4), 19:1\u201319:64 (2008). https:\/\/doi.org\/10.1145\/1391289.1391293, https:\/\/doi.org\/10.1145\/1391289.1391293","DOI":"10.1145\/1391289.1391293 10.1145\/1391289.1391293"},{"key":"2_CR35","doi-asserted-by":"crossref","unstructured":"Gautam, N.D.: The validity of equations of complex algebras. Archiv f\u00fcr mathematische Logik und Grundlagenforschung 3(3), 117\u2013124 (1957)","DOI":"10.1007\/BF01988052"},{"key":"2_CR36","doi-asserted-by":"publisher","unstructured":"Gavazzo, F., Faggian, C.: A relational theory of monadic rewriting systems, part I. In: 36th Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2021, Rome, Italy, June 29 - July 2, 2021. pp. 1\u201314. IEEE (2021). https:\/\/doi.org\/10.1109\/LICS52264.2021.9470633, https:\/\/doi.org\/10.1109\/LICS52264.2021.9470633","DOI":"10.1109\/LICS52264.2021.9470633 10.1109\/LICS52264.2021.9470633"},{"key":"2_CR37","unstructured":"Gavazzo, F., Treglia, R., Vanoni, G.: Monadic intersection types, relationally (extended version) (2024), https:\/\/arxiv.org\/abs\/2401.12744"},{"key":"2_CR38","doi-asserted-by":"publisher","unstructured":"Girard, J.Y.: Linear logic. Theoretical Computer Science 50(1), 1\u2013101 (1987). https:\/\/doi.org\/10.1016\/0304-3975(87)90045-4","DOI":"10.1016\/0304-3975(87)90045-4"},{"key":"2_CR39","unstructured":"Hoffman, D., Seal, G.J.: A cottage industry of lax extensions. Categories and General Algebraic Structures with Applications 3(1), 113\u2013151 (2015)"},{"key":"2_CR40","doi-asserted-by":"crossref","unstructured":"Hofmann, D., Seal, G., Tholen, W.: Monoidal Topology: A Categorical Approach to Order, Metric and Topology. Encyclopedia of Mathematics and its Applications, Cambridge University Press (2014)","DOI":"10.1017\/CBO9781107517288"},{"key":"2_CR41","doi-asserted-by":"crossref","unstructured":"Hughes, J., Jacobs, B.: Simulations in coalgebra. Theor. Comput. Sci. 327(1-2), 71\u2013108 (2004)","DOI":"10.1016\/j.tcs.2004.07.022"},{"key":"2_CR42","doi-asserted-by":"crossref","unstructured":"Kawahara, Y.: Notes on the universality of relational functors. Memoirs of the Faculty of Science, Kyushu University. Series A, Mathematics 27(2), 275\u2013289 (1973)","DOI":"10.2206\/kyushumfs.27.275"},{"key":"2_CR43","unstructured":"Kelly, G.M.: Basic concepts of enriched category theory. Reprints in Theory and Applications of Categories (10), 1\u2013136 (2005)"},{"key":"2_CR44","unstructured":"Kesner, D., Ramos, M., Treglia, R.: A quantitative understanding of exceptions (2023), presented at TLLA 2023"},{"key":"2_CR45","doi-asserted-by":"publisher","unstructured":"Kesner, D., Vial, P.: Non-idempotent types for classical calculi in natural deduction style. Log. Methods Comput. Sci. 16(1) (2020). https:\/\/doi.org\/10.23638\/LMCS-16(1:3)2020, https:\/\/doi.org\/10.23638\/LMCS-16(1:3)2020","DOI":"10.23638\/LMCS-16(1:3)2020 10.23638\/LMCS-16(1:3)2020"},{"key":"2_CR46","doi-asserted-by":"publisher","unstructured":"Kobayashi, N.: Types and higher-order recursion schemes for verification of higher-order programs. In: Shao, Z., Pierce, B.C. (eds.) Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2009, Savannah, GA, USA, January 21-23, 2009. pp. 416\u2013428. ACM (2009). https:\/\/doi.org\/10.1145\/1480881.1480933","DOI":"10.1145\/1480881.1480933"},{"key":"2_CR47","doi-asserted-by":"crossref","unstructured":"Kobayashi, N., Dal\u00a0Lago, U., Grellois, C.: On the termination problem for probabilistic higher-order recursive programs. Log. Methods Comput. Sci. 16(4) (2020)","DOI":"10.1109\/LICS.2019.8785679"},{"key":"2_CR48","doi-asserted-by":"publisher","unstructured":"Kobayashi, N., Ong, C.L.: 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 2009, 11-14 August 2009, Los Angeles, CA, USA. pp. 179\u2013188. IEEE Computer Society (2009). https:\/\/doi.org\/10.1109\/LICS.2009.29","DOI":"10.1109\/LICS.2009.29"},{"key":"2_CR49","doi-asserted-by":"crossref","unstructured":"MacLane, S.: Categories for the Working Mathematician. Springer-Verlag (1971)","DOI":"10.1007\/978-1-4612-9839-7"},{"key":"2_CR50","doi-asserted-by":"publisher","unstructured":"Moggi, E.: Computational lambda-calculus and monads. In: Proceedings of the Fourth Annual Symposium on Logic in Computer Science (LICS \u201989). pp. 14\u201323. IEEE Computer Society (1989). https:\/\/doi.org\/10.1109\/LICS.1989.39155","DOI":"10.1109\/LICS.1989.39155"},{"key":"2_CR51","doi-asserted-by":"crossref","unstructured":"Moggi, E.: Notions of computation and monads. Inf. Comput. 93(1), 55\u201392 (1991). 10.1016\/0890-5401(91)90052-4","DOI":"10.1016\/0890-5401(91)90052-4"},{"key":"2_CR52","doi-asserted-by":"publisher","unstructured":"Ong, C.L.: On model-checking trees generated by higher-order recursion schemes. In: 21th IEEE Symposium on Logic in Computer Science (LICS 2006), 12-15 August 2006, Seattle, WA, USA, Proceedings. pp. 81\u201390. IEEE Computer Society (2006). https:\/\/doi.org\/10.1109\/LICS.2006.38","DOI":"10.1109\/LICS.2006.38"},{"key":"2_CR53","doi-asserted-by":"publisher","unstructured":"Pierce, B.C.: Intersection types and bounded polymorphism. Math. Struct. Comput. Sci. 7(2), 129\u2013193 (1997). https:\/\/doi.org\/10.1017\/S096012959600223X","DOI":"10.1017\/S096012959600223X"},{"key":"2_CR54","doi-asserted-by":"crossref","unstructured":"Plotkin, G., Power, J.: Adequacy for algebraic effects. In: Honsell, F., Miculan, M. (eds.) Foundations of Software Science and Computation Structures. pp. 1\u201324. Springer Berlin Heidelberg, Berlin, Heidelberg (2001)","DOI":"10.1007\/3-540-45315-6_1"},{"key":"2_CR55","doi-asserted-by":"publisher","unstructured":"Plotkin, G.D.: Call-by-name, call-by-value and the lambda-calculus. Theor. Comput. Sci. 1(2), 125\u2013159 (1975). https:\/\/doi.org\/10.1016\/0304-3975(75)90017-1","DOI":"10.1016\/0304-3975(75)90017-1"},{"key":"2_CR56","doi-asserted-by":"publisher","unstructured":"Plotkin, G.D., Power, J.: Adequacy for algebraic effects. In: Honsell, F., Miculan, M. (eds.) Foundations of Software Science and Computation Structures, 4th International Conference, FOSSACS 2001 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2001 Genova, Italy, April 2-6, 2001, Proceedings. Lecture Notes in Computer Science, vol.\u00a02030, pp. 1\u201324. Springer (2001). https:\/\/doi.org\/10.1007\/3-540-45315-6_1, https:\/\/doi.org\/10.1007\/3-540-45315-6_1","DOI":"10.1007\/3-540-45315-6_1 10.1007\/3-540-45315-6_1"},{"key":"2_CR57","doi-asserted-by":"publisher","unstructured":"Plotkin, G.D., Power, J.: Notions of computation determine monads. In: FOSSACS 2002. Lecture Notes in Computer Science, vol.\u00a02303, pp. 342\u2013356. Springer (2002). https:\/\/doi.org\/10.1007\/3-540-45931-6_24, https:\/\/doi.org\/10.1007\/3-540-45931-6_24","DOI":"10.1007\/3-540-45931-6_24 10.1007\/3-540-45931-6_24"},{"key":"2_CR58","doi-asserted-by":"publisher","unstructured":"Plotkin, G.D., Power, J.: Algebraic operations and generic effects. Appl. Categorical Struct. 11(1), 69\u201394 (2003). https:\/\/doi.org\/10.1023\/A:1023064908962","DOI":"10.1023\/A:1023064908962"},{"key":"2_CR59","unstructured":"Sands, D.: Improvement theory and its applications. In: Gordon, A.D., Pitts, A.M. (eds.) Higher Order Operational Techniques in Semantics, pp. 275\u2013306. Publications of the Newton Institute, Cambridge University Press (1998)"},{"key":"2_CR60","unstructured":"Sankappanavar, H.P., Burris, S.: A course in universal algebra. Graduate Texts Math 78 (1981)"},{"key":"2_CR61","unstructured":"Schmidt, G.: Relational Mathematics, Encyclopedia of Mathematics and its Applications, vol.\u00a0132. Cambridge University Press (2011)"},{"key":"2_CR62","doi-asserted-by":"publisher","unstructured":"Simpson, A., Voorneveld, N.F.W.: Behavioural equivalence via modalities for algebraic effects. ACM Trans. Program. Lang. Syst. 42(1), 4:1\u20134:45 (2020). https:\/\/doi.org\/10.1145\/3363518, https:\/\/doi.org\/10.1145\/3363518","DOI":"10.1145\/3363518 10.1145\/3363518"},{"key":"2_CR63","doi-asserted-by":"publisher","unstructured":"Stone, M.H.: Postulates for the barycentric calculus. Ann. Mat. Pura Appl. (4) 29(1), 25\u201330 (1949). https:\/\/doi.org\/10.1007\/BF02413910","DOI":"10.1007\/BF02413910"},{"key":"2_CR64","doi-asserted-by":"crossref","unstructured":"Syropoulos, A.: Mathematics of multisets. In: Workshop on Membrane Computing. pp. 347\u2013358. Springer (2000)","DOI":"10.1007\/3-540-45523-X_17"},{"key":"2_CR65","doi-asserted-by":"publisher","unstructured":"Tsukada, T., Kobayashi, N.: Complexity of model-checking call-by-value programs. In: Muscholl, A. (ed.) Foundations of Software Science and Computation Structures - 17th International Conference, FOSSACS 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014, Proceedings. Lecture Notes in Computer Science, vol.\u00a08412, pp. 180\u2013194. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-642-54830-7_12","DOI":"10.1007\/978-3-642-54830-7_12"},{"key":"2_CR66","unstructured":"Varacca, D.: Probability, nondeterminism and concurrency: two denotational models for probabilistic computation. Ph.D. thesis, Aarhus University (2003)"},{"key":"2_CR67","doi-asserted-by":"crossref","unstructured":"Varacca, D., Winskel, G.: Distributing probability over non-determinism. Math. Struct. Comput. Sci. 16(1), 87\u2013113 (2006)","DOI":"10.1017\/S0960129505005074"},{"key":"2_CR68","doi-asserted-by":"crossref","unstructured":"Vial, P.: Infinitary intersection types as sequences: A new answer to klop\u2019s problem. In: LICS. pp. 1\u201312. IEEE Computer Society (2017)","DOI":"10.1109\/LICS.2017.8005103"},{"key":"2_CR69","doi-asserted-by":"publisher","unstructured":"Vial, P.: Every $$\\lambda $$-term is meaningful for the infinitary relational model. In: Dawar, A., Gr\u00e4del, E. (eds.) Proceedings of the 33rd Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, 2018. pp. 899\u2013908. ACM (2018). https:\/\/doi.org\/10.1145\/3209108.3209133","DOI":"10.1145\/3209108.3209133"},{"key":"2_CR70","doi-asserted-by":"publisher","unstructured":"Wadler, P.: Monads for functional programming. In: Advanced Functional Programming, First International Spring School on Advanced Functional Programming Techniques. Lecture Notes in Computer Science, vol.\u00a0925, pp. 24\u201352. Springer (1995). https:\/\/doi.org\/10.1007\/3-540-59451-5_2","DOI":"10.1007\/3-540-59451-5_2"},{"key":"2_CR71","unstructured":"Weber, M.: Generic morphisms, parametric representations and weakly cartesian monads. Theory Appl. Categ 13(14), 191\u2013234 (2004)"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-57262-3_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,4,4]],"date-time":"2024-04-04T07:02:55Z","timestamp":1712214175000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-57262-3_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031572616","9783031572623"],"references-count":71,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-57262-3_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"5 April 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ESOP","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"European Symposium on Programming","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg City","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 April 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 April 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"33","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"esop2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2024\/conferences\/esop\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"72","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"25","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"1","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"35% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3.2","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"8","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"The proceedings also contain 4 artifact report that have not been part of the original submission","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}