{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T13:05:29Z","timestamp":1770296729598,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642120312","type":"print"},{"value":"9783642120329","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-12032-9_24","type":"book-chapter","created":{"date-parts":[[2010,3,8]],"date-time":"2010-03-08T01:07:56Z","timestamp":1268010476000},"page":"343-357","source":"Crossref","is-referenced-by-count":15,"title":["Untyped Recursion Schemes and Infinite Intersection Types"],"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":[{"key":"24_CR1","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":"24_CR2","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 Computer Society Press, Los Alamitos (2006)"},{"key":"24_CR3","doi-asserted-by":"crossref","unstructured":"Kobayashi, N.: Types and higher-order recursion schemes for verification of higher-order programs. In: Proceedings of ACM SIGPLAN\/SIGACT Symposium on Principles of Programming Languages, pp. 416\u2013428 (2009)","DOI":"10.1145\/1594834.1480933"},{"key":"24_CR4","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, pp. 495\u2013507 (2010)","DOI":"10.1145\/1706299.1706355"},{"key":"24_CR5","first-page":"179","volume-title":"Proceedings of 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: Proceedings of LICS 2009, pp. 179\u2013188. IEEE Computer Society Press, Los Alamitos (2009)"},{"issue":"2","key":"24_CR6","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":"24_CR7","doi-asserted-by":"crossref","unstructured":"Leivant, D.: Discrete polymorphism. In: LISP and Functional Programming, pp. 288\u2013297 (1990)","DOI":"10.1145\/91556.91675"},{"key":"24_CR8","volume-title":"Computation: Finite and infinite Machines","author":"M.L. Minsky","year":"1967","unstructured":"Minsky, M.L.: Computation: Finite and infinite Machines. Prentice-Hall, Englewood Cliffs (1967)"},{"key":"24_CR9","volume-title":"Proceedings of PPDP 2009","author":"N. Kobayashi","year":"2009","unstructured":"Kobayashi, N.: Model-checking higher-order functions. In: Proceedings of PPDP 2009. ACM Press, New York (2009)"},{"key":"24_CR10","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1016\/j.entcs.2005.06.014","volume":"136","author":"J.J. Hallett","year":"2005","unstructured":"Hallett, J.J., Kfoury, A.J.: Programming examples needing polymorphic recursion. Electr. Notes Theor. Comput. Sci.\u00a0136, 57\u2013102 (2005)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"24_CR11","first-page":"111","volume-title":"LICS","author":"T. Terauchi","year":"2006","unstructured":"Terauchi, T., Aiken, A.: On typability for rank-2 intersection types with polymorphic recursion. In: LICS, pp. 111\u2013122. IEEE Computer Society, Los Alamitos (2006)"},{"key":"24_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1007\/3-540-45413-6_21","volume-title":"Typed Lambda Calculi and Applications","author":"T. Knapik","year":"2001","unstructured":"Knapik, T., Niwinski, D., Urzyczyn, P.: Deciding monadic theories of hyperalgebraic trees. In: Abramsky, S. (ed.) TLCA 2001. LNCS, vol.\u00a02044, pp. 253\u2013267. Springer, Heidelberg (2001)"},{"key":"24_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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)"},{"issue":"2","key":"24_CR14","doi-asserted-by":"publisher","first-page":"285","DOI":"10.1016\/S0890-5401(03)00143-3","volume":"186","author":"M.M. Bonsangue","year":"2003","unstructured":"Bonsangue, M.M., Kok, J.N.: Infinite intersection types. Inf. Comput.\u00a0186(2), 285\u2013318 (2003)","journal-title":"Inf. Comput."},{"issue":"1-2","key":"24_CR15","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1016\/S0304-3975(98)00135-2","volume":"212","author":"A. Berarducci","year":"1999","unstructured":"Berarducci, A., Dezani-Ciancaglini, M.: Infinite lambda-calculus and types. Theor. Comput. Sci.\u00a0212(1-2), 29\u201375 (1999)","journal-title":"Theor. Comput. Sci."},{"key":"24_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"195","DOI":"10.1007\/978-3-540-78969-7_15","volume-title":"Functional and Logic Programming","author":"M. Tatsuta","year":"2008","unstructured":"Tatsuta, M.: Types for hereditary head normalizing terms. In: Garrigue, J., Hermenegildo, M.V. (eds.) FLOPS 2008. LNCS, vol.\u00a04989, pp. 195\u2013209. Springer, Heidelberg (2008)"},{"key":"24_CR17","first-page":"83","volume-title":"LICS","author":"M. Tatsuta","year":"2008","unstructured":"Tatsuta, M.: Types for hereditary permutators. In: LICS, pp. 83\u201392. IEEE Computer Society, Los Alamitos (2008)"}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Science and Computational Structures"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-12032-9_24.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,24]],"date-time":"2020-11-24T02:47:02Z","timestamp":1606186022000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-12032-9_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642120312","9783642120329"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-12032-9_24","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010]]}}}