{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T02:11:57Z","timestamp":1775873517166,"version":"3.50.1"},"reference-count":68,"publisher":"Cambridge University Press (CUP)","issue":"6","license":[{"start":{"date-parts":[[2022,3,16]],"date-time":"2022-03-16T00:00:00Z","timestamp":1647388800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["cambridge.org"],"crossmark-restriction":true},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2022,6]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>This article gives an overview of automatic amortized resource analysis (AARA), a technique for inferring symbolic resource bounds for programs at compile time. AARA has been introduced by Hofmann and Jost in 2003 as a type system for deriving linear worst-case bounds on the heap-space consumption of first-order functional programs with eager evaluation strategy. Since then AARA has been the subject of dozens of research articles, which extended the analysis to different resource metrics, other evaluation strategies, non-linear bounds, and additional language features. All these works preserved the defining characteristics of the original paper: local inference rules, which reduce bound inference to numeric (usually linear) optimization; a soundness proof with respect to an operational cost semantics; and the support of amortized analysis with the potential method.<\/jats:p>","DOI":"10.1017\/s0960129521000487","type":"journal-article","created":{"date-parts":[[2022,3,16]],"date-time":"2022-03-16T09:32:42Z","timestamp":1647423162000},"page":"729-759","update-policy":"https:\/\/doi.org\/10.1017\/policypage","source":"Crossref","is-referenced-by-count":18,"title":["Two decades of automatic amortized resource analysis"],"prefix":"10.1017","volume":"32","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-8326-0788","authenticated-orcid":false,"given":"Jan","family":"Hoffmann","sequence":"first","affiliation":[]},{"given":"Steffen","family":"Jost","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2022,3,16]]},"reference":[{"key":"S0960129521000487_ref20","unstructured":"Hoffmann, J. (2011). Types with Potential: Polynomial Resource Bounds via Automatic Amortized Analysis. Phd thesis, Ludwig-Maximilians-Universit\u00e4t M\u00fcnchen."},{"key":"S0960129521000487_ref41","unstructured":"Jost, S. (2010). Automated Amortised Analysis. Phd thesis, Faculty of Mathematics, Computer Science and Statistics, LMU Munich, Germany, September 2010."},{"key":"S0960129521000487_ref50","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17184-1_1"},{"key":"S0960129521000487_ref28","doi-asserted-by":"publisher","DOI":"10.1145\/346048.346051"},{"key":"S0960129521000487_ref5","doi-asserted-by":"crossref","unstructured":"Borgstr\u00f6m, J. , Dal Lago, U. , Gordon, A. D. and Szymczak, M. (2016). A lambda-calculus foundation for universal probabilistic programming. In: International Conference on Functional Programming (ICFP\u201916).","DOI":"10.1145\/2951913.2951942"},{"key":"S0960129521000487_ref37","first-page":"509","volume-title":"CONCUR\u201993","author":"Honda","year":"1993"},{"key":"S0960129521000487_ref43","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-05089-3_23"},{"key":"S0960129521000487_ref67","doi-asserted-by":"crossref","unstructured":"Wang, D. and Hoffmann, J. (2019). Type-guided worst-case input generation. In: 46th Symposium on Principles of Programming Languages (POPL\u201919).","DOI":"10.1145\/3290326"},{"key":"S0960129521000487_ref35","unstructured":"Hofmann, M. and Moser, G. (2018). Analysis of logarithmic amortised complexity. CoRR, abs\/1807.08242."},{"key":"S0960129521000487_ref11","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-017-9431-7"},{"key":"S0960129521000487_ref17","doi-asserted-by":"publisher","DOI":"10.1145\/113445.113468"},{"key":"S0960129521000487_ref32","doi-asserted-by":"crossref","unstructured":"Hofmann, M. and Jost, S. (2003). Static prediction of heap space usage for first-order functional programs. In: 30th ACM Symposium on Principals of Programming Languages (POPL\u201903).","DOI":"10.1145\/604131.604148"},{"key":"S0960129521000487_ref9","doi-asserted-by":"crossref","unstructured":"Carbonneaux, Q. , Hoffmann, J. , Reps, T. and Shao, Z. (2017). Automated resource analysis with Coq proof objects. In: 29th International Conference on Computer-Aided Verification (CAV\u201917).","DOI":"10.1007\/978-3-319-63390-9_4"},{"key":"S0960129521000487_ref15","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-65474-0_15"},{"key":"S0960129521000487_ref18","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139342131"},{"key":"S0960129521000487_ref57","doi-asserted-by":"publisher","DOI":"10.1145\/3158124"},{"key":"S0960129521000487_ref1","doi-asserted-by":"crossref","unstructured":"Atkey, R. (2010). Amortised resource analysis with separation logic. In: 19th European Symposium on Programming (ESOP\u201910).","DOI":"10.1007\/978-3-642-11957-6_6"},{"key":"S0960129521000487_ref38","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0053567"},{"key":"S0960129521000487_ref30","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503297"},{"key":"S0960129521000487_ref55","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511530104"},{"key":"S0960129521000487_ref59","unstructured":"Reynolds, J. C. (2002). Separation logic: A logic for shared mutable data structures. In: 17th Annual IEEE Symposium on Logic in Computer Science (LICS\u201902)."},{"key":"S0960129521000487_ref66","volume-title":"Advanced Topics in Types and Programming Languages","author":"Walker","year":"2002"},{"key":"S0960129521000487_ref53","doi-asserted-by":"crossref","unstructured":"Ngo, V. C. , Dehesa-Azuara, M. , Fredrikson, M. and Hoffmann, J. (2017). Verifying and synthesizing constant-resource implementations with types. In: 38th IEEE Symposium on Security and Privacy (S&P \u201917).","DOI":"10.1109\/SP.2017.53"},{"key":"S0960129521000487_ref34","first-page":"1","article-title":"Type-based analysis of logarithmic amortised complexity","author":"Hofmann","year":"2021","journal-title":"Mathematical Structures in Computer Science"},{"key":"S0960129521000487_ref65","doi-asserted-by":"crossref","unstructured":"Vasconcelos, P. B. , Jost, S. , Florido, M. and Hammond, K. (2015). Type-based allocation analysis for co-recursion in lazy functional languages. In: 24th European Symposium on Programming (ESOP\u201915).","DOI":"10.1007\/978-3-662-46669-8_32"},{"key":"S0960129521000487_ref64","doi-asserted-by":"publisher","DOI":"10.1137\/0606031"},{"key":"S0960129521000487_ref42","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706327"},{"key":"S0960129521000487_ref14","doi-asserted-by":"crossref","unstructured":"Das, A. , Hoffmann, J. and Pfenning, F. (2018). Work analysis with resource-aware session types. In: 33th ACM\/IEEE Symposium on Logic in Computer Science (LICS\u201918).","DOI":"10.1145\/3209108.3209146"},{"key":"S0960129521000487_ref49","volume-title":"Studies in proof theory","volume":"1","author":"Martin-L\u00f6f","year":"1984"},{"key":"S0960129521000487_ref27","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1999.782641"},{"key":"S0960129521000487_ref3","unstructured":"Bauer, S. and Hofmann, M. (2017). Decidable linear list constraints. In: Eiter, T. and Sands, D. (eds.) LPAR-21, 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Maun, Botswana, May 7\u201312, 2017, EPiC Series in Computing, vol. 46, EasyChair, 181\u2013199."},{"key":"S0960129521000487_ref25","doi-asserted-by":"crossref","unstructured":"Hoffmann, J. , Marmar, M. and Shao, Z. (2013). Quantitative reasoning for proving lock-freedom. In: 28th ACM\/IEEE Symposium on Logic in Computer Science (LICS\u201913).","DOI":"10.1109\/LICS.2013.18"},{"key":"S0960129521000487_ref26","doi-asserted-by":"crossref","unstructured":"Hoffmann, J. and Shao, Z. (2015). Automatic static cost analysis for parallel programs. In: 24th European Symposium on Programming (ESOP\u201915).","DOI":"10.1007\/978-3-662-46669-8_6"},{"key":"S0960129521000487_ref40","volume-title":"Diploma thesis","author":"Jost","year":"2002"},{"key":"S0960129521000487_ref8","doi-asserted-by":"crossref","unstructured":"Carbonneaux, Q. , Hoffmann, J. , Ramananandro, T. and Shao, Z. (2014). End-to-end verification of stack-space bounds for C programs. In: 35th Conference on Programming Language Design and Implementation (PLDI\u201914). Artifact submitted and approved.","DOI":"10.1145\/2594291.2594301"},{"key":"S0960129521000487_ref54","unstructured":"Niu, Y. and Hoffmann, J. (2018). Automatic space bound analysis for functional programs with garbage collection. In: 22nd International Conference on Logic for Programming Artificial Intelligence and Reasoning (LPAR\u201918)."},{"key":"S0960129521000487_ref62","unstructured":"Sim\u00f5es, H. R. (2014). Amortised Resource Analysis for Lazy Functional Programs. Phd thesis, Faculdade de Ci\u00eancias da Universidade do Porto."},{"key":"S0960129521000487_ref61","doi-asserted-by":"publisher","DOI":"10.1007\/BF01019462"},{"key":"S0960129521000487_ref52","doi-asserted-by":"crossref","unstructured":"Ngo, V. C. , Carbonneaux, Q. and Hoffmann, J. (2018). Bounded expectations: Resource analysis for probabilistic programs. In: 39th Conference on Programming Language Design and Implementation (PLDI\u201918).","DOI":"10.1145\/3192366.3192394"},{"key":"S0960129521000487_ref68","doi-asserted-by":"crossref","unstructured":"Wang, D. , Kahn, D. M. and Hoffmann, J. (2020). Raising expectations: Automating expected cost analysis with types. In: 25th International Conference on Functional Programming (ICFP\u201920).","DOI":"10.1145\/3408992"},{"key":"S0960129521000487_ref48","unstructured":"Lichtman, B. and Hoffmann, J. (2017). Arrays and references in resource aware ML. In: 2nd International Conference on Formal Structures for Computation and Deduction (FSCD\u201917)."},{"key":"S0960129521000487_ref63","doi-asserted-by":"crossref","unstructured":"Sim\u00f5es, H. R. , Vasconcelos, P. B. , Florido, M. , Jost, S. and Hammond, K. (2012). Automatic amortised analysis of dynamic memory allocation for lazy functional programs. In: 17th International Conference on Functional Programming (ICFP\u201912).","DOI":"10.1145\/2364527.2364575"},{"key":"S0960129521000487_ref31","doi-asserted-by":"publisher","DOI":"10.1016\/S0890-5401(03)00009-9"},{"key":"S0960129521000487_ref16","unstructured":"Embounded (2005\u20132008). EU Project No. IST-510255, https:\/\/cordis.europa.eu\/project\/id\/510255."},{"key":"S0960129521000487_ref44","unstructured":"Jost, S. , Loidl, H.-W. , Scaife, N. , Hammond, K. , Michaelson, G. and Hofmann, M. (2009b). Worst-case execution time analysis through types. In: 21st Euromicro Conference on Real-Time Systems (ECRTS\u201909), ACM, 13\u201316. Work-in-Progress Session."},{"key":"S0960129521000487_ref19","unstructured":"Hammond, K. , Dyckhoff, R. , Ferdinand, C. , Heckmann, R. , Hofmann, M. , Loidl, H.-W. , Michaelson, G. , S\u00e9rot, J. and Wallace, A. (2006). The EmBounded project: Automatic prediction of resource bounds for embedded systems. In: Trends in Functional Programming, vol. 6."},{"key":"S0960129521000487_ref33","doi-asserted-by":"crossref","unstructured":"Hofmann, M. and Jost, S. (2006). Type-based amortised heap-space analysis. In: 15th European Symposium on Programming (ESOP\u201906).","DOI":"10.1007\/11693024_3"},{"key":"S0960129521000487_ref2","unstructured":"Bauer, S. (2019). Decidability of Linear Tree Constraints for Resource Analysis of Object-Oriented Programs. Phd thesis, Faculty of Mathematics, Computer Science and Statistics, LMU Munich, Germany, May 2019."},{"key":"S0960129521000487_ref21","doi-asserted-by":"crossref","unstructured":"Hoffmann, J. , Aehlig, K. and Hofmann, M. (2011). Multivariate amortized resource analysis. In: 38th Symposium on Principles of Programming Languages (POPL\u201911).","DOI":"10.1145\/1926385.1926427"},{"key":"S0960129521000487_ref46","doi-asserted-by":"crossref","unstructured":"Kahn, D. and Hoffmann, J. (2020). Exponential automatic amortized resource analysis. In: 23rd International Conference on Foundations of Software Science and Computation Structures (FoSSaCS\u201920).","DOI":"10.1007\/978-3-030-45231-5_19"},{"key":"S0960129521000487_ref45","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-016-9398-9"},{"key":"S0960129521000487_ref47","doi-asserted-by":"crossref","unstructured":"Knoth, T. , Wang, D. , Hoffmann, J. and Polikarpova, N. (2019). Resource-guided program synthesis. In: 40th Conference on Programming Language Design and Implementation (PLDI\u201919).","DOI":"10.1145\/3314221.3314602"},{"key":"S0960129521000487_ref7","doi-asserted-by":"crossref","unstructured":"Campbell, B. (2009). Amortised memory analysis using the depth of data structures. In: 18th European Symposium on Programming (ESOP\u201909).","DOI":"10.1007\/978-3-642-00590-9_14"},{"key":"S0960129521000487_ref22","doi-asserted-by":"crossref","unstructured":"Hoffmann, J. , Das, A. and Weng, S.-C. (2017). Towards automatic resource bound analysis for OCaml. In: 44th Symposium on Principles of Programming Languages (POPL\u201917).","DOI":"10.1145\/3009837.3009842"},{"key":"S0960129521000487_ref6","doi-asserted-by":"crossref","unstructured":"Blelloch, G. E. and Greiner, J. (1996). A provable time and space efficient implementation of NESL. In: 1st International Conference on Functional Programming (ICFP\u201996).","DOI":"10.1145\/232627.232650"},{"key":"S0960129521000487_ref51","unstructured":"Mobile Resource Guarantees (2002\u20132005). EU Project No. IST-2001-33149, https:\/\/cordis.europa.eu\/project\/id\/IST-2001-33149\/de."},{"key":"S0960129521000487_ref23","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-17164-2_13"},{"key":"S0960129521000487_ref4","unstructured":"Bauer, S. , Jost, S. and Hofmann, M. (2018). Decidable inequalities over infinite trees. In: Barthe, G., Sutcliffe, G. and Veanes, M. (eds.) LPAR-22. 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Awassa, Ethiopia, 16\u201321 November 2018, EPiC Series in Computing, vol. 57, EasyChair, 111\u2013130."},{"key":"S0960129521000487_ref12","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129521000505"},{"key":"S0960129521000487_ref58","doi-asserted-by":"crossref","unstructured":"Rajani, V. , Gaboardi, M. , Garg, D. and Hoffmann, J. (2021). A unifying type-theory for Higher-Order (Amortized) Cost Analysis. In: 48th Symposium on Principles of Programming Languages (POPL\u201921).","DOI":"10.1145\/3434308"},{"key":"S0960129521000487_ref60","unstructured":"Rodriguez, D. (2012). Amortised Resource Analysis for Object-Oriented Programs. Phd thesis, Faculty of Mathematics, Computer Science and Statistics, LMU Munich, Germany, October 2012."},{"key":"S0960129521000487_ref10","doi-asserted-by":"crossref","unstructured":"Carbonneaux, Q. , Hoffmann, J. and Shao, Z. (2015). Compositional certified resource bounds. In: 36th Conference on Programming Language Design and Implementation (PLDI\u201915). Artifact submitted and approved.","DOI":"10.1145\/2737924.2737955"},{"key":"S0960129521000487_ref36","doi-asserted-by":"crossref","unstructured":"Hofmann, M. and Rodriguez, D. (2009). Efficient type-checking for amortised heap-space analysis. In: 18th Conference on Computer Science Logic (CSL\u201909), LNCS.","DOI":"10.1007\/978-3-642-04027-6_24"},{"key":"S0960129521000487_ref29","unstructured":"Hofmann, M. (2000b). A type system for bounded space and functional in-place update. Nordic Journal of Computing 7 (4) 258\u2013289. An earlier version appeared in ESOP2000."},{"key":"S0960129521000487_ref13","doi-asserted-by":"crossref","unstructured":"Das, A. , Balzer, S. , Hoffmann, J. , Pfenning, F. and Santurkar, I. (2021). Resource-aware session types for digital contracts. In: 2021 IEEE Computer Security Foundations Symposium (CSF\u201921).","DOI":"10.1109\/CSF51468.2021.00004"},{"key":"S0960129521000487_ref24","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-11957-6_16"},{"key":"S0960129521000487_ref39","doi-asserted-by":"crossref","unstructured":"Ishtiaq, S. S. and O\u2019Hearn, P. W. (2001). BI as an assertion language for mutable data structures. In: 28th Symposium on Principles of Programming Languages (POPL\u201901).","DOI":"10.1145\/360204.375719"},{"key":"S0960129521000487_ref56","author":"Pfenning","year":"2015"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129521000487","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,3,8]],"date-time":"2023-03-08T09:49:25Z","timestamp":1678268965000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129521000487\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,3,16]]},"references-count":68,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2022,6]]}},"alternative-id":["S0960129521000487"],"URL":"https:\/\/doi.org\/10.1017\/s0960129521000487","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,3,16]]},"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 (http:\/\/creativecommons.org\/licenses\/by\/4.0\/), which permits unrestricted re-use, distribution and reproduction, provided the original article 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"}]}}