{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,19]],"date-time":"2026-09-19T12:01:08Z","timestamp":1789819268819,"version":"4.0.1"},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783662544570","type":"print"},{"value":"9783662544587","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-54458-7_22","type":"book-chapter","created":{"date-parts":[[2017,3,15]],"date-time":"2017-03-15T09:22:57Z","timestamp":1489569777000},"page":"370-386","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["On Higher-Order Probabilistic Subrecursion"],"prefix":"10.1007","author":[{"given":"Flavien","family":"Breuvart","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ugo","family":"Dal Lago","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Agathe","family":"Herrou","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2017,3,16]]},"reference":[{"key":"22_CR1","series-title":"Studies in Logic and the Foundations of Mathematics","volume-title":"The Lambda Calculus, Its Syntax and Semantics","author":"HP Barendregt","year":"1981","unstructured":"Barendregt, H.P.: The Lambda Calculus, Its Syntax and Semantics. Studies in Logic and the Foundations of Mathematics. North-Holland, Amsterdam (1981)"},{"key":"22_CR2","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":"22_CR3","unstructured":"Breuvart, F., Dal Lago, U., Herrou, A.: On probabilistic subrecursion (long version) (2016). http:\/\/arxiv.org\/abs\/1701.04786"},{"key":"22_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1007\/978-3-642-54833-8_12","volume-title":"Programming Languages and Systems","author":"R Crubill\u00e9","year":"2014","unstructured":"Crubill\u00e9, R., Dal Lago, U.: On probabilistic applicative bisimulation and call-by-value $$\\lambda $$-calculi. In: Shao, Z. (ed.) ESOP 2014. LNCS, vol. 8410, pp. 209\u2013228. Springer, Heidelberg (2014). doi:10.1007\/978-3-642-54833-8_12"},{"key":"22_CR5","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., Toldin, P.P.: A higher-order characterization of probabilistic polynomial time. Inf. Comput. 241, 114\u2013141 (2015)","journal-title":"Inf. Comput."},{"issue":"3","key":"22_CR6","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 - Theor. Inf. Appl. 46(3), 413\u2013450 (2012)","journal-title":"RAIRO - Theor. Inf. Appl."},{"issue":"2","key":"22_CR7","first-page":"177","volume":"24","author":"U Dal Lago","year":"2014","unstructured":"Dal Lago, U., Zuppiroli, S., Gabbrielli, M.: Probabilistic recursion theory and implicit computational complexity. Sci. Ann. Comp. Sci. 24(2), 177\u2013216 (2014)","journal-title":"Sci. Ann. Comp. Sci."},{"key":"22_CR8","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 Stud. 34, 183\u2013198 (1956)","journal-title":"Automata Stud."},{"key":"22_CR9","doi-asserted-by":"crossref","unstructured":"Ehrhard, T., Pagani, M., Tasson, C.: Probabilistic coherence spaces are fully abstract for probabilistic PCF. In: Sewell, P. (ed.) Proceedings of POPL. ACM (2014)","DOI":"10.1145\/2535838.2535865"},{"key":"22_CR10","doi-asserted-by":"crossref","unstructured":"Ferrer Fioriti, L.M., Hermanns, H.: Probabilistic termination: soundness, completeness, and compositionality. In: Proceedings of POPL, pp. 489\u2013501 (2015)","DOI":"10.1145\/2775051.2677001"},{"issue":"4","key":"22_CR11","doi-asserted-by":"publisher","first-page":"675","DOI":"10.1137\/0206049","volume":"6","author":"J Gill","year":"1977","unstructured":"Gill, J.: Computational complexity of probabilistic turing machines. SIAM J. Comput. 6(4), 675\u2013695 (1977)","journal-title":"SIAM J. Comput."},{"key":"22_CR12","volume-title":"Proofs and Types","author":"J-Y Girard","year":"1989","unstructured":"Girard, J.-Y., Taylor, P., Lafont, Y.: Proofs and Types. Cambridge University Press, Cambridge (1989)"},{"key":"22_CR13","unstructured":"Goodman, N.D., Mansinghka, V.K., Roy, D.M., Bonawitz, K., Tenenbaum, J.B.: Church: a language for generative models. In: UAI, pp. 220\u2013229 (2008)"},{"key":"22_CR14","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1016\/S1571-0661(05)80216-6","volume":"13","author":"A Jung","year":"1998","unstructured":"Jung, A., Tix, R.: The troublesome probabilistic powerdomain. Electr. Notes Theor. Comput. Sci. 13, 70\u201391 (1998)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"22_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1007\/978-3-662-48057-1_24","volume-title":"Mathematical Foundations of Computer Science 2015","author":"BL Kaminski","year":"2015","unstructured":"Kaminski, B.L., Katoen, J.-P.: On the hardness of almost\u2013sure termination. In: Italiano, G.F., Pighizzini, G., Sannella, D.T. (eds.) MFCS 2015. LNCS, vol. 9234, pp. 307\u2013318. Springer, Heidelberg (2015). doi:10.1007\/978-3-662-48057-1_24"},{"issue":"3","key":"22_CR16","doi-asserted-by":"publisher","first-page":"328","DOI":"10.1016\/0022-0000(81)90036-2","volume":"22","author":"D Kozen","year":"1981","unstructured":"Kozen, D.: Semantics of probabilistic programs. J. Comput. Syst. Sci. 22(3), 328\u2013350 (1981)","journal-title":"J. Comput. Syst. Sci."},{"key":"22_CR17","volume-title":"Foundations of Statistical Natural Language Processing","author":"CD Manning","year":"1999","unstructured":"Manning, C.D., Sch\u00fctze, H.: Foundations of Statistical Natural Language Processing, vol. 999. MIT Press, Cambridge (1999)"},{"key":"22_CR18","series-title":"Monographs in Computer Science","volume-title":"Abstraction, Refinement and Proof for Probabilistic Systems","author":"A McIver","year":"2005","unstructured":"McIver, A., Morgan, C.: Abstraction, Refinement and Proof for Probabilistic Systems. Monographs in Computer Science. Springer, Heidelberg (2005)"},{"key":"22_CR19","volume-title":"Probabilistic Reasoning in Intelligent Systems: Networks of Plausible Inference","author":"J Pearl","year":"1988","unstructured":"Pearl, J.: Probabilistic Reasoning in Intelligent Systems: Networks of Plausible Inference. Morgan Kaufmann, San Mateo (1988)"},{"key":"22_CR20","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511996504","volume-title":"Computer Vision: Models, Learning, and Inference","author":"SJD Prince","year":"2012","unstructured":"Prince, S.J.D.: Computer Vision: Models, Learning, and Inference. Cambridge University Press, New York (2012)"},{"key":"22_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"442","DOI":"10.1007\/3-540-08921-7_92","volume-title":"Mathematical Foundations of Computer Science 1978","author":"N Saheb-Djahromi","year":"1978","unstructured":"Saheb-Djahromi, N.: Probabilistic LCF. In: Winkowski, J. (ed.) MFCS 1978. LNCS, vol. 64, pp. 442\u2013451. Springer, Heidelberg (1978). doi:10.1007\/3-540-08921-7_92"},{"issue":"3","key":"22_CR22","doi-asserted-by":"publisher","first-page":"704","DOI":"10.1090\/S0002-9939-1969-0249221-4","volume":"22","author":"ES Santos","year":"1969","unstructured":"Santos, E.S.: Probabilistic turing machines and computability. Proc. Am. Math. Soc. 22(3), 704\u2013710 (1969)","journal-title":"Proc. Am. Math. Soc."},{"key":"22_CR23","volume-title":"Lectures on the Curry-Howard Isomorphism","author":"MH S\u00f8rensen","year":"2006","unstructured":"S\u00f8rensen, M.H., Urzyczyn, P.: Lectures on the Curry-Howard Isomorphism. Elsevier Science Inc., New York (2006)"},{"key":"22_CR24","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1016\/0304-3975(79)90007-0","volume":"9","author":"R Statman","year":"1979","unstructured":"Statman, R.: The typed lambda-calculus is not elementary recursive. Theor. Comput. Sci. 9, 73\u201381 (1979)","journal-title":"Theor. Comput. Sci."},{"key":"22_CR25","doi-asserted-by":"crossref","unstructured":"Staton, S., Yang, H., Heunen, C., Kammar, O., Wood, F.: Semantics for probabilistic programming: higher-order functions, continuous distributions, and soft constraints. In: Proceedings of LICS, pp. 525\u2013534 (2016)","DOI":"10.1145\/2933575.2935313"}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Science and Computation Structures"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-54458-7_22","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,21]],"date-time":"2021-04-21T02:05:53Z","timestamp":1618970753000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-662-54458-7_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783662544570","9783662544587"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-54458-7_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017]]},"assertion":[{"value":"16 March 2017","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FoSSaCS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Foundations of Software Science and Computation Structures","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":"24 April 2017","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 April 2017","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fossacs2017","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/www.etaps.org\/index.php\/2017\/fossacs","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"}]}}