{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,19]],"date-time":"2026-06-19T07:53:01Z","timestamp":1781855581732,"version":"3.54.5"},"reference-count":69,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2021,1,4]],"date-time":"2021-01-04T00:00:00Z","timestamp":1609718400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["818616"],"award-info":[{"award-number":["818616"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001665","name":"Agence Nationale de la Recherche","doi-asserted-by":"publisher","award":["19-CE48-0014"],"award-info":[{"award-number":["19-CE48-0014"]}],"id":[{"id":"10.13039\/501100001665","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100003407","name":"Ministero dell\u2019Istruzione, dell\u2019Universit\u00e0 e della Ricerca","doi-asserted-by":"publisher","award":["201784YSZ5"],"award-info":[{"award-number":["201784YSZ5"]}],"id":[{"id":"10.13039\/501100003407","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":[[2021,1,4]]},"abstract":"<jats:p>\n                    Randomized higher-order computation can be seen as being captured by a \u03bb-calculus endowed with a single algebraic operation, namely a construct for binary probabilistic choice. What matters about such computations is the\n                    <jats:italic toggle=\"yes\">probability<\/jats:italic>\n                    of obtaining any given result, rather than the\n                    <jats:italic toggle=\"yes\">possibility<\/jats:italic>\n                    or the\n                    <jats:italic toggle=\"yes\">necessity<\/jats:italic>\n                    of obtaining it, like in (non)deterministic computation. Termination, arguably the simplest kind of reachability problem, can be spelled out in at least two ways, depending on whether it talks about the probability of convergence or about the expected evaluation time, the second one providing a stronger guarantee. In this paper, we show that intersection types are capable of precisely characterizing\n                    <jats:italic toggle=\"yes\">both<\/jats:italic>\n                    notions of termination inside\n                    <jats:italic toggle=\"yes\">a single<\/jats:italic>\n                    system of types: the probability of convergence of any \u03bb-term can be underapproximated by its\n                    <jats:italic toggle=\"yes\">type<\/jats:italic>\n                    , while the underlying derivation\u2019s\n                    <jats:italic toggle=\"yes\">weight<\/jats:italic>\n                    gives a lower bound to the term\u2019s expected number of steps to normal form. Noticeably, both approximations are tight\u2014not only soundness but also completeness holds. The crucial ingredient is non-idempotency, without which it would be impossible to reason on the expected number of reduction steps which are necessary to completely evaluate any term. Besides, the kind of approximation we obtain is proved to be\n                    <jats:italic toggle=\"yes\">optimal<\/jats:italic>\n                    recursion theoretically: no recursively enumerable formal system can do better than that.\n                  <\/jats:p>","DOI":"10.1145\/3434313","type":"journal-article","created":{"date-parts":[[2021,1,4]],"date-time":"2021-01-04T12:34:24Z","timestamp":1609763664000},"page":"1-32","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":20,"title":["Intersection types and (positive) almost-sure termination"],"prefix":"10.1145","volume":"5","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9200-070X","authenticated-orcid":false,"given":"Ugo","family":"Dal Lago","sequence":"first","affiliation":[{"name":"University of Bologna, Italy"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Claudia","family":"Faggian","sequence":"additional","affiliation":[{"name":"University of Paris, France \/ IRIF, France \/ CNRS, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Simona Ronchi Della","family":"Rocca","sequence":"additional","affiliation":[{"name":"University of Turin, Italy"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2021,1,4]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236789"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17184-1_15"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2019.8785725"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.2307\/2273659"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","unstructured":"Alexis Bernadet and St\u00e9phane Lengrand. 2013. Non-idempotent intersection types and strong normalisation. Log. Methods Comput. Sci. 9 4 ( 2013 ). https:\/\/doi.org\/10.2168\/LMCS-9( 4 :3) 2013 10.2168\/LMCS-9(4:3)2013","DOI":"10.2168\/LMCS-9("},{"key":"e_1_2_1_7_1","volume-title":"Probability and measure","author":"Billingsley Patrick","unstructured":"Patrick Billingsley. 1979. Probability and measure. John Wiley and Sons, New York."},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46678-0_18"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/11805618_27"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-43476-6"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236950.3236968"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24725-8_21"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_34"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","unstructured":"Mario Coppo and Mariangiola Dezani-Ciancaglini. 1978. A new type assignment for lambda-terms. Archiv f\u00fcr mathematische Logik und Grundlagenforschung 19 1 ( 1978 ) 139-156. https:\/\/doi.org\/10.1007\/BF02011875 10.1007\/BF02011875","DOI":"10.1007\/BF02011875"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1305\/ndjfl\/1093883253"},{"key":"e_1_2_1_16_1","volume-title":"To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism","author":"Coppo Mario","unstructured":"Mario Coppo, Mariangiola Dezani-Ciancaglini, and Betti Venneri. 1980. Principal type schemes and lambda-calculus semantics. In To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism. Academic Press, 535-560."},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1002\/malq.19810270205"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","unstructured":"Mario Coppo Mariangiola Dezani-Ciancaglini and Maddalena Zacchi. 1987. Type Theories Normal Forms and D \u221e-LambdaModels. Inf. Comput. 72 2 ( 1987 ) 85-116. https:\/\/doi.org\/10.1016\/ 0890-5401 ( 87 ) 90042-3 10.1016\/0890-5401(87)90042-3","DOI":"10.1016\/0890-5401(87)90042-3"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/263699.263744"},{"key":"e_1_2_1_20_1","unstructured":"Ugo Dal Lago and Beniamino Accattoli. 2017. Encoding Turing Machines into the Deterministic Lambda-Calculus. CoRR abs\/1711.10078 ( 2017 ). http:\/\/arxiv.org\/abs\/1711.10078"},{"key":"e_1_2_1_21_1","volume-title":"http:\/\/arxiv.org\/abs\/","author":"Lago Ugo Dal","year":"2010","unstructured":"Ugo Dal Lago, Claudia Faggian, and Simona Ronchi Della Rocca. 2020. Intersection Types and (Positive) Almost-Sure Termination (Extended version). CoRR 2010. 12689 ( 2020 ). http:\/\/arxiv.org\/abs\/ 2010.12689"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","unstructured":"Ugo Dal Lago and Marco Gaboardi. 2011. Linear Dependent Types and Relative Completeness. Log. Methods Comput. Sci. 8 4 ( 2011 ). https:\/\/doi.org\/10.2168\/LMCS-8( 4 :11) 2012 10.2168\/LMCS-8(4:11)2012","DOI":"10.2168\/LMCS-8("},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3293605"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535872"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","unstructured":"Ugo Dal Lago and Margherita Zorzi. 2012. Probabilistic operational semantics for the lambda calculus. RAIRO-Theor. Inf. and Applic. 46 3 ( 2012 ) 413-450. https:\/\/doi.org\/10.1051\/ita\/2012012 10.1051\/ita\/2012012","DOI":"10.1051\/ita\/2012012"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","unstructured":"Daniel de Carvalho. 2018. Execution time of \u03bb-terms via denotational semantics and intersection types. Math. Struct. Comput. Sci. 28 7 ( 2018 ) 1169-1203. https:\/\/doi.org\/10.1017\/S0960129516000396 Availabel in preprint form from 2009 https:\/\/arxiv.org\/abs\/0905.4251.","DOI":"10.1017\/S0960129516000396"},{"key":"e_1_2_1_27_1","doi-asserted-by":"crossref","unstructured":"Karel De Leeuw Edward F Moore Claude E Shannon and Norman Shapiro. 1956. Computability by probabilistic machines. Automata studies 34 ( 1956 ) 183-198.","DOI":"10.1515\/9781400882618-010"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45413-6_25"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-57182-5_32"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535865"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/1462153.1462154"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2677001"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-57887-0_115"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1137\/0206049"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(08)70843-7"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(84)90070-9"},{"key":"e_1_2_1_38_1","first-page":"220","article-title":"Church: a language for generative models","author":"Goodman Noah D.","year":"2008","unstructured":"Noah D. Goodman, Vikash K. Mansinghka, Daniel M. Roy, Keith Bonawitz, and Joshua B. Tenenbaum. 2008. Church: a language for generative models. In UAI. 220-229.","journal-title":"UAI."},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","unstructured":"Jean Goubault-Larrecq. 2015. Full Abstraction for Non-Deterministic and Probabilistic Extensions of PCF I: the Angelic Cases. Journal of Logic and Algebraic Methods in Programming 84 ( 2015 ) 155-184. https:\/\/doi.org\/10.1016\/j.jlamp. 2014. 09.003 10.1016\/j.jlamp.2014.09.003","DOI":"10.1016\/j.jlamp"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/237721.240882"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","unstructured":"Achim Jung and Regina Tix. 1998. The troublesome probabilistic powerdomain. Electr. Notes Theor. Comput. Sci. 13 ( 1998 ) 70-91. https:\/\/doi.org\/10.1016\/S1571-0661 ( 05 ) 80216-6 10.1016\/S1571-0661(05)80216-6","DOI":"10.1016\/S1571-0661"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-018-0321-1"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/3208102"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/10.3"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/292540.292556"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480933"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2019.8785679"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2009.29"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(81)90036-2"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1007\/b138392"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/360204.360211"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1017\/cbo9780511814075"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/1016850.1016871"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192394"},{"key":"e_1_2_1_56_1","volume-title":"Classical Recursion Theory","author":"Odifreddi Piergiorgio","unstructured":"Piergiorgio Odifreddi. 1989. Classical Recursion Theory. Elsevier."},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS"},{"key":"e_1_2_1_58_1","volume-title":"Types and programming languages","author":"Pierce Benjamin C.","unstructured":"Benjamin C. Pierce. 2002. Types and programming languages. MIT Press."},{"key":"e_1_2_1_59_1","doi-asserted-by":"publisher","unstructured":"Gordon D. Plotkin. 1975. Call-by-Name Call-by-Value and the lambda-Calculus. Theor. Comput. Sci. 1 2 ( 1975 ) 125-159. https:\/\/doi.org\/10.1016\/ 0304-3975 ( 75 ) 90017-1 10.1016\/0304-3975(75)90017-1","DOI":"10.1016\/0304-3975(75)90017-1"},{"key":"e_1_2_1_60_1","volume-title":"To H.B. Curry: Essays on Combinatory Logic, Lambda Caclulus and Formalism","author":"Pottinger Garrell","unstructured":"Garrell Pottinger. 1980. A type assignment for the strongly normalizable lambda-terms. In To H.B. Curry: Essays on Combinatory Logic, Lambda Caclulus and Formalism. Academic Press, 561-577."},{"key":"e_1_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1002\/9780470316887"},{"key":"e_1_2_1_62_1","doi-asserted-by":"publisher","unstructured":"Michael O Rabin. 1963. Probabilistic automata. Information and control 6 3 ( 1963 ) 230-245. https:\/\/doi.org\/10.1016\/S0019-9958 ( 63 ) 90290-0 10.1016\/S0019-9958(63)90290-0","DOI":"10.1016\/S0019-9958"},{"key":"e_1_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-504-08921-7_92"},{"key":"e_1_2_1_64_1","doi-asserted-by":"publisher","DOI":"10.1090\/S0002-9939-1969-0249221-4"},{"key":"e_1_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(06)80005-4"},{"key":"e_1_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-23461-8_36"},{"key":"e_1_2_1_67_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33475-7_25"},{"key":"e_1_2_1_68_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.121.1"},{"key":"e_1_2_1_69_1","volume-title":"To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism","author":"Wadsworth Christopher","unstructured":"Christopher Wadsworth. 1980. Some unusual \u03bb-calculus numeral systems. In To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, J.P. Seldin and J.R. Hindley (Eds.). Academic Press."}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3434313","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3434313","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,6,19]],"date-time":"2026-06-19T07:24:38Z","timestamp":1781853878000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3434313"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,1,4]]},"references-count":69,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2021,1,4]]}},"alternative-id":["10.1145\/3434313"],"URL":"https:\/\/doi.org\/10.1145\/3434313","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,1,4]]},"assertion":[{"value":"2021-01-04","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}