{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,26]],"date-time":"2026-09-26T19:38:58Z","timestamp":1790451538043,"version":"4.1.0"},"reference-count":60,"publisher":"Association for Computing Machinery (ACM)","issue":"ICFP","license":[{"start":{"date-parts":[[2026,8,17]],"date-time":"2026-08-17T00:00:00Z","timestamp":1786924800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/legalcode"}],"funder":[{"name":"JSPS","award":["JP24H00699"],"award-info":[{"award-number":["JP24H00699"]}]},{"name":"JST","award":["JPMJCR21M3"],"award-info":[{"award-number":["JPMJCR21M3"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2026,8,17]]},"abstract":"<jats:p>\n                    We introduce a novel intersection type system for a\n                    <jats:italic toggle=\"yes\">\u03bb<\/jats:italic>\n                    -calculus with algebraic effects and handlers. The system, inherently behavioral in nature, enjoys the classical properties of intersection type systems, in particular subject reduction and\n                    <jats:italic toggle=\"yes\">expansion<\/jats:italic>\n                    . It thus characterizes the set of terms whose evaluation process terminates and, at the same time, allows reducing the reachability problem to type inference. This new system, the first with these features for a calculus with handlers, induces a system of simple types which, although not guaranteeing termination, is type sound and admits a decidable HOMC problem, unlike similar type systems like Dal Lago and Ghyselen's\n                    <jats:monospace>HEPCF<\/jats:monospace>\n                    .\n                  <\/jats:p>","DOI":"10.1145\/3828707","type":"journal-article","created":{"date-parts":[[2026,8,17]],"date-time":"2026-08-17T20:23:46Z","timestamp":1786998226000},"page":"1013-1041","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["When Types Intersect and Effects Get Handled"],"prefix":"10.1145","volume":"10","author":[{"ORCID":"https:\/\/orcid.org\/0009-0007-0829-5789","authenticated-orcid":false,"given":"Stefano","family":"Catozi","sequence":"first","affiliation":[{"name":"University Sorbonne Paris Nord, Villetaneuse, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9200-070X","authenticated-orcid":false,"given":"Ugo","family":"Dal Lago","sequence":"additional","affiliation":[{"name":"University of Bologna, Bologna, Italy"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9286-230X","authenticated-orcid":false,"given":"Taro","family":"Sekiyama","sequence":"additional","affiliation":[{"name":"National Institute of Informatics, Tokyo, Japan"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2026,8,17]]},"reference":[{"key":"e_1_3_1_2_2","doi-asserted-by":"publisher","DOI":"10.1145\/3434332"},{"key":"e_1_3_1_3_2","doi-asserted-by":"publisher","unstructured":"Sandra Alves Delia Kesner and Miguel Ramos. 2023. Quantitative Global Memory. In Logic Language Information and Computation. 53\u201368. doi:10.1007\/978-3-031-39784-4_4","DOI":"10.1007\/978-3-031-39784-4_4"},{"key":"e_1_3_1_4_2","doi-asserted-by":"publisher","DOI":"10.2307\/2273659"},{"key":"e_1_3_1_5_2","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-10(4:9)2014"},{"key":"e_1_3_1_6_2","doi-asserted-by":"publisher","unstructured":"Alexis Bernadet and St\u00e9phane Lengrand. 2011. Filter Models: Non-idempotent Intersection Types Orthogonality and Polymorphism. In Computer Science Logic - 25th International Workshop CSL 2011 (LIPIcs Vol. 12). 51\u201366. doi:10.4230\/LIPICS.CSL.2011.51","DOI":"10.4230\/LIPICS.CSL.2011.51"},{"key":"e_1_3_1_7_2","doi-asserted-by":"publisher","unstructured":"Gavin Bierman Mart\u00edn Abadi and Mads Torgersen. 2014. Understanding typescript. In European Conference on Object-Oriented Programming. Springer 257\u2013281. doi:10.1007\/978-3-662-44202-9_11","DOI":"10.1007\/978-3-662-44202-9_11"},{"key":"e_1_3_1_8_2","doi-asserted-by":"publisher","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. 7\u201320. doi:10.1145\/3373718.3394733","DOI":"10.1145\/3373718.3394733"},{"key":"e_1_3_1_9_2","doi-asserted-by":"publisher","DOI":"10.1145\/286936.286957"},{"key":"e_1_3_1_10_2","doi-asserted-by":"publisher","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. 1\u201313. doi:10.1145\/3236950.3236968","DOI":"10.1145\/3236950.3236968"},{"key":"e_1_3_1_11_2","doi-asserted-by":"crossref","unstructured":"Stefano Catozi Ugo Dal Lago and Taro Sekiyama. 2026. When Types Intersect and Effects Get Handled. arXiv:2606.09526 https:\/\/arxiv.org\/abs\/2606.09526","DOI":"10.1145\/3828707"},{"key":"e_1_3_1_12_2","doi-asserted-by":"publisher","DOI":"10.1145\/3158127"},{"key":"e_1_3_1_13_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF02011875"},{"key":"e_1_3_1_14_2","doi-asserted-by":"publisher","DOI":"10.1145\/3434313"},{"key":"e_1_3_1_15_2","doi-asserted-by":"publisher","DOI":"10.1145\/3632929"},{"key":"e_1_3_1_16_2","volume-title":"S\u00e9mantiques de la logique lin\u00e9aire et temps de calcul","author":"Carvalho Daniel De","year":"2007","unstructured":"Daniel De Carvalho. 2007. S\u00e9mantiques de la logique lin\u00e9aire et temps de calcul. Ph. D. Dissertation. Aix-Marseille 2."},{"key":"e_1_3_1_17_2","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1995.1145"},{"key":"e_1_3_1_18_2","doi-asserted-by":"publisher","unstructured":"Andrej Dudenhefner and Daniele Pautasso. 2024. Mechanized Subject Expansion in Uniform Intersection Types for Perpetual Reductions. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). 8\u20131. doi:10.4230\/LIPIcs.FSCD.2024.8","DOI":"10.4230\/LIPIcs.FSCD.2024.8"},{"key":"e_1_3_1_19_2","doi-asserted-by":"publisher","unstructured":"Ryunosuke Endo and Tachio Terauchi. 2025. Reachability is Decidable for ATM-Typable Finitary PCF with Effect Handlers. In Programming Languages and Systems APLAS (Lecture Notes in Computer Science Vol. 16201). 67\u201387. doi:10.1007\/978-981-95-3585-9_4","DOI":"10.1007\/978-981-95-3585-9_4"},{"key":"e_1_3_1_20_2","doi-asserted-by":"publisher","DOI":"10.1145\/3777483"},{"key":"e_1_3_1_21_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-57262-3_2"},{"key":"e_1_3_1_22_2","volume-title":"Th\u00e8se de Doctorat d'\u00c9tat","author":"Girard J. Y.","year":"1972","unstructured":"J. Y. Girard. 1972. Interpr\u00e9tation fonctionnelle et \u00e9limination des coupures de l'arithm\u00e9tique d'ordre sup\u00e9rieur. Th\u00e8se de Doctorat d'\u00c9tat. Universit\u00e9 Paris 7."},{"key":"e_1_3_1_23_2","doi-asserted-by":"publisher","unstructured":"Colin S. Gordon. 2020. Lifting Sequential Effects to Control Operators. In 34th European Conference on Object-Oriented Programming ECOOP 2020 (LIPIcs Vol. 166). 23:1\u201323:30. doi:10.4230\/LIPIcs.ECOOP.2020.23","DOI":"10.4230\/LIPIcs.ECOOP.2020.23"},{"key":"e_1_3_1_24_2","doi-asserted-by":"publisher","DOI":"10.1145\/3450272"},{"key":"e_1_3_1_25_2","doi-asserted-by":"publisher","unstructured":"Charles Grellois and Paul-Andr\u00e9 Melli\u00e8s. 2015. Relational Semantics of Linear Logic and Higher-order Model Checking. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015) (Leibniz International Proceedings in Informatics (LIPIcs) Vol. 41). 260\u2013276. doi:10.4230\/LIPIcs.CSL.2015.260","DOI":"10.4230\/LIPIcs.CSL.2015.260"},{"key":"e_1_3_1_26_2","doi-asserted-by":"publisher","unstructured":"Daniel Hillerstr\u00f6m and Sam Lindley. 2016. Liberating effects with rows and handlers. In Proceedings of the 1st International Workshop on Type-Driven Development TyDe@ICFP 2016. 15\u201327. doi:10.1145\/2976022.2976033","DOI":"10.1145\/2976022.2976033"},{"key":"e_1_3_1_27_2","doi-asserted-by":"publisher","unstructured":"Oleg Kiselyov and Hiromi Ishii. 2015. Freer monads more extensible effects. In Proceedings of the 8th ACM SIGPLAN Symposium on Haskell Haskell 2015. 94\u2013105. doi:10.1145\/2804302.2804319","DOI":"10.1145\/2804302.2804319"},{"key":"e_1_3_1_28_2","doi-asserted-by":"publisher","unstructured":"Teodor Knapik Damian Niwinski and Pawel Urzyczyn. 2001. Deciding Monadic Theories of Hyperalgebraic Trees. In Typed Lambda Calculi and Applications TLCA 2001 (Lecture Notes in Computer Science Vol. 2044). 253\u2013267. doi:10.1007\/3-540-45413-6_21","DOI":"10.1007\/3-540-45413-6_21"},{"key":"e_1_3_1_29_2","doi-asserted-by":"publisher","unstructured":"Teodor Knapik Damian Niwinski and Pawel Urzyczyn. 2002. Higher-Order Pushdown Trees Are Easy. In Foundations of Software Science and Computation Structures 5th International Conference FOSSACS 2002 (Lecture Notes in Computer Science Vol. 2303). 205\u2013222. doi:10.1007\/3-540-45931-6_15","DOI":"10.1007\/3-540-45931-6_15"},{"key":"e_1_3_1_30_2","doi-asserted-by":"publisher","unstructured":"Naoki Kobayashi. 2009. Types and higher-order recursion schemes for verification of higher-order programs. In Proceedings of the 36th annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 416\u2013428. doi:10.1145\/1594834.1480933","DOI":"10.1145\/1594834.1480933"},{"key":"e_1_3_1_31_2","doi-asserted-by":"publisher","DOI":"10.1145\/2487241.2487246"},{"key":"e_1_3_1_32_2","doi-asserted-by":"publisher","unstructured":"Naoki Kobayashi Ugo Dal Lago and Charles Grellois. 2019. On the Termination Problem for Probabilistic Higher-Order Recursive Programs. In 34th Annual ACM\/IEEE Symposium on Logic in Computer Science LICS 2019. 1\u201314. doi:10.1109\/LICS.2019.8785679","DOI":"10.1109\/LICS.2019.8785679"},{"key":"e_1_3_1_33_2","doi-asserted-by":"publisher","unstructured":"Naoki Kobayashi and Atsushi Igarashi. 2013. Model-Checking Higher-Order Programs with Recursive Types. In Programming Languages and Systems ESOP 2013 (Lecture Notes in Computer Science Vol. 7792). 431\u2013450. doi:10.1007\/978-3-642-37036-6_24","DOI":"10.1007\/978-3-642-37036-6_24"},{"key":"e_1_3_1_34_2","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2009.29"},{"key":"e_1_3_1_35_2","doi-asserted-by":"publisher","unstructured":"Eric Koskinen and Tachio Terauchi. 2014. Local Temporal Reasoning. In Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic and the Twenty-Ninth Annual ACM\/IEEE Symposium on Logic in Computer Science (CSL-LICS '14). 59:1\u201359: doi:10.1145\/2603088.2603138","DOI":"10.1145\/2603088.2603138"},{"key":"e_1_3_1_36_2","doi-asserted-by":"crossref","unstructured":"Daan Leijen. 2017. Type directed compilation of row-typed algebraic effects. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages POPL 2017. 486\u2013499. http:\/\/dl.acm.org\/citation.cfm?id=3009872","DOI":"10.1145\/3009837.3009872"},{"key":"e_1_3_1_37_2","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90052-4"},{"key":"e_1_3_1_38_2","doi-asserted-by":"publisher","unstructured":"Yoji Nanjo Hiroshi Unno Eric Koskinen and Tachio Terauchi. 2018. A Fixpoint Logic and Dependent Effects for Temporal Property Verification. In Proceedings of the 33rd Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS '18). 759\u2013768. doi:10.1145\/3209108.3209204","DOI":"10.1145\/3209108.3209204"},{"key":"e_1_3_1_39_2","unstructured":"Martin Odersky Philippe Altherr Vincent Cremet Burak Emir Sebastian Maneth St\u00e9phane Micheloud Nikolay Mihaylov Michel Schinz Erik Stenman and Matthias Zenger. 2004. An overview of the Scala programming language. (2004)."},{"key":"e_1_3_1_40_2","doi-asserted-by":"publisher","unstructured":"C.-H. Luke Ong. 2006. On Model-Checking Trees Generated by Higher-Order Recursion Schemes. In 21th IEEE Symposium on Logic in Computer Science (LICS 2006). 81\u201390. doi:10.1109\/LICS.2006.38","DOI":"10.1109\/LICS.2006.38"},{"key":"e_1_3_1_41_2","doi-asserted-by":"publisher","DOI":"10.1145\/2914770.2837634"},{"key":"e_1_3_1_42_2","doi-asserted-by":"publisher","unstructured":"Gordon D. Plotkin and John Power. 2003. Algebraic Operations and Generic Effects. Applied Categorical Structures 11 1 (2003) 69\u201394. doi:10.1023\/A:1023064908962","DOI":"10.1023\/A:1023064908962"},{"key":"e_1_3_1_43_2","doi-asserted-by":"publisher","unstructured":"Gordon D. Plotkin and Matija Pretnar. 2009. Handlers of Algebraic Effects. In Programming Languages and Systems 18th European Symposium on Programming ESOP 2009 . 80\u201394. doi:10.1007\/978-3-642-00590-9_7","DOI":"10.1007\/978-3-642-00590-9_7"},{"key":"e_1_3_1_44_2","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-9(4:23)2013"},{"key":"e_1_3_1_45_2","doi-asserted-by":"publisher","unstructured":"Matija Pretnar. 2015. An Introduction to Algebraic Effects and Handlers. Invited tutorial paper. In The 31st Conference on the Mathematical Foundations of Programming Semantics MFPS 2015 (Electronic Notes in Theoretical Computer Science Vol. 319). 19\u201335. doi:10.1016\/J.ENTCS.2015.12.003","DOI":"10.1016\/J.ENTCS.2015.12.003"},{"key":"e_1_3_1_46_2","doi-asserted-by":"publisher","unstructured":"John C. Reynolds. 1974. Towards a theory of type structure. In Programming Symposium Proceedings Colloque sur la Programmation. 408\u2013423. doi:10.1007\/3-540-06859-7_148","DOI":"10.1007\/3-540-06859-7_148"},{"key":"e_1_3_1_47_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-4118-8_9"},{"key":"e_1_3_1_48_2","doi-asserted-by":"publisher","unstructured":"Tom Schrijvers Maciej Pir\u00f3g Nicolas Wu and Mauro Jaskelioff. 2019. Monad transformers and modular algebraic effects: what binds them together. In Proceedings of the 12th ACM SIGPLAN International Symposium on Haskell Haskell@ICFP 2019. 98\u2013113. doi:10.1145\/3331545.3342595","DOI":"10.1145\/3331545.3342595"},{"key":"e_1_3_1_49_2","doi-asserted-by":"publisher","DOI":"10.1145\/3763184"},{"key":"e_1_3_1_50_2","doi-asserted-by":"publisher","DOI":"10.1145\/3571264"},{"key":"e_1_3_1_51_2","doi-asserted-by":"publisher","DOI":"10.1145\/3689805"},{"key":"e_1_3_1_52_2","doi-asserted-by":"publisher","DOI":"10.1145\/3704914"},{"key":"e_1_3_1_53_2","doi-asserted-by":"publisher","unstructured":"Christian Skalka and Scott F. Smith. 2004. History Effects and Verification. In Programming Languages and Systems: Second Asian Symposium APLAS 2004 (Lecture Notes in Computer Science Vol. 3302). 107\u2013128. doi:10.1007\/978-3-540-30477-7_8","DOI":"10.1007\/978-3-540-30477-7_8"},{"key":"e_1_3_1_54_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796807006466"},{"key":"e_1_3_1_55_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(06)X8001-1"},{"key":"e_1_3_1_56_2","doi-asserted-by":"publisher","unstructured":"Nikhil Swamy Joel Weinberger Cole Schlesinger Juan Chen and Benjamin Livshits. 2013. Verifying higher-order programs with the dijkstra monad. In ACM SIGPLAN Conference on Programming Language Design and Implementation PLDI '13. 387\u2013398. doi:10.1145\/2491956.2491978","DOI":"10.1145\/2491956.2491978"},{"key":"e_1_3_1_57_2","doi-asserted-by":"publisher","DOI":"10.2307\/2271658"},{"key":"e_1_3_1_58_2","volume-title":"Session-Typed Effect Handlers","author":"Tang Wenhao","year":"2024","unstructured":"Wenhao Tang. 2024. Session-Typed Effect Handlers. POPL 2024 SRC (2024)."},{"key":"e_1_3_1_59_2","doi-asserted-by":"publisher","unstructured":"Wenhao Tang and Sam Lindley. 2026. Rows and Capabilities as Modal Effects. Proc. ACM Program. Lang. 10 POPL (2026) 923\u2013950. doi:10.1145\/3776674","DOI":"10.1145\/3776674"},{"key":"e_1_3_1_60_2","doi-asserted-by":"publisher","DOI":"10.23638\/LMCS-14(1:2)2018"},{"key":"e_1_3_1_61_2","doi-asserted-by":"publisher","unstructured":"Takuma Yoshioka Taro Sekiyama and Atsushi Igarashi. 2024. Abstracting Effect Systems for Algebraic Effect Handlers. Proc. ACM Program. Lang. 8 ICFP (2024) 455\u2013484. doi:10.1145\/3674641","DOI":"10.1145\/3674641"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3828707","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,9,26]],"date-time":"2026-09-26T08:10:48Z","timestamp":1790410248000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3828707"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,8,17]]},"references-count":60,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2026,8,17]]}},"alternative-id":["10.1145\/3828707"],"URL":"https:\/\/doi.org\/10.1145\/3828707","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,8,17]]},"assertion":[{"value":"2026-02-19","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2026-05-13","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2026-08-17","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}