{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,19]],"date-time":"2026-06-19T18:11:13Z","timestamp":1781892673507,"version":"3.54.5"},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642334740","type":"print"},{"value":"9783642334757","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-33475-7_25","type":"book-chapter","created":{"date-parts":[[2012,9,8]],"date-time":"2012-09-08T06:43:09Z","timestamp":1347086589000},"page":"357-371","source":"Crossref","is-referenced-by-count":4,"title":["An Intersection Type System for Deterministic Pushdown Automata"],"prefix":"10.1007","author":[{"given":"Takeshi","family":"Tsukada","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Naoki","family":"Kobayashi","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"25_CR1","doi-asserted-by":"crossref","unstructured":"Alur, R., Madhusudan, P.: Visibly pushdown languages. In: Babai, L. (ed.) STOC, pp. 202\u2013211. ACM (2004)","DOI":"10.1145\/1007352.1007390"},{"issue":"3","key":"25_CR2","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1516512.1516518","volume":"56","author":"R. Alur","year":"2009","unstructured":"Alur, R., Madhusudan, P.: Adding nesting structure to words. J. ACM\u00a056(3), 1\u201343 (2009)","journal-title":"J. ACM"},{"issue":"1-2","key":"25_CR3","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1016\/S0304-3975(99)00113-9","volume":"230","author":"P.R.J. Asveld","year":"2000","unstructured":"Asveld, P.R.J., Nijholt, A.: The inclusion problem for some subclasses of context-free languages. Theor. Comput. Sci.\u00a0230(1-2), 247\u2013256 (2000)","journal-title":"Theor. Comput. Sci."},{"key":"25_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"120","DOI":"10.1007\/11779148_12","volume-title":"Developments in Language Theory","author":"D. Caucal","year":"2006","unstructured":"Caucal, D.: Synchronization of Pushdown Automata. In: Ibarra, O.H., Dang, Z. (eds.) DLT 2006. LNCS, vol.\u00a04036, pp. 120\u2013132. Springer, Heidelberg (2006)"},{"issue":"4","key":"25_CR5","doi-asserted-by":"publisher","first-page":"675","DOI":"10.1145\/322217.322224","volume":"27","author":"S.A. Greibach","year":"1980","unstructured":"Greibach, S.A., Friedman, E.P.: Superdeterministic PDAs: A subcase with a decidable inclusion problem. J. ACM\u00a027(4), 675\u2013700 (1980)","journal-title":"J. ACM"},{"key":"25_CR6","doi-asserted-by":"crossref","unstructured":"Kobayashi, N.: Model-checking higher-order functions. In: Porto, A., L\u00f3pez-Fraguas, F.J. (eds.) PPDP, pp. 25\u201336. ACM (2009)","DOI":"10.1145\/1599410.1599415"},{"key":"25_CR7","doi-asserted-by":"crossref","unstructured":"Kobayashi, N.: Types and higher-order recursion schemes for verification of higher-order programs. In: Shao, Z., Pierce, B.C. (eds.) POPL, pp. 416\u2013428. ACM (2009)","DOI":"10.1145\/1594834.1480933"},{"key":"25_CR8","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":"25_CR9","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: LICS, pp. 179\u2013188. IEEE Computer Society (2009)","DOI":"10.1109\/LICS.2009.29"},{"key":"25_CR10","doi-asserted-by":"crossref","unstructured":"Kobayashi, N., Sato, R., Unno, H.: Predicate abstraction and CEGAR for higher-order model checking. In: Hall, M.W., Padua, D.A. (eds.) PLDI, pp. 222\u2013233. ACM (2011)","DOI":"10.1145\/1993316.1993525"},{"key":"25_CR11","doi-asserted-by":"crossref","unstructured":"Kobayashi, N., Tabuchi, N., Unno, H.: Higher-order multi-parameter tree transducers and recursion schemes for program verification. In: Hermenegildo, M.V., Palsberg, J. (eds.) POPL, pp. 495\u2013508. ACM (2010)","DOI":"10.1145\/1707801.1706355"},{"key":"25_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"357","DOI":"10.1007\/11924661_22","volume-title":"Programming Languages and Systems","author":"Y. Minamide","year":"2006","unstructured":"Minamide, Y., Tozawa, A.: XML Validation for Context-Free Grammars. In: Kobayashi, N. (ed.) APLAS 2006. LNCS, vol.\u00a04279, pp. 357\u2013373. Springer, Heidelberg (2006)"},{"key":"25_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"426","DOI":"10.1007\/978-3-642-19805-2_29","volume-title":"Foundations of Software Science and Computational Structures","author":"A. M\u00f8ller","year":"2011","unstructured":"M\u00f8ller, A., Schwarz, M.: HTML Validation of Context-Free Languages. In: Hofmann, M. (ed.) FOSSACS 2011. LNCS, vol.\u00a06604, pp. 426\u2013440. Springer, Heidelberg (2011)"},{"key":"25_CR14","unstructured":"Murata, M.: Hedge automata: a formal model for XML schemata (1999), http:\/\/www.xml.gr.jp\/relax\/hedge_nice.html"},{"issue":"1","key":"25_CR15","first-page":"36","volume":"1","author":"V.T. Nguyen","year":"2008","unstructured":"Nguyen, V.T., Ogawa, M.: Alternate stacking technique revisited: Inclusion problem of superdeterministic pushdown automata. IPSJ Transactions on Programming\u00a01(1), 36\u201346 (2008)","journal-title":"IPSJ Transactions on Programming"},{"key":"25_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/978-3-540-74456-6_13","volume-title":"Mathematical Foundations of Computer Science 2007","author":"D. Nowotka","year":"2007","unstructured":"Nowotka, D., Srba, J.: Height-Deterministic Pushdown Automata. In: Ku\u010dera, L., Ku\u010dera, A. (eds.) MFCS 2007. LNCS, vol.\u00a04708, pp. 125\u2013134. Springer, Heidelberg (2007)"},{"key":"25_CR17","doi-asserted-by":"crossref","unstructured":"Ong, C.H.L.: On model-checking trees generated by higher-order recursion schemes. In: LICS, pp. 81\u201390. IEEE Computer Society (2006)","DOI":"10.1109\/LICS.2006.38"},{"issue":"6","key":"25_CR18","doi-asserted-by":"publisher","first-page":"565","DOI":"10.1016\/S0019-9958(68)90999-6","volume":"13","author":"C. Pair","year":"1968","unstructured":"Pair, C., Qu\u00e9r\u00e9, A.: D\u00e9finition et etude des bilangages r\u00e9guliers. Information and Control\u00a013(6), 565\u2013593 (1968)","journal-title":"Information and Control"},{"key":"25_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"343","DOI":"10.1007\/978-3-642-12032-9_24","volume-title":"Foundations of Software Science and Computational Structures","author":"T. Tsukada","year":"2010","unstructured":"Tsukada, T., Kobayashi, N.: Untyped Recursion Schemes and Infinite Intersection Types. In: Ong, L. (ed.) FOSSACS 2010. LNCS, vol.\u00a06014, pp. 343\u2013357. Springer, Heidelberg (2010)"},{"issue":"2","key":"25_CR20","first-page":"31","volume":"4","author":"T. Tsukada","year":"2011","unstructured":"Tsukada, T., Kobayashi, N.: A type-theoretic proof of the decidability of the language containment between context-free languages and superdeterministic languages. IPSJ Transactions on Programming\u00a04(2), 31\u201347 (2011) (in Japanese)","journal-title":"IPSJ Transactions on Programming"}],"container-title":["Lecture Notes in Computer Science","Theoretical Computer Science"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-33475-7_25","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,8]],"date-time":"2025-04-08T01:50:15Z","timestamp":1744077015000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-33475-7_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642334740","9783642334757"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-33475-7_25","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012]]}}}