{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T22:35:34Z","timestamp":1770330934496,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642171635","type":"print"},{"value":"9783642171642","type":"electronic"}],"license":[{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-17164-2_22","type":"book-chapter","created":{"date-parts":[[2010,11,19]],"date-time":"2010-11-19T05:54:39Z","timestamp":1290146079000},"page":"312-327","source":"Crossref","is-referenced-by-count":6,"title":["Verification of Tree-Processing Programs via Higher-Order Model Checking"],"prefix":"10.1007","author":[{"given":"Hiroshi","family":"Unno","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Naoshi","family":"Tabuchi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Naoki","family":"Kobayashi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"22_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)"},{"key":"22_CR2","first-page":"51","volume-title":"ICFP 2003","author":"V. Benzaken","year":"2003","unstructured":"Benzaken, V., Castagna, G., Frisch, A.: CDuce: an XML-centric general-purpose language. In: ICFP 2003, pp. 51\u201363. ACM, New York (2003)"},{"key":"22_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-44898-5_1","volume-title":"Static Analysis","author":"A.S. Christensen","year":"2003","unstructured":"Christensen, A.S., M\u00f8ller, A., Schwartzbach, M.I.: Precise analysis of string expressions. In: Cousot, R. (ed.) SAS 2003. LNCS, vol.\u00a02694, pp. 1\u201318. Springer, Heidelberg (2003)"},{"key":"22_CR4","unstructured":"Davies, R.: Practical refinement-type checking. Ph.D. thesis, Carnegie Mellon University, chair-Pfenning, Frank (2005)"},{"issue":"1","key":"22_CR5","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1016\/0022-0000(85)90066-2","volume":"31","author":"J. Engelfriet","year":"1985","unstructured":"Engelfriet, J., Vogler, H.: Macro tree transducers. Journal of Computer and System Sciences\u00a031(1), 71\u2013146 (1985)","journal-title":"Journal of Computer and System Sciences"},{"issue":"1\/2","key":"22_CR6","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1007\/BF02915449","volume":"26","author":"J. Engelfriet","year":"1988","unstructured":"Engelfriet, J., Vogler, H.: High level tree transducers and iterated pushdown tree transducers. Acta Informatica\u00a026(1\/2), 131\u2013192 (1988)","journal-title":"Acta Informatica"},{"key":"22_CR7","first-page":"268","volume-title":"PLDI 1991","author":"T. Freeman","year":"1991","unstructured":"Freeman, T., Pfenning, F.: Refinement types for ML. In: PLDI 1991, pp. 268\u2013277. ACM, New York (1991)"},{"issue":"1","key":"22_CR8","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1596527.1596529","volume":"32","author":"H. Hosoya","year":"2009","unstructured":"Hosoya, H., Frisch, A., Castagna, G.: Parametric polymorphism for XML. ACM Transactions on Programming Languages and Systems\u00a032(1), 1\u201356 (2009)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"issue":"2","key":"22_CR9","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1145\/767193.767195","volume":"3","author":"H. Hosoya","year":"2003","unstructured":"Hosoya, H., Pierce, B.C.: XDuce: A statically typed XML processing language. ACM Transactions on Internet Technology\u00a03(2), 117\u2013148 (2003)","journal-title":"ACM Transactions on Internet Technology"},{"key":"22_CR10","first-page":"11","volume-title":"ICFP 2000","author":"H. Hosoya","year":"2000","unstructured":"Hosoya, H., Vouillon, J., Pierce, B.C.: Regular expression types for XML. In: ICFP 2000, pp. 11\u201322. ACM, New York (2000)"},{"key":"22_CR11","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., Niwinski, 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":"22_CR12","first-page":"25","volume-title":"PPDP 2009","author":"N. Kobayashi","year":"2009","unstructured":"Kobayashi, N.: Model-checking higher-order functions. In: PPDP 2009, pp. 25\u201336. ACM, New York (2009)"},{"key":"22_CR13","first-page":"416","volume-title":"POPL 2009","author":"N. Kobayashi","year":"2009","unstructured":"Kobayashi, N.: Types and higher-order recursion schemes for verification of higher-order programs. In: POPL 2009, pp. 416\u2013428. ACM, New York (2009)"},{"key":"22_CR14","first-page":"179","volume-title":"LICS 2009","author":"N. Kobayashi","year":"2009","unstructured":"Kobayashi, N., Ong, C.-H.L.: A type system equivalent to the modal mu-calculus model checking of higher-order recursion schemes. In: LICS 2009, pp. 179\u2013188. IEEE, Los Alamitos (2009)"},{"key":"22_CR15","first-page":"495","volume-title":"POPL 2010","author":"N. Kobayashi","year":"2010","unstructured":"Kobayashi, N., Tabuchi, N., Unno, H.: Higher-order multi-parameter tree transducers and recursion schemes for program verification. In: POPL 2010, pp. 495\u2013508. ACM, New York (2010)"},{"key":"22_CR16","doi-asserted-by":"crossref","unstructured":"Kobayashi, N., Tabuchi, N., Unno, H.: Higher-order multi-parameter tree transducers and recursion schemes for program verification. An extended version (2010), http:\/\/www.kb.ecei.tohoku.ac.jp\/~koba\/papers\/hmtt.pdf","DOI":"10.1145\/1706299.1706355"},{"key":"22_CR17","first-page":"283","volume-title":"PODS 2005","author":"S. Maneth","year":"2005","unstructured":"Maneth, S., Berlea, A., Perst, T., Seidl, H.: XML type checking with macro tree transducers. In: PODS 2005, pp. 283\u2013294. ACM, New York (2005)"},{"issue":"1","key":"22_CR18","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1016\/S0022-0000(02)00030-2","volume":"66","author":"T. Milo","year":"2003","unstructured":"Milo, T., Suciu, D., Vianu, V.: Typechecking for XML transformers. Journal of Computer and System Sciences\u00a066(1), 66\u201397 (2003)","journal-title":"Journal of Computer and System Sciences"},{"key":"22_CR19","first-page":"432","volume-title":"WWW 2005","author":"Y. Minamide","year":"2005","unstructured":"Minamide, Y.: Static approximation of dynamically generated web pages. In: WWW 2005, pp. 432\u2013441. ACM, New York (2005)"},{"key":"22_CR20","first-page":"81","volume-title":"LICS 2006","author":"C.-H.L. Ong","year":"2006","unstructured":"Ong, C.-H.L.: On model-checking trees generated by higher-order recursion schemes. In: LICS 2006, pp. 81\u201390. IEEE, Los Alamitos (2006)"},{"key":"22_CR21","doi-asserted-by":"crossref","unstructured":"Schmidt, A., Waas, F., Kersten, M., Carey, M.J., Manolescu, I., Busse, R.: XMark: a benchmark for XML data management. In: VLDB 2002, pp. 974\u2013985. VLDB Endowment (2002)","DOI":"10.1016\/B978-155860869-6\/50096-2"},{"key":"22_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1007\/11737414_7","volume-title":"Functional and Logic Programming","author":"A. Tozawa","year":"2006","unstructured":"Tozawa, A.: XML type checking using high-level tree transducer. In: Hagiya, M., Wadler, P. (eds.) FLOPS 2006. LNCS, vol.\u00a03945, pp. 81\u201396. Springer, Heidelberg (2006)"},{"key":"22_CR23","doi-asserted-by":"crossref","unstructured":"Unno, H., Tabuchi, N., Kobayashi, N.: Verification of tree-processing programs via higher-order model checking. An extended version (2010), http:\/\/www.kb.ecei.tohoku.ac.jp\/~uhiro\/papers\/aplas2010.pdf","DOI":"10.1007\/978-3-642-17164-2_22"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-17164-2_22","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,6]],"date-time":"2019-06-06T07:18:10Z","timestamp":1559805490000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-17164-2_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642171635","9783642171642"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-17164-2_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010]]}}}