{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,26]],"date-time":"2026-05-26T23:05:11Z","timestamp":1779836711041,"version":"3.53.1"},"reference-count":61,"publisher":"Cambridge University Press (CUP)","license":[{"start":{"date-parts":[[2022,7,5]],"date-time":"2022-07-05T00:00:00Z","timestamp":1656979200000},"content-version":"unspecified","delay-in-days":185,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["cambridge.org"],"crossmark-restriction":true},"short-container-title":["J. Funct. Prog."],"published-print":{"date-parts":[[2022]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    A standard informal method for analyzing the asymptotic complexity of a program is to extract a recurrence that describes its cost in terms of the size of its input and then to compute a closed-form upper bound on that recurrence. We give a formal account of that method for functional programs in a higher order language with\n                    <jats:inline-formula>\n                      <jats:alternatives>\n                        <jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"png\" xlink:href=\"S095679682200003X_inline1.png\"\/>\n                        <jats:tex-math>$\\mathtt{let}$<\/jats:tex-math>\n                      <\/jats:alternatives>\n                    <\/jats:inline-formula>\n                    -polymorphism. The method consists of two phases. In the first phase, a monadic translation is performed to extract a cost-annotated version of the original program. In the second phase, the extracted program is interpreted in a model. The key feature of this second phase is that different models describe different notions of size. This plays out in several ways. For example, when analyzing functions that take arguments of inductive types, different notions of size may be appropriate depending on the analysis. When analyzing polymorphic functions, our approach shows that one can formally describe the notion of size of an argument in terms of the data that is common to the notions of size for each type instance of the domain type. We give several examples of different models that formally justify various informal cost analyses to show the applicability of our approach.\n                  <\/jats:p>","DOI":"10.1017\/s095679682200003x","type":"journal-article","created":{"date-parts":[[2022,7,5]],"date-time":"2022-07-05T01:50:35Z","timestamp":1656985835000},"update-policy":"https:\/\/doi.org\/10.1017\/policypage","source":"Crossref","is-referenced-by-count":3,"title":["Denotational semantics as a foundation for cost recurrence extraction for functional languages"],"prefix":"10.1017","volume":"32","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-1119-4982","authenticated-orcid":false,"given":"NORMAN","family":"DANNER","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"DANIEL R.","family":"LICATA","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"56","published-online":{"date-parts":[[2022,7,5]]},"reference":[{"key":"S095679682200003X_ref44","volume-title":"Foundations for Programming Languages","author":"Mitchell","year":"1996"},{"key":"S095679682200003X_ref43","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2017.05.001"},{"key":"S095679682200003X_ref34","doi-asserted-by":"publisher","DOI":"10.1145\/237721.240882"},{"key":"S095679682200003X_ref41","doi-asserted-by":"publisher","DOI":"10.1145\/42190.42347"},{"key":"S095679682200003X_ref24","volume-title":"Introduction to Lattices and Order","author":"Davey","year":"1999"},{"key":"S095679682200003X_ref38","doi-asserted-by":"publisher","DOI":"10.1145\/3158142"},{"key":"S095679682200003X_ref33","doi-asserted-by":"publisher","DOI":"10.1145\/604131.604148"},{"key":"S095679682200003X_ref36","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-016-9398-9"},{"key":"S095679682200003X_ref15","doi-asserted-by":"publisher","DOI":"10.1145\/355616.361015"},{"key":"S095679682200003X_ref3","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2011.07.009"},{"key":"S095679682200003X_ref32","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-11957-6_16"},{"key":"S095679682200003X_ref14","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-017-9431-7"},{"key":"S095679682200003X_ref5","doi-asserted-by":"publisher","DOI":"10.1145\/2499937.2499943"},{"key":"S095679682200003X_ref37","doi-asserted-by":"publisher","DOI":"10.1145\/3371083"},{"key":"S095679682200003X_ref31","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009842"},{"key":"S095679682200003X_ref61","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-94205-6_35"},{"key":"S095679682200003X_ref50","unstructured":"Sands, D. (1990) Calculi for Time Analysis of Functional Programs. PhD thesis, University of London."},{"key":"S095679682200003X_ref28","doi-asserted-by":"publisher","DOI":"10.1145\/3371092"},{"key":"S095679682200003X_ref23","first-page":"0","article-title":"Adventures in time and space","volume":"30","author":"Danner","year":"2007","journal-title":"Logical Methods Comput. Sci."},{"key":"S095679682200003X_ref53","doi-asserted-by":"publisher","DOI":"10.1137\/0211062"},{"key":"S095679682200003X_ref55","doi-asserted-by":"publisher","DOI":"10.1145\/99370.99404"},{"key":"S095679682200003X_ref48","unstructured":"Raymond, J. (2016) Extracting Cost Recurrences from Sequential and Parallel Functional Programs. M.A. thesis, Wesleyan University."},{"key":"S095679682200003X_ref49","doi-asserted-by":"publisher","DOI":"10.1145\/99370.99381"},{"key":"S095679682200003X_ref12","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(90)90044-I"},{"key":"S095679682200003X_ref21","doi-asserted-by":"publisher","DOI":"10.1145\/2784731.2784749"},{"key":"S095679682200003X_ref51","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.57.7"},{"key":"S095679682200003X_ref4","doi-asserted-by":"publisher","DOI":"10.1145\/3274278"},{"key":"S095679682200003X_ref16","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"S095679682200003X_ref2","volume-title":"Non-well-founded Sets","author":"Aczel","year":"1988"},{"key":"S095679682200003X_ref54","unstructured":"Van Stone, K. (2003) A Denotational Approach to Measuring Complexity in Functional Programs. PhD thesis, School of Computer Science, Carnegie Mellon University."},{"key":"S095679682200003X_ref57","doi-asserted-by":"publisher","DOI":"10.1145\/3290326"},{"key":"S095679682200003X_ref59","first-page":"528","article-title":"Mechanical program analysis","volume":"180","author":"Wegbreit","year":"1975","journal-title":"Commun. Assoc. Comput. Mach."},{"key":"S095679682200003X_ref19","article-title":"Linear dependent types and relative completeness","volume":"80","author":"Dal Lago","year":"2011","journal-title":"Logical Methods Comput. Sci."},{"key":"S095679682200003X_ref1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796800000186"},{"key":"S095679682200003X_ref60","doi-asserted-by":"publisher","DOI":"10.1145\/292540.292560"},{"key":"S095679682200003X_ref42","volume-title":"Semantic Structures in Computation","author":"Levy","year":"2003"},{"key":"S095679682200003X_ref58","doi-asserted-by":"publisher","DOI":"10.1145\/3133903"},{"key":"S095679682200003X_ref56","doi-asserted-by":"publisher","DOI":"10.1145\/143165.143169"},{"key":"S095679682200003X_ref10","volume-title":"Honors thesis","author":"Barnaby","year":"2018"},{"key":"S095679682200003X_ref22","doi-asserted-by":"publisher","DOI":"10.1145\/2428116.2428123"},{"key":"S095679682200003X_ref27","doi-asserted-by":"publisher","DOI":"10.1145\/3341718"},{"key":"S095679682200003X_ref8","doi-asserted-by":"publisher","DOI":"10.1145\/2784731.2784753"},{"key":"S095679682200003X_ref13","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009858"},{"key":"S095679682200003X_ref17","doi-asserted-by":"publisher","DOI":"10.1145\/325694.325716"},{"key":"S095679682200003X_ref35","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706327"},{"key":"S095679682200003X_ref46","doi-asserted-by":"publisher","DOI":"10.1145\/3158124"},{"key":"S095679682200003X_ref25","unstructured":"Fisher, K. & Reppy, J. (eds). (2015) Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming."},{"key":"S095679682200003X_ref9","first-page":"613","article-title":"Can programming be liberated from the von Neumann style? A functional style and its algebra of programs","volume":"210","author":"Backus","year":"1978","journal-title":"Commun. Assoc. Comput. Mach."},{"key":"S095679682200003X_ref11","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2003.10.022"},{"key":"S095679682200003X_ref26","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89884-1_19"},{"key":"S095679682200003X_ref29","unstructured":"Hoffmann, J. (2020) Resource Aware ML. URL http:\/\/raml.co."},{"key":"S095679682200003X_ref39","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314602"},{"key":"S095679682200003X_ref47","doi-asserted-by":"publisher","DOI":"10.1145\/3434308"},{"key":"S095679682200003X_ref52","unstructured":"Shultis, J. On the complexity of higher-order programs. Technical Report CU-CS-288-85, University of Colorado at Boulder, 1985."},{"key":"S095679682200003X_ref7","doi-asserted-by":"publisher","DOI":"10.1145\/3110287"},{"key":"S095679682200003X_ref6","article-title":"Amortised resource analysis with separation logic","volume":"70","author":"Atkey","year":"2011","journal-title":"Logical Methods Comput. Sci."},{"key":"S095679682200003X_ref30","doi-asserted-by":"publisher","DOI":"10.1145\/2362389.2362393"},{"key":"S095679682200003X_ref40","doi-asserted-by":"publisher","DOI":"10.1145\/3408988"},{"key":"S095679682200003X_ref18","doi-asserted-by":"publisher","DOI":"10.1145\/3408979"},{"key":"S095679682200003X_ref45","article-title":"Purely Functional Data Structures","author":"Okasaki","year":"1998","journal-title":"Cambridge University Press."},{"key":"S095679682200003X_ref20","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328457"}],"container-title":["Journal of Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S095679682200003X","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,5,26]],"date-time":"2026-05-26T22:35:07Z","timestamp":1779834907000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S095679682200003X\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"references-count":61,"alternative-id":["S095679682200003X"],"URL":"https:\/\/doi.org\/10.1017\/s095679682200003x","relation":{},"ISSN":["0956-7968","1469-7653"],"issn-type":[{"value":"0956-7968","type":"print"},{"value":"1469-7653","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"\u00a9 The Author(s), 2022. Published by Cambridge University Press","name":"copyright","label":"Copyright","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}},{"value":"This is an Open Access article, distributed under the terms of the Creative Commons Attribution licence (https:\/\/creativecommons.org\/licenses\/by\/4.0\/), which permits unrestricted re-use, distribution, and reproduction in any medium, provided the original work is properly cited.","name":"license","label":"License","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}],"article-number":"e8"}}