{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T04:08:16Z","timestamp":1750133296106,"version":"3.41.0"},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662544570"},{"type":"electronic","value":"9783662544587"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-662-54458-7_4","type":"book-chapter","created":{"date-parts":[[2017,3,15]],"date-time":"2017-03-15T09:22:57Z","timestamp":1489569777000},"page":"53-68","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Almost Every Simply Typed $$\\lambda $$-Term Has a Long $$\\beta $$-Reduction Sequence"],"prefix":"10.1007","author":[{"given":"Ryoma","family":"Sin\u2019ya","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kazuyuki","family":"Asada","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Naoki","family":"Kobayashi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Takeshi","family":"Tsukada","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,3,16]]},"reference":[{"issue":"3","key":"4_CR1","doi-asserted-by":"publisher","first-page":"1277","DOI":"10.2307\/2695106","volume":"66","author":"A Beckmann","year":"2001","unstructured":"Beckmann, A.: Exact bounds for lengths of reductions in typed lambda-calculus. J. Symb. Logic 66(3), 1277\u20131285 (2001)","journal-title":"J. Symb. Logic"},{"key":"4_CR2","doi-asserted-by":"crossref","unstructured":"David, R., Grygiel, K., Kozic, J., Raffalli, C., Theyssier, G., Zaionc, M.: Asymptotically almost all $$\\lambda $$-terms are strongly normalizing. Logical Method Comput. Sci. 9(2) (2013)","DOI":"10.2168\/LMCS-9(1:2)2013"},{"issue":"05","key":"4_CR3","doi-asserted-by":"publisher","first-page":"594","DOI":"10.1017\/S0956796813000178","volume":"23","author":"K Grygiel","year":"2013","unstructured":"Grygiel, K., Lescanne, P.: Counting and generating lambda terms. J. Funct. Program. 23(05), 594\u2013628 (2013)","journal-title":"J. Funct. Program."},{"key":"4_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1007\/978-3-662-49192-8_15","volume-title":"SOFSEM 2016: Theory and Practice of Computer Science","author":"M Bendkowski","year":"2016","unstructured":"Bendkowski, M., Grygiel, K., Lescanne, P., Zaionc, M.: A natural counting of lambda terms. In: Freivalds, R.M., Engels, G., Catania, B. (eds.) SOFSEM 2016. LNCS, vol. 9587, pp. 183\u2013194. Springer, Heidelberg (2016). doi:10.1007\/978-3-662-49192-8_15"},{"key":"4_CR5","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. 2303, pp. 205\u2013222. Springer, Heidelberg (2002). doi:10.1007\/3-540-45931-6_15"},{"key":"4_CR6","doi-asserted-by":"crossref","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 (2006)","DOI":"10.1109\/LICS.2006.38"},{"key":"4_CR7","doi-asserted-by":"crossref","unstructured":"Kobayashi, N.: Model-checking higher-order functions. In: Proceedings of PPDP 2009, pp. 25\u201336. ACM Press (2009)","DOI":"10.1145\/1599410.1599415"},{"key":"4_CR8","unstructured":"Broadbent, C.H., Kobayashi, N.: Saturation-based model checking of higher-order recursion schemes. In: Proceedings of CSL 2013, vol. 23, pp. 129\u2013148. LIPIcs (2013)"},{"key":"4_CR9","doi-asserted-by":"crossref","unstructured":"Ramsay, S., Neatherway, R., Ong, C.H.L.: An abstraction refinement approach to higher-order model checking. In: Proceedings of POpPL 2014 (2014)","DOI":"10.1145\/2535838.2535873"},{"key":"4_CR10","doi-asserted-by":"publisher","first-page":"416","DOI":"10.1145\/1594834.1480933","volume":"44","author":"N Kobayashi","year":"2009","unstructured":"Kobayashi, N.: Types and higher-order recursion schemes for verification of higher-order programs. ACM SIGPLAN Not. 44, 416\u2013428 (2009). ACM Press","journal-title":"ACM SIGPLAN Not."},{"key":"4_CR11","doi-asserted-by":"publisher","first-page":"222","DOI":"10.1145\/1993316.1993525","volume":"46","author":"N Kobayashi","year":"2011","unstructured":"Kobayashi, N., Sato, R., Unno, H.: Predicate abstraction and CEGAR for higher-order model checking. ACM SIGPLAN Not. 46, 222\u2013233 (2011). ACM Press","journal-title":"ACM SIGPLAN Not."},{"key":"4_CR12","doi-asserted-by":"publisher","first-page":"587","DOI":"10.1145\/1925844.1926453","volume":"46","author":"CHL Ong","year":"2011","unstructured":"Ong, C.H.L., Ramsay, S.: Verifying higher-order programs with pattern-matching algebraic data types. ACM SIGPLAN Not. 46, 587\u2013598 (2011). ACM Press","journal-title":"ACM SIGPLAN Not."},{"key":"4_CR13","doi-asserted-by":"crossref","unstructured":"Sato, R., Unno, H., Kobayashi, N.: Towards a scalable software model checker for higher-order programs. In: Proceedings of PEpPM 2013, pp. 53\u201362. ACM Press (2013)","DOI":"10.1145\/2426890.2426900"},{"key":"4_CR14","unstructured":"Terui, K.: Semantic evaluation, intersection types and complexity of simply typed lambda calculus. In: 23rd International Conference on Rewriting Techniques and Applications (RTA 2012), vol. 15, pp. 323\u2013338. LIPIcs, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2012)"},{"key":"4_CR15","doi-asserted-by":"crossref","unstructured":"Mairson, H.G.: Deciding ML typability is complete for deterministic exponential time. In: POPL, pp. 382\u2013401. ACM Press (1990)","DOI":"10.1145\/96709.96748"},{"key":"4_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"206","DOI":"10.1007\/3-540-52590-4_50","volume-title":"CAAP 1990","author":"AJ Kfoury","year":"1990","unstructured":"Kfoury, A.J., Tiuryn, J., Urzyczyn, P.: ML typability is dexptime-complete. In: Arnold, A. (ed.) CAAP 1990. LNCS, vol. 431, pp. 206\u2013220. Springer, Heidelberg (1990). doi:10.1007\/3-540-52590-4_50"},{"key":"4_CR17","unstructured":"Sin\u2019ya, R., Asada, K., Kobayashi, N., Tsukada, T.: Almost every simply typed $$\\lambda $$-term has a long $$\\beta $$-reduction sequence ( full version). http:\/\/www-kb.is.s.u-tokyo.ac.jp\/ryoma\/papers\/fossacs17full.pdf"},{"key":"4_CR18","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1145\/258916.258939","volume":"32","author":"N Heintze","year":"1997","unstructured":"Heintze, N., McAllester, D.: Linear-time subtransitive control flow analysis. ACM SIGPLAN Not. 32, 261\u2013272 (1997)","journal-title":"ACM SIGPLAN Not."},{"key":"4_CR19","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511801655","volume-title":"Analytic Combinatorics","author":"P Flajolet","year":"2009","unstructured":"Flajolet, P., Sedgewick, R.: Analytic Combinatorics, 1st edn. Cambridge University Press, New York (2009)","edition":"1"},{"key":"4_CR20","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511804106","volume-title":"Computational Complexity: A Conceptual Perspective","author":"O Goldreich","year":"2008","unstructured":"Goldreich, O.: Computational Complexity: A Conceptual Perspective. Cambridge University Press, Cambridge (2008)"}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Science and Computation Structures"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-54458-7_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,16]],"date-time":"2025-06-16T21:22:21Z","timestamp":1750108941000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-662-54458-7_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783662544570","9783662544587"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-54458-7_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]},"assertion":[{"value":"16 March 2017","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FoSSaCS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Foundations of Software Science and Computation Structures","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Uppsala","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Sweden","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2017","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24 April 2017","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 April 2017","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fossacs2017","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/www.etaps.org\/index.php\/2017\/fossacs","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}