{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T16:41:43Z","timestamp":1725727303967},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642389450"},{"type":"electronic","value":"9783642389467"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-38946-7_15","type":"book-chapter","created":{"date-parts":[[2013,5,27]],"date-time":"2013-05-27T01:30:38Z","timestamp":1369618238000},"page":"189-204","source":"Crossref","is-referenced-by-count":7,"title":["Using Models to Model-Check Recursive Schemes"],"prefix":"10.1007","author":[{"given":"Sylvain","family":"Salvati","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Igor","family":"Walukiewicz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"15_CR1","doi-asserted-by":"crossref","unstructured":"Aehlig, K.: A finite semantics of simply-typed lambda terms for infinite runs of automata. Logical Methods in Computer Science\u00a03(3) (2007)","DOI":"10.2168\/LMCS-3(3:1)2007"},{"key":"15_CR2","doi-asserted-by":"crossref","unstructured":"Amadio, R.M., Curien, P.-L.: Domains and Lambda-Calculi. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press (1998)","DOI":"10.1017\/CBO9780511983504"},{"key":"15_CR3","unstructured":"Barendregt, H.: The Lambda Calculus, Its Syntax and Semantics. Studies in Logic and the Foundations of Mathematics, vol.\u00a0103. North-Holland (1984)"},{"key":"15_CR4","doi-asserted-by":"crossref","unstructured":"Broadbent, C., Carayol, A., Ong, L., Serre, O.: Recursion schemes and logical reflection. In: LICS, pp. 120\u2013129 (2010)","DOI":"10.1109\/LICS.2010.40"},{"key":"15_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"165","DOI":"10.1007\/978-3-642-31585-5_18","volume-title":"Automata, Languages, and Programming","author":"C. Broadbent","year":"2012","unstructured":"Broadbent, C., Carayol, A., Hague, M., Serre, O.: A saturation method for collapsible pushdown systems. In: Czumaj, A., Mehlhorn, K., Pitts, A., Wattenhofer, R. (eds.) ICALP 2012, Part II. LNCS, vol.\u00a07392, pp. 165\u2013176. Springer, Heidelberg (2012)"},{"key":"15_CR6","volume-title":"Automata, Languages and Machines","author":"S. Eilenberg","year":"1974","unstructured":"Eilenberg, S.: Automata, Languages and Machines. Academic Press, New York (1974)"},{"key":"15_CR7","doi-asserted-by":"crossref","unstructured":"Haddad, A.: IO vs OI in higher-order recursion schemes. In: FICS. EPTCS, vol.\u00a077, pp. 23\u201330 (2012)","DOI":"10.4204\/EPTCS.77.4"},{"key":"15_CR8","doi-asserted-by":"crossref","unstructured":"Hague, M., Murawski, A.S., Ong, C.-H.L., Serre, O.: Collapsible pushdown automata and recursion schemes. In: LICS, pp. 452\u2013461 (2008)","DOI":"10.1109\/LICS.2008.34"},{"key":"15_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1007\/978-3-642-10622-4_2","volume-title":"Advances in Computer Science - ASIAN 2009. Information Security and Privacy","author":"N. Kobayashi","year":"2009","unstructured":"Kobayashi, N.: Higher-order program verification and language-based security. In: Datta, A. (ed.) ASIAN 2009. LNCS, vol.\u00a05913, pp. 17\u201323. Springer, Heidelberg (2009)"},{"key":"15_CR10","doi-asserted-by":"crossref","unstructured":"Kobayashi, N.: Types and higher-order recursion schemes for verification of higher-order programs. In: POPL, pp. 416\u2013428. ACM (2009)","DOI":"10.1145\/1594834.1480933"},{"key":"15_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/978-3-642-10672-9_2","volume-title":"Programming Languages and Systems","author":"N. Kobayashi","year":"2009","unstructured":"Kobayashi, N.: Types and recursion schemes for higher-order program verification. In: Hu, Z. (ed.) APLAS 2009. LNCS, vol.\u00a05904, pp. 2\u20133. Springer, Heidelberg (2009)"},{"key":"15_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"260","DOI":"10.1007\/978-3-642-19805-2_18","volume-title":"Foundations of Software Science and Computational Structures","author":"N. Kobayashi","year":"2011","unstructured":"Kobayashi, N.: A practical linear time algorithm for trivial automata model checking of higher-order recursion schemes. In: Hofmann, M. (ed.) FOSSACS 2011. LNCS, vol.\u00a06604, pp. 260\u2013274. Springer, Heidelberg (2011)"},{"key":"15_CR13","doi-asserted-by":"crossref","unstructured":"Kobayashi, N., Ong, L.: A type system equivalent to modal mu-calculus model checking of recursion schemes. In: LICS, pp. 179\u2013188 (2009)","DOI":"10.1109\/LICS.2009.29"},{"key":"15_CR14","unstructured":"Ong, C.-H.L.: On model-checking trees generated by higher-order recursion schemes. In: LICS, pp. 81\u201390 (2006)"},{"key":"15_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1007\/978-3-642-31585-5_31","volume-title":"Automata, Languages, and Programming","author":"C.-H.L. Ong","year":"2012","unstructured":"Ong, C.-H.L., Tsukada, T.: Two-level game semantics, intersection types, and recursion schemes. In: Czumaj, A., Mehlhorn, K., Pitts, A., Wattenhofer, R. (eds.) ICALP 2012, Part II. LNCS, vol.\u00a07392, pp. 325\u2013336. Springer, Heidelberg (2012)"},{"key":"15_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/978-3-642-31585-5_34","volume-title":"Automata, Languages, and Programming","author":"S. Salvati","year":"2012","unstructured":"Salvati, S., Manzonetto, G., Gehrke, M., Barendregt, H.: Loader and Urzyczyn are logically related. In: Czumaj, A., Mehlhorn, K., Pitts, A., Wattenhofer, R. (eds.) ICALP 2012, Part II. LNCS, vol.\u00a07392, pp. 364\u2013376. Springer, Heidelberg (2012)"},{"key":"15_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1007\/978-3-642-22012-8_12","volume-title":"Automata, Languages and Programming","author":"S. Salvati","year":"2011","unstructured":"Salvati, S., Walukiewicz, I.: Krivine machines and higher-order schemes. In: Aceto, L., Henzinger, M., Sgall, J. (eds.) ICALP 2011, Part II. LNCS, vol.\u00a06756, pp. 162\u2013173. Springer, Heidelberg (2011)"},{"key":"15_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"6","DOI":"10.1007\/978-3-642-33512-9_2","volume-title":"Reachability Problems","author":"S. Salvati","year":"2012","unstructured":"Salvati, S., Walukiewicz, I.: Recursive schemes, Krivine machines, and collapsible pushdown automata. In: Finkel, A., Leroux, J., Potapov, I. (eds.) RP 2012. LNCS, vol.\u00a07550, pp. 6\u201320. Springer, Heidelberg (2012)"},{"key":"15_CR19","unstructured":"Salvati, S., Walukiewicz, I.: Using models to model-check recursive schemes. Technical report, LaBRI (2012), \n                    \n                      http:\/\/hal.inria.fr\/hal-00741077"},{"key":"15_CR20","unstructured":"Terui, K.: Semantic evaluation, intersection types and complexity of simply typed lambda calculus. In: RTA. LIPIcs, vol.\u00a015, pp. 323\u2013338. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2012)"},{"key":"15_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/978-3-642-32589-2_6","volume-title":"Mathematical Foundations of Computer Science 2012","author":"I. Walukiewicz","year":"2012","unstructured":"Walukiewicz, I.: Simple models for recursive schemes. In: Rovan, B., Sassone, V., Widmayer, P. (eds.) MFCS 2012. LNCS, vol.\u00a07464, pp. 49\u201360. Springer, Heidelberg (2012)"}],"container-title":["Lecture Notes in Computer Science","Typed Lambda Calculi and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-38946-7_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,13]],"date-time":"2019-05-13T07:31:39Z","timestamp":1557732699000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-38946-7_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642389450","9783642389467"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-38946-7_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}