{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,11,13]],"date-time":"2026-11-13T03:22:29Z","timestamp":1794540149120,"version":"4.9.1"},"publisher-location":"Berlin, Heidelberg","reference-count":34,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783662544334","type":"print"},{"value":"9783662544341","type":"electronic"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-662-54434-1_15","type":"book-chapter","created":{"date-parts":[[2017,3,18]],"date-time":"2017-03-18T00:20:06Z","timestamp":1489796406000},"page":"393-419","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":13,"title":["Probabilistic Termination by Monadic Affine Sized Typing"],"prefix":"10.1007","author":[{"given":"Ugo","family":"Dal Lago","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Charles","family":"Grellois","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2017,3,19]]},"reference":[{"key":"15_CR1","volume-title":"Foundations of Statistical Natural Language Processing","author":"CD Manning","year":"2001","unstructured":"Manning, C.D., Sch\u00fctze, H.: Foundations of Statistical Natural Language Processing. MIT Press, Cambridge (2001)"},{"key":"15_CR2","series-title":"Morgan Kaufmann Series in Representation and Reasoning","volume-title":"Probabilistic Reasoning in Intelligent Systems - Networks of Plausible Inference","author":"J Pearl","year":"1989","unstructured":"Pearl, J.: Probabilistic Reasoning in Intelligent Systems - Networks of Plausible Inference. Morgan Kaufmann Series in Representation and Reasoning. Morgan Kaufmann, Burlington (1989)"},{"key":"15_CR3","unstructured":"Thrun, S.: Robotic mapping: a survey. In: Exploring Artificial Intelligence in the New Millenium, Morgan Kaufmann (2002)"},{"key":"15_CR4","first-page":"183","volume":"34","author":"K de Leeuw","year":"1956","unstructured":"de Leeuw, K., Moore, E.F., Shannon, C.E., Shapiro, N.: Computability by probabilistic machines. Automata Studies 34, 183\u2013212 (1956)","journal-title":"Automata Studies"},{"key":"15_CR5","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511814075","volume-title":"Randomized Algorithms","author":"R Motwani","year":"1995","unstructured":"Motwani, R., Raghavan, P.: Randomized Algorithms. Cambridge University Press, Cambridge (1995)"},{"key":"15_CR6","doi-asserted-by":"crossref","unstructured":"Barthe, G., Gr\u00e9goire, B., B\u00e9guelin, S.Z.: Formal certification of code-based cryptographic proofs. In: Shao, Z., Pierce, B.C. (eds.) POPL 2009, pp. 90\u2013101. ACM (2009)","DOI":"10.1145\/1594834.1480894"},{"key":"15_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1007\/978-3-642-22792-9_5","volume-title":"Advances in Cryptology \u2013 CRYPTO 2011","author":"G Barthe","year":"2011","unstructured":"Barthe, G., Gr\u00e9goire, B., Heraud, S., B\u00e9guelin, S.Z.: Computer-aided security proofs for the working cryptographer. In: Rogaway, P. (ed.) CRYPTO 2011. LNCS, vol. 6841, pp. 71\u201390. Springer, Heidelberg (2011). doi:10.1007\/978-3-642-22792-9_5"},{"key":"15_CR8","unstructured":"Goodman, N.D., Mansinghka, V.K., Roy, D.M., Bonawitz, K., Tenenbaum, J.B.: Church: a language for generative models. In: McAllester, D.A., Myllym\u00e4ki, P. (eds.) UAI 2008, pp. 220\u2013229. AUAI Press (2008)"},{"key":"15_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"252","DOI":"10.1007\/3-540-45610-4_18","volume-title":"Rewriting Techniques and Applications","author":"O Bournez","year":"2002","unstructured":"Bournez, O., Kirchner, C.: Probabilistic rewrite strategies. applications to ELAN. In: Tison, S. (ed.) RTA 2002. LNCS, vol. 2378, pp. 252\u2013266. Springer, Heidelberg (2002). doi:10.1007\/3-540-45610-4_18"},{"key":"15_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/978-3-642-31424-7_14","volume-title":"Computer Aided Verification","author":"J Esparza","year":"2012","unstructured":"Esparza, J., Gaiser, A., Kiefer, S.: Proving termination of probabilistic programs using patterns. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 123\u2013138. Springer, Heidelberg (2012). doi:10.1007\/978-3-642-31424-7_14"},{"key":"15_CR11","doi-asserted-by":"crossref","unstructured":"Fioriti, L.M.F., Hermanns, H.: Probabilistic termination: soundness, completeness, and compositionality. In: Rajamani, S.K., Walker, D. (eds.) POPL 2015, pp. 489\u2013501. ACM (2015)","DOI":"10.1145\/2775051.2677001"},{"key":"15_CR12","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Fu, H., Novotn\u00fd, P., Hasheminezhad, R.: Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs. In: Bod\u00edk, R., Majumdar, R. (eds.) POPL 2016, pp. 327\u2013342. ACM (2016)","DOI":"10.1145\/2914770.2837639"},{"key":"15_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-319-41528-4_1","volume-title":"Computer Aided Verification","author":"K Chatterjee","year":"2016","unstructured":"Chatterjee, K., Fu, H., Goharshady, A.K.: Termination analysis of probabilistic programs through Positivstellensatz\u2019s. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9779, pp. 3\u201322. Springer, Heidelberg (2016). doi:10.1007\/978-3-319-41528-4_1"},{"key":"15_CR14","doi-asserted-by":"crossref","unstructured":"Hughes, J., Pareto, L., Sabry, A.: Proving the correctness of reactive systems using sized types. In: Boehm, H. Jr., Shackle, G.L.S. (eds.) POPL 1996, pp. 410\u2013423. ACM Press (1996)","DOI":"10.1145\/237721.240882"},{"key":"15_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1007\/BFb0028020","volume-title":"Computer Science Logic","author":"M Hofmann","year":"1998","unstructured":"Hofmann, M.: A mixed modal\/linear lambda calculus with applications to Bellantoni-Cook safe recursion. In: Nielsen, M., Thomas, W. (eds.) CSL 1997. LNCS, vol. 1414, pp. 275\u2013294. Springer, Heidelberg (1998). doi:10.1007\/BFb0028020"},{"key":"15_CR16","volume-title":"Proofs and Types","author":"JY Girard","year":"1989","unstructured":"Girard, J.Y., Taylor, P., Lafont, Y.: Proofs and Types. Cambridge University Press, New York (1989)"},{"issue":"20","key":"15_CR17","doi-asserted-by":"publisher","first-page":"2029","DOI":"10.1016\/j.tcs.2010.12.025","volume":"412","author":"U Dal Lago","year":"2011","unstructured":"Dal Lago, U., Hofmann, M.: Realizability models and implicit complexity. Theoret. Comput. Sci. 412(20), 2029\u20132047 (2011)","journal-title":"Theoret. Comput. Sci."},{"key":"15_CR18","unstructured":"Dal Lago, U., Grellois, C.: Probabilistic termination by monadic affine sized typing (long version) (2016). https:\/\/arxiv.org\/abs\/1701.04089"},{"issue":"1","key":"15_CR19","first-page":"97","volume":"14","author":"G Barthe","year":"2004","unstructured":"Barthe, G., Frade, M.J., Gim\u00e9nez, E., Pinto, L., Uustalu, T.: Type-based termination of recursive definitions. MSCS 14(1), 97\u2013141 (2004)","journal-title":"MSCS"},{"key":"15_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"100","DOI":"10.1007\/978-3-642-03153-3_3","volume-title":"Language Engineering and Rigorous Software Development","author":"G Barthe","year":"2009","unstructured":"Barthe, G., Gr\u00e9goire, B., Riba, C.: A tutorial on type-based termination. In: Bove, A., Barbosa, L.S., Pardo, A., Pinto, J.S. (eds.) LerNet 2008. LNCS, vol. 5520, pp. 100\u2013152. Springer, Heidelberg (2009). doi:10.1007\/978-3-642-03153-3_3"},{"key":"15_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"493","DOI":"10.1007\/978-3-540-87531-4_35","volume-title":"Computer Science Logic","author":"G Barthe","year":"2008","unstructured":"Barthe, G., Gr\u00e9goire, B., Riba, C.: Type-based termination with sized products. In: Kaminski, M., Martini, S. (eds.) CSL 2008. LNCS, vol. 5213, pp. 493\u2013507. Springer, Heidelberg (2008). doi:10.1007\/978-3-540-87531-4_35"},{"issue":"4","key":"15_CR22","first-page":"277","volume":"38","author":"A Abel","year":"2004","unstructured":"Abel, A.: Termination checking with types. ITA 38(4), 277\u2013319 (2004)","journal-title":"ITA"},{"issue":"1","key":"15_CR23","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1023\/A:1019916231463","volume":"15","author":"H Xi","year":"2002","unstructured":"Xi, H.: Dependent types for program termination verification. High.-Order Symb. Comput. 15(1), 91\u2013131 (2002)","journal-title":"High.-Order Symb. Comput."},{"key":"15_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"48","DOI":"10.1007\/BFb0053541","volume-title":"Foundations of Software Science and Computation Structures","author":"RM Amadio","year":"1998","unstructured":"Amadio, R.M., Coupet-Grimal, S.: Analysis of a guard condition in type theory. In: Nivat, M. (ed.) FoSSaCS 1998. LNCS, vol. 1378, pp. 48\u201362. Springer, Heidelberg (1998). doi:10.1007\/BFb0053541"},{"key":"15_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1007\/978-3-540-32033-3_24","volume-title":"Term Rewriting and Applications","author":"O Bournez","year":"2005","unstructured":"Bournez, O., Garnier, F.: Proving positive almost-sure termination. In: Giesl, J. (ed.) RTA 2005. LNCS, vol. 3467, pp. 323\u2013337. Springer, Heidelberg (2005). doi:10.1007\/978-3-540-32033-3_24"},{"key":"15_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"511","DOI":"10.1007\/978-3-642-39799-8_34","volume-title":"Computer Aided Verification","author":"A Chakarov","year":"2013","unstructured":"Chakarov, A., Sankaranarayanan, S.: Probabilistic program analysis with martingales. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 511\u2013526. Springer, Heidelberg (2013). doi:10.1007\/978-3-642-39799-8_34"},{"key":"15_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"311","DOI":"10.1007\/978-3-319-22177-9_24","volume-title":"Fundamentals of Computation Theory","author":"A Cappai","year":"2015","unstructured":"Cappai, A., Dal Lago, U.: On equivalences, metrics, and polynomial time. In: Kosowski, A., Walukiewicz, I. (eds.) FCT 2015. LNCS, vol. 9210, pp. 311\u2013323. Springer, Cham (2015). doi:10.1007\/978-3-319-22177-9_24"},{"key":"15_CR28","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1016\/j.ic.2014.10.009","volume":"241","author":"U Dal Lago","year":"2015","unstructured":"Dal Lago, U., Parisen Toldin, P.: A higher-order characterization of probabilistic polynomial time. Inf. Comput. 241, 114\u2013141 (2015)","journal-title":"Inf. Comput."},{"key":"15_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1007\/978-3-642-31485-8_3","volume-title":"Lectures on Logic and Computation","author":"U Dal Lago","year":"2012","unstructured":"Dal Lago, U.: A short introduction to implicit computational complexity. In: Bezhanishvili, N., Goranko, V. (eds.) ESSLLI 2010-2011. LNCS, vol. 7388, pp. 89\u2013109. Springer, Heidelberg (2012). doi:10.1007\/978-3-642-31485-8_3"},{"issue":"3","key":"15_CR30","doi-asserted-by":"publisher","first-page":"413","DOI":"10.1051\/ita\/2012012","volume":"46","author":"U Dal Lago","year":"2012","unstructured":"Dal Lago, U., Zorzi, M.: Probabilistic operational semantics for the lambda calculus. RAIRO - Theoret. Inf. Appl. 46(3), 413\u2013450 (2012)","journal-title":"RAIRO - Theoret. Inf. Appl."},{"key":"15_CR31","doi-asserted-by":"crossref","unstructured":"Br\u00e1zdil, T., Bro\u017eek, V., Etessami, K., Ku\u010dera, A., Wojtczak, D.: One-counter Markov decision processes. In: 21st ACM-SIAM Symposium on Discrete Algorithms (2010)","DOI":"10.1137\/1.9781611973075.70"},{"key":"15_CR32","unstructured":"Dal Lago, U.: The geometry of linear higher-order recursion. In: LICS 2005, pp. 366\u2013375. IEEE Computer Society (2005)"},{"issue":"3\u20134","key":"15_CR33","first-page":"289","volume":"6","author":"A Sabry","year":"1993","unstructured":"Sabry, A., Felleisen, M.: Reasoning about programs in continuation-passing style. LISP Symb. Comput. 6(3\u20134), 289\u2013360 (1993)","journal-title":"LISP Symb. Comput."},{"key":"15_CR34","doi-asserted-by":"crossref","unstructured":"Dal Lago, U., Gaboardi, M.: Linear dependent types and relative completeness. In: LICS 2011, pp. 133\u2013142. IEEE Computer Society (2011)","DOI":"10.1109\/LICS.2011.22"}],"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-662-54434-1_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,10,26]],"date-time":"2021-10-26T11:44:56Z","timestamp":1635248696000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-662-54434-1_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783662544334","9783662544341"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-54434-1_15","relation":{"is-part-of":[{"id-type":"doi","id":"https:\/\/doi.org\/10.1007\/978-3-662-54434-1","asserted-by":"object"}]},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017]]},"assertion":[{"value":"19 March 2017","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":"Uppsala","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Sweden","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2017","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25 April 2017","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28 April 2017","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"esop2017a","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/www.etaps.org\/index.php\/2017\/esop","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}