{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T20:10:02Z","timestamp":1784837402130,"version":"3.55.0"},"reference-count":58,"publisher":"Cambridge University Press (CUP)","issue":"6","license":[{"start":{"date-parts":[[2021,10,19]],"date-time":"2021-10-19T00:00:00Z","timestamp":1634601600000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by-nc-sa\/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>We introduce a novel amortised resource analysis couched in a type-and-effect system. Our analysis is formulated in terms of the physicist\u2019s method of amortised analysis and is potentialbased. The type system makes use of logarithmic potential functions and is the first such system to exhibit <jats:italic>logarithmic amortised complexity<\/jats:italic>. With our approach, we target the automated analysis of self-adjusting data structures, like splay trees, which so far have only manually been analysed in the literature. In particular, we have implemented a semi-automated prototype, which successfully analyses the zig-zig case of <jats:italic>splaying<\/jats:italic>, once the type annotations are fixed.<\/jats:p>","DOI":"10.1017\/s0960129521000232","type":"journal-article","created":{"date-parts":[[2021,10,19]],"date-time":"2021-10-19T21:25:54Z","timestamp":1634678754000},"page":"794-826","update-policy":"https:\/\/doi.org\/10.1017\/policypage","source":"Crossref","is-referenced-by-count":9,"title":["Type-based analysis of logarithmic amortised complexity"],"prefix":"10.1017","volume":"32","author":[{"given":"Martin","family":"Hofmann","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0391-3430","authenticated-orcid":false,"given":"Lorenz","family":"Leutgeb","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"David","family":"Obwaller","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Georg","family":"Moser","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1468-8398","authenticated-orcid":false,"given":"Florian","family":"Zuleger","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"56","published-online":{"date-parts":[[2021,10,19]]},"reference":[{"key":"S0960129521000232_ref26","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009842"},{"key":"S0960129521000232_ref1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-69166-2_15"},{"key":"S0960129521000232_ref58","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-23702-7_22"},{"key":"S0960129521000232_ref2","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-010-9174-1"},{"key":"S0960129521000232_ref20","doi-asserted-by":"publisher","DOI":"10.1145\/1806596.1806630"},{"key":"S0960129521000232_ref7","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2015.12.007"},{"key":"S0960129521000232_ref44","volume-title":"Structures","author":"Okasaki","year":"1999"},{"key":"S0960129521000232_ref25","doi-asserted-by":"crossref","unstructured":"Hoffmann, J. , Aehlig, K. and Hofmann, M. (2012b). Resource aware ML. In Proceedings of the 24th CAV, vol. 7358, LNCS, 781\u2013786.","DOI":"10.1007\/978-3-642-31424-7_64"},{"key":"S0960129521000232_ref38","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-05089-3_23"},{"key":"S0960129521000232_ref32","doi-asserted-by":"publisher","DOI":"10.1145\/604131.604148"},{"key":"S0960129521000232_ref4","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33125-1_27"},{"key":"S0960129521000232_ref46","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24622-0_20"},{"key":"S0960129521000232_ref29","doi-asserted-by":"crossref","unstructured":"Hoffmann, J. and Shao, Z. (2015a). Automatic static cost analysis for parallel programs. In: Proceedings of the 24th ESOP, vol. 9032. LNCS, 132\u2013157.","DOI":"10.1007\/978-3-662-46669-8_6"},{"key":"S0960129521000232_ref54","doi-asserted-by":"publisher","DOI":"10.1145\/3133903"},{"key":"S0960129521000232_ref50","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2015.7542264"},{"key":"S0960129521000232_ref22","unstructured":"Hoffmann, J. (2011). Types with Potential: Polynomial Resource Bounds via Automatic Amortized Analysis. PhD thesis, Ludwig-Maximilians-Universi\u00e4t M\u00fcnchen."},{"key":"S0960129521000232_ref40","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-45231-5_19"},{"key":"S0960129521000232_ref10","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17127-8_5"},{"key":"S0960129521000232_ref47","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(93)90249-9"},{"key":"S0960129521000232_ref52","first-page":"652","article-title":"Self-adjusting binary search trees","volume":"32","author":"Sleator","year":"1985","journal-title":"Journal of Alternative and Complementary Medicine"},{"key":"S0960129521000232_ref27","doi-asserted-by":"crossref","unstructured":"Hoffmann, J. and Hofmann, M. (2010a). Amortized resource analysis with polymorphic recursion and partial big-step operational semantics. In: Proceedings of the 8th APLAS, vol. 6461. LNCS, 172\u2013187.","DOI":"10.1007\/978-3-642-17164-2_13"},{"key":"S0960129521000232_ref41","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-90686-7_14"},{"key":"S0960129521000232_ref3","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15769-1_8"},{"key":"S0960129521000232_ref15","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-005-9022-x"},{"key":"S0960129521000232_ref9","unstructured":"Bauer, S. , Jost, S. and Hofmann, M. (2018). Decidable inequalities over infinite trees. In: Barthe, G. , Sutcliffe, G. and Veanes, M. (eds.), Proceedings of the 22nd LPAR, vol. 57. EPiC Series in Computing, EasyChair, 111\u2013130."},{"key":"S0960129521000232_ref43","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-22102-1_21"},{"key":"S0960129521000232_ref53","doi-asserted-by":"publisher","DOI":"10.1137\/0606031"},{"key":"S0960129521000232_ref5","unstructured":"Avanzini, M. , Eguchi, N. and Moser, G. (2011). A path order for rewrite systems that compute exponential time functions. In: Proceedings of the 22nd RTA, vol. 10. LIPIcs, 123\u2013138."},{"key":"S0960129521000232_ref24","doi-asserted-by":"publisher","DOI":"10.1145\/2362389.2362393"},{"key":"S0960129521000232_ref34","unstructured":"Hofmann, M. and Moser, G. (2015). Multivariate amortised resource analysis for term rewrite systems. In: Proceedings of the 13th TLCA, vol. 38, LIPIcs, 241\u2013256."},{"key":"S0960129521000232_ref37","doi-asserted-by":"crossref","unstructured":"Jost, S. , Hammond, K. , Loidl, H.-W. and Hofmann, M. (2010). Static determination of quantitative resource usage for higherorder programs. In: Proceedings of the 37th POPL, ACM, 223\u2013236.","DOI":"10.1145\/1707801.1706327"},{"key":"S0960129521000232_ref19","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-016-9388-y"},{"key":"S0960129521000232_ref21","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068411000457"},{"key":"S0960129521000232_ref28","doi-asserted-by":"crossref","unstructured":"Hoffmann, J. and Hofmann, M. (2010b). Amortized resource analysis with polynomial potential. In: Proceedings of the 19th ESOP, vol. 6012, LNCS, 287\u2013306.","DOI":"10.1007\/978-3-642-11957-6_16"},{"key":"S0960129521000232_ref30","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796815000192"},{"key":"S0960129521000232_ref17","unstructured":"Flores-Montoya, A. (2017). Cost Analysis of Programs Based on the Refinement of Cost Relations. PhD thesis, Darmstadt University of Technology, Germany."},{"key":"S0960129521000232_ref45","unstructured":"Pierce, B. (2002). Types and Programming Languages, MIT Press."},{"key":"S0960129521000232_ref49","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_50"},{"key":"S0960129521000232_ref12","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209191"},{"key":"S0960129521000232_ref51","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-016-9402-4"},{"key":"S0960129521000232_ref36","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_32"},{"key":"S0960129521000232_ref57","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-45231-5_32"},{"key":"S0960129521000232_ref16","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-73721-8_10"},{"key":"S0960129521000232_ref18","first-page":"14:1","article-title":"Verifying procedural programs via constrained rewriting induction","volume":"18","author":"Fuhs","year":"2017","journal-title":"Transactions on Computational Logic"},{"key":"S0960129521000232_ref6","doi-asserted-by":"publisher","DOI":"10.1145\/2784731.2784753"},{"key":"S0960129521000232_ref8","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49674-9_24"},{"key":"S0960129521000232_ref14","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-44522-8_18"},{"key":"S0960129521000232_ref39","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-016-9398-9"},{"key":"S0960129521000232_ref55","doi-asserted-by":"crossref","unstructured":"Winkler, S. and Moser, G. (2020). Runtime complexity analysis of logically constrained rewriting. In: Proceedings of the LOPSTR 2020.","DOI":"10.1007\/978-3-030-68446-4_2"},{"key":"S0960129521000232_ref11","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-17511-4_7"},{"key":"S0960129521000232_ref33","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08918-8_19"},{"key":"S0960129521000232_ref42","first-page":"185","article-title":"Automated amortised resource analysis for term rewrite systems","author":"Moser","year":"2020","journal-title":"Science of Computer Programming"},{"key":"S0960129521000232_ref56","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-20297-6_27"},{"key":"S0960129521000232_ref13","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63390-9_3"},{"key":"S0960129521000232_ref23","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926427"},{"key":"S0960129521000232_ref31","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-07151-0_10"},{"key":"S0960129521000232_ref35","unstructured":"Hofmann, M. and Moser, G. (2018). Analysis of logarithmic amortised complexity."},{"key":"S0960129521000232_ref48","unstructured":"Schrijver, A. (1999). Theory of Linear and Integer Programming, Wiley."}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129521000232","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,3,8]],"date-time":"2023-03-08T09:49:18Z","timestamp":1678268958000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129521000232\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,10,19]]},"references-count":58,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2022,6]]}},"alternative-id":["S0960129521000232"],"URL":"https:\/\/doi.org\/10.1017\/s0960129521000232","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,10,19]]},"assertion":[{"value":"\u00a9 The Author(s), 2021. 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-NonCommercial-ShareAlike licence (http:\/\/creativecommons.org\/licenses\/by-nc-sa\/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"}]}}