{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:21:44Z","timestamp":1751660504928,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642335112"},{"type":"electronic","value":"9783642335129"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-33512-9_2","type":"book-chapter","created":{"date-parts":[[2012,9,8]],"date-time":"2012-09-08T07:18:53Z","timestamp":1347088733000},"page":"6-20","source":"Crossref","is-referenced-by-count":9,"title":["Recursive Schemes, Krivine Machines, and Collapsible Pushdown Automata"],"prefix":"10.1007","author":[{"given":"Sylvain","family":"Salvati","sequence":"first","affiliation":[]},{"given":"Igor","family":"Walukiewicz","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"2_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/11417170_5","volume-title":"Typed Lambda Calculi and Applications","author":"K. Aehlig","year":"2005","unstructured":"Aehlig, K., de Miranda, J.G., Ong, C.-H.L.: The Monadic Second Order Theory of Trees Given by Arbitrary Level-Two Recursion Schemes Is Decidable. In: Urzyczyn, P. (ed.) TLCA 2005. LNCS, vol.\u00a03461, pp. 39\u201354. Springer, Heidelberg (2005)"},{"issue":"4","key":"2_CR2","doi-asserted-by":"publisher","first-page":"647","DOI":"10.1145\/321479.321488","volume":"15","author":"A. Aho","year":"1968","unstructured":"Aho, A.: Indexed grammars \u2013 an extension of context-free grammars. J. ACM\u00a015(4), 647\u2013671 (1968)","journal-title":"J. ACM"},{"key":"2_CR3","doi-asserted-by":"crossref","unstructured":"Barendregt, H.: The type free lambda calculus. In: Barwise, J. (ed.) Handbook of Mathematical Logic, ch. D.7, pp. 1091\u20131132. North Holland (1977)","DOI":"10.1016\/S0049-237X(08)71129-7"},{"key":"2_CR4","unstructured":"Barendregt, H.: The Lambda Calculus, Its Syntax and Semantics. Studies in Logic and the Foundations of Mathematics, vol.\u00a0103. Elsevier (1985)"},{"issue":"5","key":"2_CR5","doi-asserted-by":"publisher","first-page":"559","DOI":"10.1016\/j.ic.2008.09.003","volume":"207","author":"H. Barendregt","year":"2009","unstructured":"Barendregt, H., Klop, J.W.: Applications of infinitary lambda calculus. Inf. Comput.\u00a0207(5), 559\u2013582 (2009)","journal-title":"Inf. Comput."},{"key":"2_CR6","doi-asserted-by":"crossref","unstructured":"Carayol, A., Serre, O.: Collapsible pushdown automata and labeled recursion schemes equivalence, safety and effective selection. In: LICS, pp. 165\u2013174 (2012)","DOI":"10.1109\/LICS.2012.73"},{"key":"2_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"112","DOI":"10.1007\/978-3-540-24597-1_10","volume-title":"FST TCS 2003: Foundations of Software Technology and Theoretical Computer Science","author":"A. Carayol","year":"2003","unstructured":"Carayol, A., W\u00f6hrle, S.: The Caucal Hierarchy of Infinite Graphs in Terms of Logic and Higher-Order Pushdown Automata. In: Pandya, P.K., Radhakrishnan, J. (eds.) FSTTCS 2003. LNCS, vol.\u00a02914, pp. 112\u2013123. Springer, Heidelberg (2003)"},{"key":"2_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"165","DOI":"10.1007\/3-540-45687-2_13","volume-title":"Mathematical Foundations of Computer Science 2002","author":"D. Caucal","year":"2002","unstructured":"Caucal, D.: On Infinite Terms Having a Decidable Monadic Theory. In: Diks, K., Rytter, W. (eds.) MFCS 2002. LNCS, vol.\u00a02420, pp. 165\u2013176. Springer, Heidelberg (2002)"},{"issue":"2","key":"2_CR9","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1016\/0304-3975(82)90009-3","volume":"20","author":"W. Damm","year":"1982","unstructured":"Damm, W.: The IO\u2013 and OI\u2013hierarchies. Theoretical Computer Science\u00a020(2), 95\u2013208 (1982)","journal-title":"Theoretical Computer Science"},{"key":"2_CR10","doi-asserted-by":"crossref","unstructured":"Dezani-Ciancaglini, M., Giovannetti, E., de\u2019 Liguoro, U.: Intersection Types, Lambda-models and B\u00f6hm Trees. In: MSJ-Memoir. Theories of Types and Proofs, vol.\u00a02, pp. 45\u201397. Mathematical Society of Japan (1998)","DOI":"10.2969\/msjmemoirs\/00201C020"},{"key":"2_CR11","doi-asserted-by":"crossref","unstructured":"Hague, M., Murawski, A.S., Ong, C.-H.L., Serre, O.: Collapsible pushdown automata and recursion schemes. In: LICS 2008, pp. 452\u2013461. IEEE Computer Society (2008)","DOI":"10.1109\/LICS.2008.34"},{"key":"2_CR12","first-page":"82","volume-title":"Problems of Cybernetics I","author":"Y. Ianov","year":"1969","unstructured":"Ianov, Y.: The logical schemes of algorithms. In: Problems of Cybernetics I, pp. 82\u2013140. Pergamon, Oxford (1969)"},{"key":"2_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"352","DOI":"10.1007\/3-540-07854-1_198","volume-title":"Mathematical Foundations of Computer Science 1976","author":"K. Indermark","year":"1976","unstructured":"Indermark, K.: Schemes with Recursion on Higher Types. In: Mazurkiewicz, A. (ed.) MFCS 1976. LNCS, vol.\u00a045, pp. 352\u2013358. Springer, Heidelberg (1976)"},{"key":"2_CR14","unstructured":"Kfoury, A., Urzyczyn, P.: Finitely typed functional programs, Part II: comparisons to imperative languages. Technical report, Boston University (1988)"},{"key":"2_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"205","DOI":"10.1007\/3-540-45931-6_15","volume-title":"Foundations of Software Science and Computation Structures","author":"T. Knapik","year":"2002","unstructured":"Knapik, T., Niwi\u0144ski, D., Urzyczyn, P.: Higher-Order Pushdown Trees Are Easy. In: Nielsen, M., Engberg, U. (eds.) FOSSACS 2002. LNCS, vol.\u00a02303, pp. 205\u2013222. Springer, Heidelberg (2002)"},{"key":"2_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1450","DOI":"10.1007\/11523468_117","volume-title":"Automata, Languages and Programming","author":"T. Knapik","year":"2005","unstructured":"Knapik, T., Niwi\u0144ski, D., Urzyczyn, P., Walukiewicz, I.: Unsafe Grammars and Panic Automata. In: Caires, L., Italiano, G.F., Monteiro, L., Palamidessi, C., Yung, M. (eds.) ICALP 2005. LNCS, vol.\u00a03580, pp. 1450\u20131461. Springer, Heidelberg (2005)"},{"key":"2_CR17","doi-asserted-by":"crossref","unstructured":"Kobayashi, N.: Types and higher-order recursion schemes for verification of higher-order programs. In: POPL 2009, pp. 416\u2013428. ACM (2009)","DOI":"10.1145\/1594834.1480933"},{"issue":"3","key":"2_CR18","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1007\/s10990-007-9018-9","volume":"20","author":"J.-L. Krivine","year":"2007","unstructured":"Krivine, J.-L.: A call-by-name lambda-calculus machine. Higher-Order and Symbolic Computation\u00a020(3), 199\u2013207 (2007)","journal-title":"Higher-Order and Symbolic Computation"},{"key":"2_CR19","first-page":"1170","volume":"15","author":"A. Maslov","year":"1974","unstructured":"Maslov, A.: The hierarchy of indexed languages of an arbitrary level. Soviet Math. Doklady\u00a015, 1170\u20131174 (1974)","journal-title":"Soviet Math. Doklady"},{"key":"2_CR20","first-page":"38","volume":"12","author":"A. Maslov","year":"1976","unstructured":"Maslov, A.: Multilevel stack automata. Problems of Information Transmission\u00a012, 38\u201343 (1976)","journal-title":"Problems of Information Transmission"},{"key":"2_CR21","doi-asserted-by":"crossref","unstructured":"Milner, R.: Models of LCF. Memo AIM-186. Stanford University (1973)","DOI":"10.21236\/AD0758645"},{"key":"2_CR22","doi-asserted-by":"crossref","unstructured":"Ong, C.-H.L.: On model-checking trees generated by higher-order recursion schemes. In: LICS 2006, pp. 81\u201390 (2006)","DOI":"10.1109\/LICS.2006.38"},{"key":"2_CR23","doi-asserted-by":"crossref","unstructured":"Parys, P.: On the significance of the collapse operation. In: LICS 2012 (2012)","DOI":"10.1109\/LICS.2012.62"},{"issue":"3","key":"2_CR24","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1016\/0304-3975(77)90044-5","volume":"5","author":"G.D. Plotkin","year":"1977","unstructured":"Plotkin, G.D.: LCF considered as a programming language. Theor. Comput. Sci.\u00a05(3), 223\u2013255 (1977)","journal-title":"Theor. Comput. Sci."},{"key":"2_CR25","unstructured":"Salvati, S., Walukiewicz, I.: Recursive Schemes, Krivine Machines, and Collapsible Pushdown Automata. HAL Report, hal-00717718 (2012), http:\/\/hal.archives-ouvertes.fr\/hal-00717718"}],"container-title":["Lecture Notes in Computer Science","Reachability Problems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-33512-9_2.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,8]],"date-time":"2025-04-08T01:51:52Z","timestamp":1744077112000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-33512-9_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642335112","9783642335129"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-33512-9_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}