{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T09:04:54Z","timestamp":1784797494743,"version":"3.55.0"},"publisher-location":"Cham","reference-count":30,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032325365","type":"print"},{"value":"9783032325372","type":"electronic"}],"license":[{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2026,7,24]],"date-time":"2026-07-24T00:00:00Z","timestamp":1784851200000},"content-version":"vor","delay-in-days":204,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    We study the fully automated amortised analysis of purely functional data structures like\n                    <jats:italic>skew heaps<\/jats:italic>\n                    , as well as\n                    <jats:italic>weight<\/jats:italic>\n                    - and\n                    <jats:italic>rank-biased<\/jats:italic>\n                    leftist heaps. For that we generalise earlier works on automated amortised resource analysis by developing a type inference based approach with a generic type system. This allows for modular reasoning and the inference of precise and optimal cost bounds.\n                  <\/jats:p>\n                  <jats:p>More specifically, we extend the work on the ATLAS system by Leutgeb et al.\u00a0 which was developed to cover the analysis of splay trees and some closely related data structures. To enable the analysis of skew heaps, however, and the even more challenging (amortised) analysis of leftist heaps, we have developed a range of new techniques for type-based automated analysis. By introducing a generic type system we allow for arbitrary (classes of) potential functions, compared to the use of hard-coded potential functions in ATLAS, which we have implemented in Haskell in an entirely modular way. We have also greatly enhanced the existing type inference algorithm by extensions in multiple directions, including path-sensitive reasoning, data structure invariants, and template parameters for piecewise defined potential functions. We show how our newly developed system supports the use of all known potential functions for analysing skew heaps and leftist heaps, confirming the known bounds.<\/jats:p>","DOI":"10.1007\/978-3-032-32537-2_5","type":"book-chapter","created":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T08:41:29Z","timestamp":1784796089000},"page":"100-122","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Automated Amortised Analysis of\u00a0Skew Heaps and Leftist Heaps"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2298-9353","authenticated-orcid":false,"given":"Armin","family":"Walch","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9240-6128","authenticated-orcid":false,"given":"Georg","family":"Moser","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6273-8930","authenticated-orcid":false,"given":"Berry","family":"Schoenmakers","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":"297","published-online":{"date-parts":[[2026,7,24]]},"reference":[{"key":"5_CR1","doi-asserted-by":"publisher","unstructured":"Cho, S., Sahni, S.: Weight-biased leftist trees and modified skip lists. J. Exper. Algorith. (JEA) 3, 2\u2013s (1998). https:\/\/doi.org\/10.1145\/297096.297111","DOI":"10.1145\/297096.297111"},{"key":"5_CR2","unstructured":"Cormen, T.H., Leiserson, C.E., Rivest, R.L., Stein, C.: Introduction to algorithms. MIT press (2022)"},{"key":"5_CR3","unstructured":"Crane, C.A.: Linear Lists and Priority Queues as Balanced Binary Trees. PhD thesis, Computer Science, Stanford University, CA (1972)"},{"key":"5_CR4","doi-asserted-by":"crossref","unstructured":"Gibbons, J., de Moor, O.: The Fun of Programming. Palgrave (2003)","DOI":"10.1007\/978-1-349-91518-7"},{"key":"5_CR5","doi-asserted-by":"publisher","unstructured":"Haeupler, B., Sen, S., Tarjan, R.E.: Rank-balanced trees. ACM Trans. Algorith.(TALG) 11(4), 1\u201326 (2015). https:\/\/doi.org\/10.1145\/2689412","DOI":"10.1145\/2689412"},{"key":"5_CR6","doi-asserted-by":"publisher","unstructured":"Hoffmann, J., Aehlig, K., Hofmann, M.: Multivariate amortized resource analysis. In: Proceedings of the 38th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pp. 357\u2013370 (2011). https:\/\/doi.org\/10.1145\/1926385.1926427","DOI":"10.1145\/1926385.1926427"},{"key":"5_CR7","doi-asserted-by":"publisher","unstructured":"Hoffmann, J., Hofmann, M.: Amortized resource analysis with polynomial potential: A static inference of polynomial bounds for functional programs. In: Programming Languages and Systems: 19th European Symposium on Programming, ESOP 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Paphos, Cyprus, March 20\u201328, 2010. Proceedings 19, pp. 287\u2013306 (2010). https:\/\/doi.org\/10.1007\/978-3-642-11957-6_16","DOI":"10.1007\/978-3-642-11957-6_16"},{"issue":"1","key":"5_CR8","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1145\/640128.604148","volume":"38","author":"M Hofmann","year":"2003","unstructured":"Hofmann, M., Jost, S.: Static prediction of heap space usage for first-order functional programs. ACM SIGPLAN Notices 38(1), 185\u2013197 (2003). https:\/\/doi.org\/10.1145\/640128.604148","journal-title":"ACM SIGPLAN Notices"},{"issue":"6","key":"5_CR9","doi-asserted-by":"publisher","first-page":"794","DOI":"10.1017\/s0960129521000232","volume":"32","author":"M Hofmann","year":"2022","unstructured":"Hofmann, M., Leutgeb, L., Obwaller, D., Moser, G., Zuleger, F.: Type-based analysis of logarithmic amortised complexity. Math. Struct. Comput. Sci. 32(6), 794\u2013826 (2022). https:\/\/doi.org\/10.1017\/s0960129521000232","journal-title":"Math. Struct. Comput. Sci."},{"key":"5_CR10","doi-asserted-by":"publisher","unstructured":"Jost, S., Hammond, K., Loidl, H.-W., Hofmann, M.: Static determination of quantitative resource usage for higher-order programs. In: Proceedings of the 37th annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 223\u2013236 (2010). https:\/\/doi.org\/10.1145\/1706299.1706327","DOI":"10.1145\/1706299.1706327"},{"key":"5_CR11","doi-asserted-by":"publisher","unstructured":"Kahn, D.M., Hoffmann, J.: Exponential automatic amortized resource analysis. In: Foundations of Software Science and Computation Structures: 23rd International Conference, FOSSACS 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25\u201330, 2020, Proceedings 23, pp. 359\u2013380 (2020). https:\/\/doi.org\/10.1007\/978-3-030-45231-5_19","DOI":"10.1007\/978-3-030-45231-5_19"},{"issue":"5","key":"5_CR12","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1016\/0020-0190(91)90218-7","volume":"37","author":"A Kaldewaij","year":"1991","unstructured":"Kaldewaij, A., Schoenmakers, B.: The derivation of a tighter bound for topdown skew heaps. Inf. Process. Lett. 37(5), 265\u2013271 (1991). https:\/\/doi.org\/10.1016\/0020-0190(91)90218-7","journal-title":"Inf. Process. Lett."},{"key":"5_CR13","unstructured":"Knuth, D.E.: The art of computer programming, volume 3: (2nd ed.) sorting and searching. Addison Wesley Longman Publishing Co., Inc., USA (1998)"},{"key":"5_CR14","doi-asserted-by":"publisher","unstructured":"Leutgeb, L., Moser, G., Zuleger, F.: ATLAS: automated amortised complexity analysis of self-adjusting data structures. In: Computer Aided Verification: 33rd International Conference, CAV 2021, Virtual Event, July 20\u201323, 2021, Proceedings, Part II 33, pp. 99\u2013122 (2021). https:\/\/doi.org\/10.1007\/978-3-030-81688-9_5","DOI":"10.1007\/978-3-030-81688-9_5"},{"key":"5_CR15","doi-asserted-by":"publisher","unstructured":"Leutgeb, L., Moser, G., Zuleger, F.: Automated expected amortised cost analysis of probabilistic data structures. In: International Conference on Computer Aided Verification, pp. 70\u201391 (2022). https:\/\/doi.org\/10.1007\/978-3-031-13188-2_4","DOI":"10.1007\/978-3-031-13188-2_4"},{"issue":"3","key":"5_CR16","doi-asserted-by":"publisher","first-page":"367","DOI":"10.1007\/s10817-018-9459-3","volume":"62","author":"T Nipkow","year":"2018","unstructured":"Nipkow, T., Brinkop, H.: Amortized Complexity Verified. J. Autom. Reason. 62(3), 367\u2013391 (2018). https:\/\/doi.org\/10.1007\/s10817-018-9459-3","journal-title":"J. Autom. Reason."},{"key":"5_CR17","doi-asserted-by":"crossref","unstructured":"Okasaki, C.: Purely functional data structures. Cambridge University Press (1998)","DOI":"10.1017\/CBO9780511530104"},{"key":"5_CR18","doi-asserted-by":"crossref","unstructured":"Reynolds, J.C.: Theories of programming languages. Cambridge University Press (1998)","DOI":"10.1017\/CBO9780511626364"},{"key":"5_CR19","doi-asserted-by":"publisher","unstructured":"Rondon, P.M., Kawaguci, M., Jhala, R.: Liquid types. In: Proceedings of the 29th ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 159\u2013169 (2008). https:\/\/doi.org\/10.1145\/1379022.1375602","DOI":"10.1145\/1379022.1375602"},{"key":"5_CR20","unstructured":"Schoenmakers, B.: Data Structures and Amortized Complexity in a Functional Setting. PhD thesis, Math & CS, TU Eindhoven, Netherlands (1992)"},{"issue":"5","key":"5_CR21","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1016\/s0020-0190(97)00028-8","volume":"61","author":"B Schoenmakers","year":"1997","unstructured":"Schoenmakers, B.: A tight lower bound for top-down skew heaps. Inf. Process. Lett. 61(5), 279\u2013284 (1997). https:\/\/doi.org\/10.1016\/s0020-0190(97)00028-8","journal-title":"Inf. Process. Lett."},{"key":"5_CR22","doi-asserted-by":"publisher","unstructured":"Schoenmakers, B.: Amortized Analysis of Leftist Heaps. In: Principles of Verification: Cycling the Probabilistic Landscape: Essays Dedicated to Joost-Pieter Katoen on the Occasion of His 60th Birthday, Part I, pp. 73\u201384. Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-75783-9_3","DOI":"10.1007\/978-3-031-75783-9_3"},{"key":"5_CR23","doi-asserted-by":"publisher","unstructured":"Simoes, H., Vasconcelos, P., Florido, M., Jost, S., 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, pp. 165\u2013176 (2012). https:\/\/doi.org\/10.1145\/2398856.2364575","DOI":"10.1145\/2398856.2364575"},{"issue":"3","key":"5_CR24","doi-asserted-by":"publisher","first-page":"652","DOI":"10.1145\/3828.3835","volume":"32","author":"DD Sleator","year":"1985","unstructured":"Sleator, D.D., Tarjan, R.E.: Self-adjusting binary search trees. J. ACM (JACM) 32(3), 652\u2013686 (1985). https:\/\/doi.org\/10.1145\/3828.3835","journal-title":"J. ACM (JACM)"},{"issue":"1","key":"5_CR25","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1137\/0215004","volume":"15","author":"DD Sleator","year":"1986","unstructured":"Sleator, D.D., Tarjan, R.E.: Self-adjusting heaps. SIAM J. Comput. 15(1), 52\u201369 (1986). https:\/\/doi.org\/10.1137\/0215004","journal-title":"SIAM J. Comput."},{"issue":"2","key":"5_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 Discr. Methods 6(2), 306\u2013318 (1985). https:\/\/doi.org\/10.1137\/0606031","journal-title":"SIAM J. Algebraic Discr. Methods"},{"key":"5_CR27","doi-asserted-by":"publisher","unstructured":"Vasconcelos, P., Jost, S., Florido, M., Hammond, K.: Type-based allocation analysis for co-recursion in lazy functional languages. In: Programming Languages and Systems: 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, 2015, Proceedings 24, pp. 787\u2013811 (2015). https:\/\/doi.org\/10.1007\/978-3-662-46669-8_32","DOI":"10.1007\/978-3-662-46669-8_32"},{"key":"5_CR28","doi-asserted-by":"publisher","unstructured":"Vazou, N., Rondon, P.M., Jhala, R.: Abstract refinement types. In: European Symposium on Programming, pp. 209\u2013228 (2013). https:\/\/doi.org\/10.1007\/978-3-642-37036-6_13","DOI":"10.1007\/978-3-642-37036-6_13"},{"key":"5_CR29","unstructured":"Walch, A., Moser, G., Schoenmakers, B., Zuleger, F.: Automated Amortised Analysis of Skew Heaps and Leftist Heaps (Extended Version), (2026). arXiv: 2605.12091 [cs.PL]. https:\/\/arxiv.org\/abs\/2605.12091"},{"key":"5_CR30","doi-asserted-by":"publisher","unstructured":"Wang, D., Kahn, D.M., Hoffmann, J.: Raising expectations: automating expected cost analysis with types. Proc. ACM Programm. Lang. 4(ICFP), 1\u201331 (2020). https:\/\/doi.org\/10.1145\/3408992","DOI":"10.1145\/3408992"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-32537-2_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T08:41:34Z","timestamp":1784796094000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-32537-2_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032325365","9783032325372"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-32537-2_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026]]},"assertion":[{"value":"24 July 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The authors have no competing interests.","order":1,"name":"Ethics","label":"Disclosure of Interests","group":{"name":"EthicsHeading","label":"Ethics"}},{"value":"A research artifact is publicly available on Zenodo at\n                      \n                      . It includes a pre-built Docker image of our prototype, provided as a command-line tool, the complete source code, and the benchmark suite used in our evaluation. The artifact also provides detailed, step-by-step instructions for reproducing the results reported in this paper, namely the automatically derived complexity bounds.In addition, the tool is released as open-source software and is hosted at\n                      \n                      , facilitating reuse, inspection, and adaptation for independent studies.","order":2,"name":"Ethics","label":"Data-Availability Statement","group":{"name":"EthicsHeading","label":"Ethics"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Lisbon","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Portugal","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2026","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26 July 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29 July 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"38","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2026","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.floc26.org\/program","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}