{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T09:29:58Z","timestamp":1770283798390,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642548291","type":"print"},{"value":"9783642548307","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-642-54830-7_12","type":"book-chapter","created":{"date-parts":[[2014,3,21]],"date-time":"2014-03-21T13:30:31Z","timestamp":1395408631000},"page":"180-194","source":"Crossref","is-referenced-by-count":6,"title":["Complexity of Model-Checking Call-by-Value Programs"],"prefix":"10.1007","author":[{"given":"Takeshi","family":"Tsukada","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Naoki","family":"Kobayashi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"3","key":"12_CR1","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1093\/logcom\/2.3.297","volume":"2","author":"J.-M. Andreoli","year":"1992","unstructured":"Andreoli, J.-M.: Logic programming with focusing proofs in linear logic. J. Log. Comput.\u00a02(3), 297\u2013347 (1992)","journal-title":"J. Log. Comput."},{"key":"12_CR2","unstructured":"Broadbent, C.H., Kobayashi, N.: Saturation-based model checking of higher-order recursion schemes. In: CSL 2013. LIPIcs, vol.\u00a023, pp. 129\u2013148, Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2013)"},{"key":"12_CR3","doi-asserted-by":"crossref","unstructured":"Davies, R., Pfenning, F.: Intersection types and computational effects. In: ICFP 2000, pp. 198\u2013208. ACM (2000)","DOI":"10.1145\/357766.351259"},{"issue":"1","key":"12_CR4","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1016\/0890-5401(91)90015-T","volume":"95","author":"J. Engelfriet","year":"1991","unstructured":"Engelfriet, J.: Iterated stack automata and complexity classes. Inf. Comput.\u00a095(1), 21\u201375 (1991)","journal-title":"Inf. Comput."},{"issue":"2","key":"12_CR5","doi-asserted-by":"publisher","first-page":"264","DOI":"10.1145\/1057387.1057390","volume":"27","author":"A. Igarashi","year":"2005","unstructured":"Igarashi, A., Kobayashi, N.: Resource usage analysis. ACM Trans. Program. Lang. Syst.\u00a027(2), 264\u2013313 (2005)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"12_CR6","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":"12_CR7","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":"12_CR8","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1145\/2487241.2487246","volume":"60","author":"N. Kobayashi","year":"2013","unstructured":"Kobayashi, N.: Model checking higher-order programs. J. ACM\u00a060(3), 20 (2013)","journal-title":"J. ACM"},{"key":"12_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 2009, pp. 179\u2013188. IEEE Computer Society (2009)","DOI":"10.1109\/LICS.2009.29"},{"key":"12_CR10","doi-asserted-by":"crossref","unstructured":"Kobayashi, N., Ong, C.-H.L.: Complexity of model checking recursion schemes for fragments of the modal mu-calculus. Logical Methods in Computer Science\u00a07(4) (2011)","DOI":"10.2168\/LMCS-7(4:9)2011"},{"key":"12_CR11","doi-asserted-by":"crossref","unstructured":"Kobayashi, N., Sato, R., Unno, H.: Predicate abstraction and CEGAR for higher-order model checking. In: PLDI 2011, pp. 222\u2013233. ACM (2011)","DOI":"10.1145\/1993316.1993525"},{"key":"12_CR12","doi-asserted-by":"crossref","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 (2010)","DOI":"10.1145\/1707801.1706355"},{"key":"12_CR13","doi-asserted-by":"publisher","first-page":"370","DOI":"10.1016\/S1571-0661(04)00022-2","volume":"1","author":"J. Maraist","year":"1995","unstructured":"Maraist, J., Odersky, M., Turner, D.N., Wadler, P.: Call-by-name, call-by-value, call-by-need and the linear lambda calculus. Electr. Notes Theor. Comput. Sci.\u00a01, 370\u2013392 (1995)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"12_CR14","doi-asserted-by":"publisher","first-page":"311","DOI":"10.1016\/S1571-0661(04)80969-1","volume":"45","author":"L.R. Nielsen","year":"2001","unstructured":"Nielsen, L.R.: A selective cps transformation. Electr. Notes Theor. Comput. Sci.\u00a045, 311\u2013331 (2001)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"12_CR15","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"},{"key":"12_CR16","doi-asserted-by":"crossref","unstructured":"Sato, R., Unno, H., Kobayashi, N.: Towards a scalable software model checker for higher-order programs. In: PEPM 2013, pp. 53\u201362. ACM (2013)","DOI":"10.1145\/2426890.2426900"},{"key":"12_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1007\/978-3-642-29822-6_22","volume-title":"Functional and Logic Programming","author":"Y. Tobita","year":"2012","unstructured":"Tobita, Y., Tsukada, T., Kobayashi, N.: Exact flow analysis by higher-order model checking. In: Schrijvers, T., Thiemann, P. (eds.) FLOPS 2012. LNCS, vol.\u00a07294, pp. 275\u2013289. Springer, Heidelberg (2012)"},{"issue":"2","key":"12_CR18","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1016\/0304-3975(95)00073-6","volume":"151","author":"S. Bakel van","year":"1995","unstructured":"van Bakel, S.: Intersection type assignment systems. Theor. Comput. Sci.\u00a0151(2), 385\u2013435 (1995)","journal-title":"Theor. Comput. Sci."},{"key":"12_CR19","doi-asserted-by":"crossref","unstructured":"Zeilberger, N.: Refinement types and computational duality. In: PLPV 2009, pp. 15\u201326. ACM (2009)","DOI":"10.1145\/1481848.1481852"}],"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_12","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_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783642548291","9783642548307"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-54830-7_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014]]}}}