{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,6]],"date-time":"2026-02-06T00:24:37Z","timestamp":1770337477473,"version":"3.49.0"},"reference-count":41,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2019,3,15]],"date-time":"2019-03-15T00:00:00Z","timestamp":1552608000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"ANR projects","award":["12IS02001 PACE and 14CE250005 ELICA"],"award-info":[{"award-number":["12IS02001 PACE and 14CE250005 ELICA"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Program. Lang. Syst."],"published-print":{"date-parts":[[2019,6,30]]},"abstract":"<jats:p>We introduce a system of monadic affine sized types, which substantially generalizes usual sized types and allows in this way to capture probabilistic higher-order programs that terminate almost surely. Going beyond plain, strong normalization without losing soundness turns out to be a hard task, which cannot be accomplished without a richer, quantitative notion of types, but also without imposing some affinity constraints. The proposed type system is powerful enough to type classic examples of probabilistically terminating programs such as random walks. The way typable programs are proved to be almost surely terminating is based on reducibility but requires a substantial adaptation of the technique.<\/jats:p>","DOI":"10.1145\/3293605","type":"journal-article","created":{"date-parts":[[2019,3,15]],"date-time":"2019-03-15T12:13:05Z","timestamp":1552651985000},"page":"1-65","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":13,"title":["Probabilistic Termination by Monadic Affine Sized Typing"],"prefix":"10.1145","volume":"41","author":[{"given":"Ugo Dal","family":"Lago","sequence":"first","affiliation":[{"name":"University of Bologna 8 INRIA Sophia Antipolis, Bologna, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Charles","family":"Grellois","sequence":"additional","affiliation":[{"name":"INRIA Sophia Antipolis"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2019,3,15]]},"reference":[{"key":"e_1_2_1_1_1","first-page":"277","article-title":"Termination checking with types","volume":"38","author":"Abel Andreas","year":"2004","unstructured":"Andreas Abel. 2004. Termination checking with types. ITA 38, 4 (2004), 277--319.","journal-title":"ITA"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.5555\/646790.704524"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129503004122"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480894"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.5555\/2033036.2033043"},{"key":"e_1_2_1_6_1","volume-title":"ALFA Summer School 2008 (LNCS), Ana Bove, Lu\u00eds Soares Barbosa","author":"Barthe Gilles","unstructured":"Gilles Barthe, Benjamin Gr\u00e9goire, and Colin Riba. 2008. A tutorial on type-based termination. In ALFA Summer School 2008 (LNCS), Ana Bove, Lu\u00eds Soares Barbosa, Alberto Pardo, and Jorge Sousa Pinto (Eds.), Vol. 5520. Springer, 100--152."},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-87531-4_35"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-32033-3_24"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.5555\/647201.718862"},{"key":"e_1_2_1_10_1","volume-title":"21st ACM-SIAM Symposium on Discrete Algorithms.","author":"Br\u00e1zdil T.","unstructured":"T. Br\u00e1zdil, V. Bro\u017eek, K. Etessami, A. Ku\u010dera, and D. Wojtczak. 2010. One-counter Markov decision processes. In 21st ACM-SIAM Symposium on Discrete Algorithms."},{"key":"e_1_2_1_11_1","volume-title":"FCT\u201915 (LNCS)","author":"Cappai Alberto","unstructured":"Alberto Cappai and Ugo Dal Lago. 2015. On equivalences, metrics, and polynomial time. In FCT\u201915 (LNCS), Adrian Kosowski and Igor Walukiewicz (Eds.), Vol. 9210. Springer, 311--323."},{"key":"e_1_2_1_12_1","volume-title":"CAV\u201913 (LNCS)","author":"Chakarov Aleksandar","unstructured":"Aleksandar Chakarov and Sriram Sankaranarayanan. 2013. Probabilistic program analysis with martingales. In CAV\u201913 (LNCS), Natasha Sharygina and Helmut Veith (Eds.), Vol. 8044. Springer, 511--526."},{"key":"e_1_2_1_13_1","volume-title":"CAV\u201916 (LNCS)","author":"Chatterjee Krishnendu","unstructured":"Krishnendu Chatterjee, Hongfei Fu, and Amir Kafshdar Goharshady. 2016. Termination analysis of probabilistic programs through Positivstellensatz\u2019s. In CAV\u201916 (LNCS), Swarat Chaudhuri and Azadeh Farzan (Eds.), Vol. 9779. Springer, 3--22."},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","unstructured":"Krishnendu Chatterjee Hongfei Fu Petr Novotn\u00fd and Rouzbeh Hasheminezhad. 2016. Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs. In POPL\u201916 Rastislav Bod\u00edk and Rupak Majumdar (Eds.). ACM 327--342. 10.1145\/2837614.2837639","DOI":"10.1145\/2837614.2837639"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2005.52"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","unstructured":"Ugo Dal Lago. 2011. A short introduction to implicit computational complexity. In ESSLLI\u201910. 89--109. 10.1007\/978-3-642-31485-8_3","DOI":"10.1007\/978-3-642-31485-8_3"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2011.22"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2010.12.025"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2014.10.009"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1051\/ita\/2012012"},{"key":"e_1_2_1_21_1","first-page":"183","article-title":"Computability by probabilistic machines","volume":"34","author":"de Leeuw Karel","year":"1956","unstructured":"Karel de Leeuw, Edward Forrest Moore, Claude Elwood Shannon, and Norman Shapiro. 1956. Computability by probabilistic machines. Automata Stud. 34 (1956), 183--212.","journal-title":"Automata Stud."},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_14"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2677001"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.5555\/64805"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.5555\/3023476.3023503"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.5555\/647847.736896"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/237721.240882"},{"key":"e_1_2_1_28_1","volume-title":"MFCS (1) (Lecture Notes in Computer Science)","author":"Kaminski Benjamin Lucien","unstructured":"Benjamin Lucien Kaminski and Joost-Pieter Katoen. 2015. On the hardness of almost-sure termination. In MFCS (1) (Lecture Notes in Computer Science), Vol. 9234. Springer, 307--318."},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3208102"},{"key":"e_1_2_1_30_1","volume-title":"ESOP\u201917 (LNCS)","author":"Lago Ugo Dal","unstructured":"Ugo Dal Lago and Charles Grellois. 2017. Probabilistic termination by monadic affine sized typing. In ESOP\u201917 (LNCS), Hongseok Yang (Ed.), Vol. 10201. Springer, 393--419."},{"key":"e_1_2_1_31_1","first-page":"177","article-title":"Probabilistic recursion theory and implicit computational complexity. Sci","volume":"24","author":"Lago Ugo Dal","year":"2014","unstructured":"Ugo Dal Lago, Sara Zuppiroli, and Maurizio Gabbrielli. 2014. Probabilistic recursion theory and implicit computational complexity. Sci. Ann. Comp. Sci. 24, 2 (2014), 177--216.","journal-title":"Ann. Comp. Sci."},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.5555\/311445"},{"key":"e_1_2_1_33_1","volume-title":"Refinement and Proof for Probabilistic Systems","author":"McIver Annabelle","unstructured":"Annabelle McIver and Carroll Morgan. 2005. Abstraction, Refinement and Proof for Probabilistic Systems. Springer."},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158121"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.5555\/211390"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","unstructured":"Judea Pearl. 1989. Probabilistic Reasoning in Intelligent Systems - Networks of Plausible Inference. Morgan Kaufmann.","DOI":"10.5555\/52121"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01019462"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.5555\/17634"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00153-007-0042-6"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","unstructured":"Sebastian Thrun. 2002. Robotic mapping: A survey. In Exploring Artificial Intelligence in the New Millenium. Morgan Kaufmann.","DOI":"10.5555\/779343.779345"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1019916231463"}],"container-title":["ACM Transactions on Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3293605","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3293605","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T01:02:01Z","timestamp":1750208521000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3293605"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,3,15]]},"references-count":41,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2019,6,30]]}},"alternative-id":["10.1145\/3293605"],"URL":"https:\/\/doi.org\/10.1145\/3293605","relation":{},"ISSN":["0164-0925","1558-4593"],"issn-type":[{"value":"0164-0925","type":"print"},{"value":"1558-4593","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,3,15]]},"assertion":[{"value":"2017-05-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2018-10-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2019-03-15","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}