{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,3]],"date-time":"2025-05-03T04:02:22Z","timestamp":1746244942624,"version":"3.40.4"},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642548291"},{"type":"electronic","value":"9783642548307"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-642-54830-7_10","type":"book-chapter","created":{"date-parts":[[2014,3,21]],"date-time":"2014-03-21T13:30:31Z","timestamp":1395408631000},"page":"149-163","source":"Crossref","is-referenced-by-count":5,"title":["Unsafe Order-2 Tree Languages Are Context-Sensitive"],"prefix":"10.1007","author":[{"given":"Naoki","family":"Kobayashi","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kazuhiro","family":"Inaba","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Takeshi","family":"Tsukada","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"10_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"490","DOI":"10.1007\/978-3-540-31982-5_31","volume-title":"Foundations of Software Science and Computational Structures","author":"K. Aehlig","year":"2005","unstructured":"Aehlig, K., de Miranda, J.G., Ong, C.-H.L.: Safety is not a restriction at level 2 for string languages. In: Sassone, V. (ed.) FOSSACS 2005. LNCS, vol.\u00a03441, pp. 490\u2013504. Springer, Heidelberg (2005)"},{"unstructured":"Curry, H.B., Feys, R.: Combinatory Logic, vol.\u00a01. North-Holland (1958)","key":"10_CR2"},{"key":"10_CR3","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- and OI-hierarchies. Theor. Comput. Sci.\u00a020, 95\u2013207 (1982)","journal-title":"Theor. Comput. Sci."},{"doi-asserted-by":"crossref","unstructured":"Haddad, A.: IO vs OI in higher-order recursion schemes. In: Proceedings of FICS 2012. EPTCS, vol.\u00a077, pp. 23\u201330 (2012)","key":"10_CR4","DOI":"10.4204\/EPTCS.77.4"},{"unstructured":"Haddad, A.: Model checking and functional program transformations. In: Proceedings of FSTTCS 2013. LIPIcs, vol.\u00a024, pp. 115\u2013126 (2013)","key":"10_CR5"},{"unstructured":"Inaba, K., Maneth, S.: The complexity of tree transducer output languages. In: Proceedings of FSTTCS 2008. LIPIcs, vol.\u00a02, pp. 244\u2013255 (2008)","key":"10_CR6"},{"key":"10_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"566","DOI":"10.1007\/978-3-642-32589-2_50","volume-title":"Mathematical Foundations of Computer Science 2012","author":"A. Kartzow","year":"2012","unstructured":"Kartzow, A., Parys, P.: Strictness of the collapsible pushdown hierarchy. In: Rovan, B., Sassone, V., Widmayer, P. (eds.) MFCS 2012. LNCS, vol.\u00a07464, pp. 566\u2013577. Springer, Heidelberg (2012)"},{"key":"10_CR8","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)"},{"doi-asserted-by":"crossref","unstructured":"Kobayashi, N.: Model checking higher-order programs. Journal of the ACM 60(3) (2013)","key":"10_CR9","DOI":"10.1145\/2487241.2487246"},{"doi-asserted-by":"crossref","unstructured":"Kobayashi, N.: Pumping by typing. In: Proceedings of LICS 2013, pp. 398\u2013407. IEEE Computer Society (2013)","key":"10_CR10","DOI":"10.1109\/LICS.2013.46"},{"unstructured":"Kobayashi, N., Inaba, K., Tsukada, T.: On unsafe tree and leaf languages (2014) (in preparation)","key":"10_CR11"},{"doi-asserted-by":"crossref","unstructured":"Kobayashi, N., Ong, C.-H.L.: A type system equivalent to the modal mu-calculus model checking of higher-order recursion schemes. In: Proceedings of LICS 2009, pp. 179\u2013188. IEEE Computer Society (2009)","key":"10_CR12","DOI":"10.1109\/LICS.2009.29"},{"doi-asserted-by":"crossref","unstructured":"Kobayashi, N., Sato, R., Unno, H.: Predicate abstraction and CEGAR for higher-order model checking. In: Proceedings of PLDI 2011, pp. 222\u2013233 (2011)","key":"10_CR13","DOI":"10.1145\/1993316.1993525"},{"key":"10_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"336","DOI":"10.1007\/978-3-642-39212-2_31","volume-title":"Automata, Languages, and Programming","author":"G.M. Kobele","year":"2013","unstructured":"Kobele, G.M., Salvati, S.: The IO and OI hierarchies revisited. In: Fomin, F.V., Freivalds, R., Kwiatkowska, M., Peleg, D. (eds.) ICALP 2013, Part II. LNCS, vol.\u00a07966, pp. 336\u2013348. Springer, Heidelberg (2013)"},{"key":"10_CR15","first-page":"1170","volume":"15","author":"A.N. Maslov","year":"1974","unstructured":"Maslov, A.N.: The hierarchy of indexed languages of an arbitrary level. Soviet Math. Dokl.\u00a015, 1170\u20131174 (1974)","journal-title":"Soviet Math. Dokl."},{"doi-asserted-by":"crossref","unstructured":"Ong, C.-H.L.: On model-checking trees generated by higher-order recursion schemes. In: Proceedings of LICS 2006, pp. 81\u201390. IEEE Computer Society (2006)","key":"10_CR16","DOI":"10.1109\/LICS.2006.38"},{"doi-asserted-by":"crossref","unstructured":"Ong, C.-H.L., Ramsay, S.: Verifying higher-order programs with pattern-matching algebraic data types. In: Proceedings of POPL 2011, pp. 587\u2013598 (2011)","key":"10_CR17","DOI":"10.1145\/1925844.1926453"},{"key":"10_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"358","DOI":"10.1007\/978-3-642-12032-9_25","volume-title":"Foundations of Software Science and Computational Structures","author":"M. Pagani","year":"2010","unstructured":"Pagani, M., della Rocca, S.R.: Solvability in resource lambda-calculus. In: Ong, L. (ed.) FOSSACS 2010. LNCS, vol.\u00a06014, pp. 358\u2013373. Springer, Heidelberg (2010)"},{"unstructured":"Turner, R.: An infinite hierarchy of term languages - an approach to mathematical complexity. In: Proceedings of ICALP, pp. 593\u2013608 (1972)","key":"10_CR19"},{"key":"10_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1007\/3-540-07142-3_84","volume-title":"Category Theory Applied to Computation and Control","author":"M. Wand","year":"1975","unstructured":"Wand, M.: An algebraic formulation of the Chomsky hierarchy. In: Manes, E.G. (ed.) Category Theory Applied to Computation and Control. LNCS, vol.\u00a025, pp. 209\u2013213. Springer, Heidelberg (1975)"}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Science and Computation Structures"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-54830-7_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,2]],"date-time":"2025-05-02T03:46:52Z","timestamp":1746157612000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-54830-7_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783642548291","9783642548307"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-54830-7_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}