{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T21:17:04Z","timestamp":1760044624234,"version":"3.37.3"},"reference-count":32,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2017,1,6]],"date-time":"2017-01-06T00:00:00Z","timestamp":1483660800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/501100004963","name":"Seventh Framework Programme","doi-asserted-by":"publisher","award":["288570"],"award-info":[{"award-number":["288570"]}],"id":[{"id":"10.13039\/501100004963","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100007601","name":"Horizon 2020","doi-asserted-by":"publisher","award":["644235"],"award-info":[{"award-number":["644235"]}],"id":[{"id":"10.13039\/501100007601","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001871","name":"Funda\u00e7\u00e3o para a Ci\u00eancia e a Tecnologia","doi-asserted-by":"publisher","award":["UID\/CEC\/00027\/2013"],"award-info":[{"award-number":["UID\/CEC\/00027\/2013"]}],"id":[{"id":"10.13039\/501100001871","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2017,6]]},"DOI":"10.1007\/s10817-016-9398-9","type":"journal-article","created":{"date-parts":[[2017,1,6]],"date-time":"2017-01-06T14:39:09Z","timestamp":1483713549000},"page":"87-120","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":16,"title":["Type-Based Cost Analysis for Lazy Functional Languages"],"prefix":"10.1007","volume":"59","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-1807-9357","authenticated-orcid":false,"given":"Steffen","family":"Jost","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8387-9772","authenticated-orcid":false,"given":"Pedro","family":"Vasconcelos","sequence":"additional","affiliation":[]},{"given":"M\u00e1rio","family":"Florido","sequence":"additional","affiliation":[]},{"given":"Kevin","family":"Hammond","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,1,6]]},"reference":[{"issue":"1\u20132","key":"9398_CR1","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1016\/j.tcs.2003.10.022","volume":"318","author":"R Benzinger","year":"2004","unstructured":"Benzinger, R.: Automated higher-order complexity analysis. Theor. Comput. Sci. 318(1\u20132), 79\u2013103 (2004)","journal-title":"Theor. Comput. Sci."},{"key":"9398_CR2","volume-title":"Introduction to Functional Programming","author":"R Bird","year":"1988","unstructured":"Bird, R., Wadler, P.: Introduction to Functional Programming. Prentice Hall, New York (1988)"},{"key":"9398_CR3","unstructured":"Coutts, D.: Stream fusion: practical shortcut fusion for coinductive sequence types. Ph.D. thesis, Worcester College, University of Oxford (2010)"},{"key":"9398_CR4","doi-asserted-by":"publisher","unstructured":"Danielsson, N.A.: Lightweight semiformal time complexity analysis for purely functional data structures. Proceedings of POPL 2008: 35th ACM SIGPLAN-SIGACT symposium on principles of programming languages. San Francisco, California, pp. 133\u2013144. ACM, San Francisco (2008)","DOI":"10.1145\/1328438.1328457"},{"key":"9398_CR5","doi-asserted-by":"publisher","unstructured":"Hoffmann, J., Aehlig, K., Hofmann, M.: Multivariate amortized resource analysis. In: 38th Symposium on Principles of Programming Languages (POPL\u201911), pp. 357\u2013370 (2011)","DOI":"10.1145\/1926385.1926427"},{"key":"9398_CR6","doi-asserted-by":"publisher","unstructured":"Hoffmann, J., Shao, Z.: Automatic static cost analysis for parallel programs. In: Proceedings of the 24th European Symposium on Programming (ESOP\u201915), pp. 132\u2013157. Springer (2015)","DOI":"10.1007\/978-3-662-46669-8_6"},{"key":"9398_CR7","doi-asserted-by":"publisher","first-page":"e17","DOI":"10.1017\/S0956796815000192","volume":"25","author":"J Hoffmann","year":"2015","unstructured":"Hoffmann, J., Shao, Z.: Type-based amortized resource analysis with integers and arrays. J. Funct. Program. 25, e17 (2015)","journal-title":"J. Funct. Program."},{"key":"9398_CR8","doi-asserted-by":"publisher","unstructured":"Hofmann, M., Jost, S.: Static prediction of heap space usage for first-order functional programs. In: Proceedings of the 30th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pp. 185\u2013197. ACM, ACM Press, New Orleans (2003)","DOI":"10.1145\/604131.604148"},{"issue":"2","key":"9398_CR9","first-page":"98","volume":"32","author":"J Hughes","year":"1989","unstructured":"Hughes, J.: Why functional programming matters. Comput. J. 32(2), 98\u2013107 (1989)","journal-title":"Why functional programming matters. Comput. J."},{"key":"9398_CR10","doi-asserted-by":"publisher","unstructured":"Hughes, J., Pareto, L.: Recursion and dynamic data structures in bounded space: towards embedded ML programming. In: Proceedings of 1999 ACM International Conference on Functional Programming (ICFP\u00a0\u201999), ACM Sigplan Notices, vol.\u00a034, pp. 70\u201381. ACM Press (1999)","DOI":"10.1145\/317636.317785"},{"key":"9398_CR11","unstructured":"Jost, S.: Automated Amortised Analysis. Ph.D. thesis, LMU Munich"},{"key":"9398_CR12","doi-asserted-by":"publisher","unstructured":"Jost, S., Loidl, H.W., Hammond, K., Hofmann, M.: Static determination of quantitative resource usage for higher-order programs. In: Proceedings of ACM Symposium on Principles of Programming Languages (POPL), pp. 223\u2013236 (2010)","DOI":"10.1145\/1706299.1706327"},{"key":"9398_CR13","doi-asserted-by":"publisher","unstructured":"Jost, S., Loidl, H.W., Hammond, K., Scaife, N., Hofmann, M.: \u201cCarbon Credits\u201d for resource-bounded computations using amortised analysis. In: Cavalcanti, A., Dams, D.R. (eds.) FM 2009: Formal Methods. Lecture Notes in Computer Science, vol. 5850, pp. 354\u2013369. Springer, Heidelberg (2009)","DOI":"10.1007\/978-3-642-05089-3_23"},{"key":"9398_CR14","doi-asserted-by":"publisher","unstructured":"La Encina, A., Pe\u00f1a, R.: Proving the correctness of the STG machine. In: Proceedings of IFL\u00a0\u201901: Implementation of Functional Programming Languages, Stockholm, Sweden, Sept. 24\u201326, 2001, pp. 88\u2013104. Springer LNCS 2312 (2002)","DOI":"10.1007\/3-540-46028-4_6"},{"key":"9398_CR15","doi-asserted-by":"publisher","unstructured":"Launchbury, J.: A natural semantics for lazy evaluation. In: Proceedings of POPL \u201993: Symposium on Principles of Programming Languages, pp. 144\u2013154 (1993)","DOI":"10.1145\/158511.158618"},{"key":"9398_CR16","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511530104","volume-title":"Purely Functional Data Structures","author":"C Okasaki","year":"1998","unstructured":"Okasaki, C.: Purely Functional Data Structures. Cambridge University Press, Cambridge (1998)"},{"key":"9398_CR17","unstructured":"Peyton Jones, S., Marlow, S., Reid, A.: The STG runtime system (revised). Draft paper, Microsoft Research Ltd (1999)"},{"key":"9398_CR18","unstructured":"Peyton Jones, S., Augustsson, L., Boutel, B., Burton, F., Fasel, J., Gordon, A., Hammond, K., Hughes, R., Hudak, P., Johnsson, T., Jones, M., Peterson, J., Reid, A., Wadler, P. (eds.): Report on the Non-Strict Functional Language, Haskell (Haskell98). Technical report, Yale University (1999)"},{"key":"9398_CR19","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/1104.001.0001","volume-title":"Advanced Topics in Types and Programming Languages","author":"BC Pierce","year":"2004","unstructured":"Pierce, B.C.: Advanced Topics in Types and Programming Languages. MIT Press, Cambridge (2004)"},{"key":"9398_CR20","doi-asserted-by":"publisher","unstructured":"Reistad, B., Gifford, D.: Static dependent costs for estimating execution time. In: Proceedings of ACM Conference on Lisp and Functional Programming, pp. 65\u201378. ACM Press, Orlando, Florida, June 27\u201329 (1994)","DOI":"10.1145\/182409.182439"},{"key":"9398_CR21","unstructured":"Sands, D.: Calculi for Time Analysis of Functional Programs. Ph.D. thesis, Imperial College, University of London (1990)"},{"key":"9398_CR22","doi-asserted-by":"crossref","unstructured":"Sands, D.: Complexity analysis for a lazy higher-order language. In: Proceedings of ESOP \u201990: European Symposium on Programming, Copenhagen, Denmark, Springer LNCS 432, pp. 361\u2013376 (1990)","DOI":"10.1007\/3-540-52592-0_74"},{"issue":"3","key":"9398_CR23","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1017\/S0956796897002712","volume":"7","author":"P Sestoft","year":"1997","unstructured":"Sestoft, P.: Deriving a lazy abstract machine. J. Funct. Program. 7(3), 231\u2013264 (1997)","journal-title":"J. Funct. Program."},{"key":"9398_CR24","doi-asserted-by":"publisher","unstructured":"Sim\u00f5es, H., Jost, S., Vasconcelos, P., Florido, M., Hammond, K.: Automatic amortised analysis of dynamic memory allocation for lazy functional programs. In: Proceedings of the 17th ACM SIGPLAN International Conference on Functional Programming (ICFP\u201912), pp. 165\u2013176. ACM (2012)","DOI":"10.1145\/2364527.2364575"},{"key":"9398_CR25","doi-asserted-by":"publisher","unstructured":"Talpin, J.P., Jouvelot, P.: The type and effect discipline. In: Scedrov, A. (ed.) Proceedings of 1992 Logics in Computer Science Conference, vol. 111, pp. 245\u2013271. IEEE (1992)","DOI":"10.1109\/LICS.1992.185530"},{"issue":"2","key":"9398_CR26","doi-asserted-by":"publisher","first-page":"306","DOI":"10.1137\/0606031","volume":"6","author":"RE Tarjan","year":"1985","unstructured":"Tarjan, R.E.: Amortized computational complexity. SIAM J. Algebraic Discrete Methods 6(2), 306\u2013318 (1985)","journal-title":"SIAM J. Algebraic Discrete Methods"},{"issue":"2","key":"9398_CR27","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1006\/inco.1996.2613","volume":"132","author":"M Tofte","year":"1997","unstructured":"Tofte, M., Talpin, J.P.: Region-based memory management. Inf. Comput. 132(2), 109\u2013176 (1997)","journal-title":"Inf. Comput."},{"key":"9398_CR28","unstructured":"Vasconcelos, P.B.: Space cost analysis using sized types. Ph.D. thesis, School of Computer Science, University of St Andrews (2008)"},{"key":"9398_CR29","doi-asserted-by":"publisher","unstructured":"Vasconcelos, P.B., Jost, S., Florido, M., Hammond, K.: Type-based allocation analysis for co-recursion in lazy functional languages. In: Programming Languages and Systems: Proceedings of 24th European Symposium on Programming, ESOP 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11\u201318, pp. 787\u2013811 (2015)","DOI":"10.1007\/978-3-662-46669-8_32"},{"key":"9398_CR30","doi-asserted-by":"publisher","unstructured":"Wadler, P.: Strictness analysis aids time analysis. In: Proceedings of POPL\u00a0\u201988: ACM Symposium on Principles of Programming Languages, pp. 119\u2013132 (1988)","DOI":"10.1145\/73560.73571"},{"key":"9398_CR31","doi-asserted-by":"publisher","unstructured":"Wadler, P.: The essence of functional programming. In: Proceedings of POPL \u201992: ACM Symposium on Principles of Programming Languages, pp. 1\u201314 (1992)","DOI":"10.1145\/143165.143169"},{"key":"9398_CR32","doi-asserted-by":"publisher","unstructured":"Wadler, P., Hughes, J.: Projections for strictness analysis. In: Proceedings of FPCA\u201987: International Conference on Functional Programming Language and Computer Architecture, Springer LNCS 274, pp. 385\u2013407 (1987)","DOI":"10.1007\/3-540-18317-5_21"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-016-9398-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-016-9398-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-016-9398-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,17]],"date-time":"2019-09-17T03:15:15Z","timestamp":1568690115000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-016-9398-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,1,6]]},"references-count":32,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2017,6]]}},"alternative-id":["9398"],"URL":"https:\/\/doi.org\/10.1007\/s10817-016-9398-9","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2017,1,6]]}}}