{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T07:01:44Z","timestamp":1779087704598,"version":"3.51.4"},"reference-count":45,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2023,1,9]],"date-time":"2023-01-09T00:00:00Z","timestamp":1673222400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-sa\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["787914"],"award-info":[{"award-number":["787914"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2023,1,9]]},"abstract":"<jats:p>\n            We develop a weakest-precondition-style calculus \u00e0 la Dijkstra for reasoning about\n            <jats:italic>amortized expected runtimes of randomized algorithms with access to dynamic memory<\/jats:italic>\n            \u2014 the aert calculus. Our calculus is truly quantitative, i.e. instead of Boolean valued predicates, it manipulates real-valued functions. \t En route to the aert calculus, we study the ert calculus for reasoning about\n            <jats:italic>expected runtimes<\/jats:italic>\n            of Kaminski et al. [2018] extended by capabilities for handling dynamic memory, thus enabling\n            <jats:italic>compositional<\/jats:italic>\n            and\n            <jats:italic>local<\/jats:italic>\n            reasoning about\n            <jats:italic>randomized data structures<\/jats:italic>\n            . This extension employs\n            <jats:italic>runtime separation logic<\/jats:italic>\n            , which has been foreshadowed by Matheja [2020] and then implemented in Isabelle\/HOL by Haslbeck [2021]. In addition to Haslbeck\u2019s results, we further prove soundness of the so-extended ert calculus with respect to an operational Markov decision process model featuring countably-branching nondeterminism, provide extensive intuitive explanations, and provide proof rules enabling separation logic-style verification for upper bounds on expected runtimes. Finally, we build the so-called\n            <jats:italic>potential method<\/jats:italic>\n            for amortized analysis into the ert calculus, thus obtaining the aert calculus. Soundness of the aert calculus is obtained from the soundness of the ert calculus and some probabilistic form of telescoping. \t Since one needs to be able to handle\n            <jats:italic>changes in potential<\/jats:italic>\n            which can in principle be both positive or negative, the aert calculus needs to be \u2014 essentially \u2014 capable of handling certain signed random variables. A particularly pleasing feature of our solution is that, unlike e.g. Kozen [1985], we obtain a loop rule for our signed random variables, and furthermore, unlike e.g. Kaminski and Katoen [2017], the aert calculus makes do without the need for involved technical machinery keeping track of the integrability of the random variables.\n          <\/jats:p>\n          <jats:p>Finally, we present case studies, including a formal analysis of a randomized delete-insert-find-any set data structure [Brodal et al. 1996], which yields a constant expected runtime per operation, whereas no deterministic algorithm can achieve this.<\/jats:p>","DOI":"10.1145\/3571260","type":"journal-article","created":{"date-parts":[[2023,1,11]],"date-time":"2023-01-11T21:58:14Z","timestamp":1673474294000},"page":"1957-1986","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":21,"title":["A Calculus for Amortized Expected Runtimes"],"prefix":"10.1145","volume":"7","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-8705-2564","authenticated-orcid":false,"given":"Kevin","family":"Batz","sequence":"first","affiliation":[{"name":"RWTH Aachen University, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5185-2324","authenticated-orcid":false,"given":"Benjamin Lucien","family":"Kaminski","sequence":"additional","affiliation":[{"name":"Saarland University, Germany \/ University College London, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6143-1926","authenticated-orcid":false,"given":"Joost-Pieter","family":"Katoen","sequence":"additional","affiliation":[{"name":"RWTH Aachen University, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9151-0441","authenticated-orcid":false,"given":"Christoph","family":"Matheja","sequence":"additional","affiliation":[{"name":"DTU, Denmark"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6823-7918","authenticated-orcid":false,"given":"Lena","family":"Verscht","sequence":"additional","affiliation":[{"name":"RWTH Aachen University, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2023,1,11]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0020-0190(01)00230-7"},{"key":"e_1_2_1_2_1","volume-title":"Amortised Resource Analysis with Separation Logic. Log. Methods Comput. Sci., 7, 2","author":"Atkey Robert","year":"2011","unstructured":"Robert Atkey . 2011. Amortised Resource Analysis with Separation Logic. Log. Methods Comput. Sci., 7, 2 ( 2011 ). Robert Atkey. 2011. Amortised Resource Analysis with Separation Logic. Log. Methods Comput. Sci., 7, 2 (2011)."},{"key":"e_1_2_1_3_1","volume-title":"Ugo Dal Lago, and Alexis Ghyselen","author":"Avanzini Martin","year":"2019","unstructured":"Martin Avanzini , Ugo Dal Lago, and Alexis Ghyselen . 2019 . Type-Based Complexity Analysis of Probabilistic Functional Programs. In LICS. IEEE , 1\u201313. Martin Avanzini, Ugo Dal Lago, and Alexis Ghyselen. 2019. Type-Based Complexity Analysis of Probabilistic Functional Programs. In LICS. IEEE, 1\u201313."},{"key":"e_1_2_1_4_1","volume-title":"Principles of Model Checking","author":"Baier Christel","unstructured":"Christel Baier and Joost-Pieter Katoen . 2008. Principles of Model Checking . MIT Press . Christel Baier and Joost-Pieter Katoen. 2008. Principles of Model Checking. MIT Press."},{"key":"e_1_2_1_5_1","volume-title":"Joost-Pieter Katoen, Christoph Matheja, and Philipp Schr\u00f6er.","author":"Batz Kevin","year":"2021","unstructured":"Kevin Batz , Mingshuai Chen , Benjamin Lucien Kaminski , Joost-Pieter Katoen, Christoph Matheja, and Philipp Schr\u00f6er. 2021 . Latticed k-Induction with an Application to Probabilistic Programs. In CAV (2) (Lecture Notes in Computer Science , Vol. 12760). Springer, 524\u2013 549 . Kevin Batz, Mingshuai Chen, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, and Philipp Schr\u00f6er. 2021. Latticed k-Induction with an Application to Probabilistic Programs. In CAV (2) (Lecture Notes in Computer Science, Vol. 12760). Springer, 524\u2013549."},{"key":"e_1_2_1_6_1","volume-title":"Christoph Matheja, and Thomas Noll.","author":"Batz Kevin","year":"2022","unstructured":"Kevin Batz , Ira Fesefeldt , Marvin Jansen , Joost-Pieter Katoen , Florian Ke\u00df ler , Christoph Matheja, and Thomas Noll. 2022 . Foundations for Entailment Checking in Quantitative Separation Logic. In ESOP (Lecture Notes in Computer Science , Vol. 13240). Springer, 57\u2013 84 . Kevin Batz, Ira Fesefeldt, Marvin Jansen, Joost-Pieter Katoen, Florian Ke\u00df ler, Christoph Matheja, and Thomas Noll. 2022. Foundations for Entailment Checking in Quantitative Separation Logic. In ESOP (Lecture Notes in Computer Science, Vol. 13240). Springer, 57\u201384."},{"key":"e_1_2_1_7_1","volume-title":"Proc. ACM Program. Lang., 5, POPL","author":"Batz Kevin","year":"2021","unstructured":"Kevin Batz , Benjamin Lucien Kaminski , Joost-Pieter Katoen , and Christoph Matheja . 2021 . Relatively complete verification of probabilistic programs: an expressive language for expectation-based reasoning . Proc. ACM Program. Lang., 5, POPL (2021), 1\u201330. Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, and Christoph Matheja. 2021. Relatively complete verification of probabilistic programs: an expressive language for expectation-based reasoning. Proc. ACM Program. Lang., 5, POPL (2021), 1\u201330."},{"key":"e_1_2_1_8_1","volume-title":"Proc. ACM Program. Lang., 3, POPL","author":"Batz Kevin","year":"2019","unstructured":"Kevin Batz , Benjamin Lucien Kaminski , Joost-Pieter Katoen , Christoph Matheja , and Thomas Noll . 2019 . Quantitative Separation Logic \u2014 A Logic for Reasoning about Probabilistic Programs . Proc. ACM Program. Lang., 3, POPL (2019), 34:1\u201334:29. Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, and Thomas Noll. 2019. Quantitative Separation Logic \u2014 A Logic for Reasoning about Probabilistic Programs. Proc. ACM Program. Lang., 3, POPL (2019), 34:1\u201334:29."},{"key":"e_1_2_1_9_1","volume-title":"Joost-Pieter Katoen, Christoph Matheja, and Lena Verscht.","author":"Batz Kevin","year":"2022","unstructured":"Kevin Batz , Benjamin Lucien Kaminski , Joost-Pieter Katoen, Christoph Matheja, and Lena Verscht. 2022 . A Calculus for Amortized Expected Runtimes - Extended Version. CoRR , to appear Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, and Lena Verscht. 2022. A Calculus for Amortized Expected Runtimes - Extended Version. CoRR, to appear"},{"key":"e_1_2_1_10_1","volume-title":"Proceedings of the 5th Berkeley Symposium on Mathematical Statistics and Probability. 1","author":"Blackwell David","year":"1967","unstructured":"David Blackwell . 1967 . Positive dynamic programming . In Proceedings of the 5th Berkeley Symposium on Mathematical Statistics and Probability. 1 , University of California Press, 415\u2013418. David Blackwell. 1967. Positive dynamic programming. In Proceedings of the 5th Berkeley Symposium on Mathematical Statistics and Probability. 1, University of California Press, 415\u2013418."},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jcss.2014.06.005"},{"key":"e_1_2_1_12_1","first-page":"337","article-title":"The Randomized Complexity of Maintaining the Minimum","volume":"3","author":"Brodal Gerth St\u00f8lting","year":"1996","unstructured":"Gerth St\u00f8lting Brodal , Shiva Chaudhuri , and Jaikumar Radhakrishnan . 1996 . The Randomized Complexity of Maintaining the Minimum . Nord. J. Comput. , 3 , 4 (1996), 337 \u2013 351 . Gerth St\u00f8lting Brodal, Shiva Chaudhuri, and Jaikumar Radhakrishnan. 1996. The Randomized Complexity of Maintaining the Minimum. Nord. J. Comput., 3, 4 (1996), 337\u2013351.","journal-title":"Nord. J. Comput."},{"key":"e_1_2_1_13_1","doi-asserted-by":"crossref","unstructured":"Quentin Carbonneaux Jan Hoffmann Tahina Ramananandro and Zhong Shao. 2014. End-to-end verification of stack-space bounds for C programs. In PLDI. ACM 270\u2013281. \t\t\t\t  Quentin Carbonneaux Jan Hoffmann Tahina Ramananandro and Zhong Shao. 2014. End-to-end verification of stack-space bounds for C programs. In PLDI. ACM 270\u2013281.","DOI":"10.1145\/2666356.2594301"},{"key":"e_1_2_1_14_1","volume-title":"Proc. of the International Symposium on Formal Methods (FM) (Lecture Notes in Computer Science","volume":"122","author":"Celiku Orieta","year":"2005","unstructured":"Orieta Celiku and Annabelle McIver . 2005 . Compositional Specification and Analysis of Cost\u2013Based Properties in Probabilistic Programs . In Proc. of the International Symposium on Formal Methods (FM) (Lecture Notes in Computer Science , Vol. 3582). Springer, 107\u2013 122 . Orieta Celiku and Annabelle McIver. 2005. Compositional Specification and Analysis of Cost\u2013Based Properties in Probabilistic Programs. In Proc. of the International Symposium on Formal Methods (FM) (Lecture Notes in Computer Science, Vol. 3582). Springer, 107\u2013122."},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-017-9431-7"},{"key":"e_1_2_1_16_1","volume-title":"Introduction to Algorithms","author":"Cormen Thomas H.","unstructured":"Thomas H. Cormen , Charles E. Leiserson , Ronald L. Rivest , and Clifford Stein . 2009. Introduction to Algorithms , 3 rd Edition. MIT Press . Thomas H. Cormen, Charles E. Leiserson, Ronald L. Rivest, and Clifford Stein. 2009. Introduction to Algorithms, 3rd Edition. MIT Press.","edition":"3"},{"key":"e_1_2_1_17_1","volume-title":"Randomized Splay Trees","author":"F\u00fcrer Martin","unstructured":"Martin F\u00fcrer . 1999. Randomized Splay Trees . In SODA. ACM\/SIAM , 903\u2013904. Martin F\u00fcrer. 1999. Randomized Splay Trees. In SODA. ACM\/SIAM, 903\u2013904."},{"key":"e_1_2_1_18_1","volume-title":"ESOP (Lecture Notes in Computer Science","volume":"560","author":"Gu\u00e9neau Arma\u00ebl","year":"2018","unstructured":"Arma\u00ebl Gu\u00e9neau , Arthur Chargu\u00e9raud , and Fran\u00e7ois Pottier . 2018 . A Fistful of Dollars: Formalizing Asymptotic Complexity Claims via Deductive Program Verification . In ESOP (Lecture Notes in Computer Science , Vol. 10801). Springer, 533\u2013 560 . Arma\u00ebl Gu\u00e9neau, Arthur Chargu\u00e9raud, and Fran\u00e7ois Pottier. 2018. A Fistful of Dollars: Formalizing Asymptotic Complexity Claims via Deductive Program Verification. In ESOP (Lecture Notes in Computer Science, Vol. 10801). Springer, 533\u2013560."},{"key":"e_1_2_1_19_1","unstructured":"Maximilian Paul Louis Haslbeck. 2021. Verified Quantitative Analysis of Imperative Algorithms. Technische Universit\u00e4t M\u00fcnchen. \t\t\t\t  Maximilian Paul Louis Haslbeck. 2021. Verified Quantitative Analysis of Imperative Algorithms. Technische Universit\u00e4t M\u00fcnchen."},{"key":"e_1_2_1_20_1","volume-title":"TACAS (1) (Lecture Notes in Computer Science","author":"Louis Haslbeck Maximilian Paul","unstructured":"Maximilian Paul Louis Haslbeck and Tobias Nipkow . 2018. Hoare Logics for Time Bounds - A Study in Meta Theory . In TACAS (1) (Lecture Notes in Computer Science , Vol. 10805). Springer, 155\u2013 171 . Maximilian Paul Louis Haslbeck and Tobias Nipkow. 2018. Hoare Logics for Time Bounds - A Study in Meta Theory. In TACAS (1) (Lecture Notes in Computer Science, Vol. 10805). Springer, 155\u2013171."},{"key":"e_1_2_1_21_1","unstructured":"Jan Hoffmann. 2011. Types with Potential: Polynomial Resource Bounds via Automatic Amortized Analysis. Ph. D. Dissertation. LMU Munich. \t\t\t\t  Jan Hoffmann. 2011. Types with Potential: Polynomial Resource Bounds via Automatic Amortized Analysis. Ph. D. Dissertation. LMU Munich."},{"key":"e_1_2_1_22_1","doi-asserted-by":"crossref","unstructured":"Jan Hoffmann and Steffen Jost. 2022. Two decades of automatic amortized resource analysis. Math. Struct. Comput. Sci.. \t\t\t\t  Jan Hoffmann and Steffen Jost. 2022. Two decades of automatic amortized resource analysis. Math. Struct. Comput. Sci..","DOI":"10.1017\/S0960129521000487"},{"key":"e_1_2_1_23_1","volume-title":"Proc. of the Symposium on Principles of Programming Languages (POPL). ACM, 14\u201326","author":"Samin","unstructured":"Samin S. Ishtiaq and Peter William O\u2019Hearn. 2001. BI as an Assertion Language for Mutable Data Structures . In Proc. of the Symposium on Principles of Programming Languages (POPL). ACM, 14\u201326 . Samin S. Ishtiaq and Peter William O\u2019Hearn. 2001. BI as an Assertion Language for Mutable Data Structures. In Proc. of the Symposium on Principles of Programming Languages (POPL). ACM, 14\u201326."},{"key":"e_1_2_1_24_1","volume-title":"Kahn and Jan Hoffmann","author":"David","year":"2020","unstructured":"David M. Kahn and Jan Hoffmann . 2020 . Exponential Automatic Amortized Resource Analysis. In FoSSaCS (Lecture Notes in Computer Science , Vol. 12077). Springer, 359\u2013 380 . David M. Kahn and Jan Hoffmann. 2020. Exponential Automatic Amortized Resource Analysis. In FoSSaCS (Lecture Notes in Computer Science, Vol. 12077). Springer, 359\u2013380."},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.18154\/RWTH-2019-01829"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2017.8005153"},{"key":"e_1_2_1_27_1","doi-asserted-by":"crossref","unstructured":"Benjamin Lucien Kaminski Joost-Pieter Katoen Christoph Matheja and Federico Olmedo. 2018. Weakest Precondition Reasoning for Expected Runtimes of Randomized Algorithms. J. ACM 30. \t\t\t\t  Benjamin Lucien Kaminski Joost-Pieter Katoen Christoph Matheja and Federico Olmedo. 2018. Weakest Precondition Reasoning for Expected Runtimes of Randomized Algorithms. J. ACM 30.","DOI":"10.1145\/3208102"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(85)90012-1"},{"key":"e_1_2_1_29_1","volume-title":"Proc. of the International Conference on Computer-Aided Verification (Lecture Notes inn Computer Science). (to appear)","author":"Leutgeb Lorenz","year":"2022","unstructured":"Lorenz Leutgeb , Georg Moser , and Florian Zuleger . 2022 . Automated Expected Amortised Cost Analysis of Probabilistic Data Structures . In Proc. of the International Conference on Computer-Aided Verification (Lecture Notes inn Computer Science). (to appear) Lorenz Leutgeb, Georg Moser, and Florian Zuleger. 2022. Automated Expected Amortised Cost Analysis of Probabilistic Data Structures. In Proc. of the International Conference on Computer-Aided Verification (Lecture Notes inn Computer Science). (to appear)"},{"key":"e_1_2_1_30_1","volume-title":"Automated Reasoning and Randomization in Separation Logic","author":"Matheja Christoph","unstructured":"Christoph Matheja . 2020. Automated Reasoning and Randomization in Separation Logic . RWTH Aachen University , Germany . Christoph Matheja. 2020. Automated Reasoning and Randomization in Separation Logic. RWTH Aachen University, Germany."},{"key":"e_1_2_1_31_1","volume-title":"Refinement and Proof for Probabilistic Systems","author":"McIver Annabelle","unstructured":"Annabelle McIver and Carroll Morgan . 2005. Abstraction , Refinement and Proof for Probabilistic Systems . Springer . Annabelle McIver and Carroll Morgan. 2005. Abstraction, Refinement and Proof for Probabilistic Systems. Springer."},{"key":"e_1_2_1_32_1","volume-title":"ESOP (Lecture Notes in Computer Science","volume":"29","author":"M\u00e9vel Glen","year":"2019","unstructured":"Glen M\u00e9vel , Jacques-Henri Jourdan , and Fran\u00e7ois Pottier . 2019 . Time Credits and Time Receipts in Iris . In ESOP (Lecture Notes in Computer Science , Vol. 11423). Springer, 3\u2013 29 . Glen M\u00e9vel, Jacques-Henri Jourdan, and Fran\u00e7ois Pottier. 2019. Time Credits and Time Receipts in Iris. In ESOP (Lecture Notes in Computer Science, Vol. 11423). Springer, 3\u201329."},{"key":"e_1_2_1_33_1","volume-title":"TACAS (1) (Lecture Notes in Computer Science","author":"Meyer Fabian","unstructured":"Fabian Meyer , Marcel Hark , and J\u00fcrgen Giesl . 2021. Inferring Expected Runtimes of Probabilistic Integer Programs Using Expected Sizes . In TACAS (1) (Lecture Notes in Computer Science , Vol. 12651). Springer, 250\u2013 269 . Fabian Meyer, Marcel Hark, and J\u00fcrgen Giesl. 2021. Inferring Expected Runtimes of Probabilistic Integer Programs Using Expected Sizes. In TACAS (1) (Lecture Notes in Computer Science, Vol. 12651). Springer, 250\u2013269."},{"key":"e_1_2_1_34_1","volume-title":"Proc. of the Static Analysis Symposium (SAS) (Lecture Notes in Computer Science","volume":"126","author":"Monniaux David","year":"2001","unstructured":"David Monniaux . 2001 . An Abstract Analysis of the Probabilistic Termination of Programs . In Proc. of the Static Analysis Symposium (SAS) (Lecture Notes in Computer Science , Vol. 2126). Springer, 111\u2013 126 . David Monniaux. 2001. An Abstract Analysis of the Probabilistic Termination of Programs. In Proc. of the Static Analysis Symposium (SAS) (Lecture Notes in Computer Science, Vol. 2126). Springer, 111\u2013126."},{"key":"e_1_2_1_35_1","volume-title":"ESOP (Lecture Notes in Computer Science","volume":"518","author":"Moosbrugger Marcel","year":"2021","unstructured":"Marcel Moosbrugger , Ezio Bartocci , Joost-Pieter Katoen , and Laura Kov\u00e1cs . 2021 . Automated Termination Analysis of Polynomial Probabilistic Programs . In ESOP (Lecture Notes in Computer Science , Vol. 12648). Springer, 491\u2013 518 . Marcel Moosbrugger, Ezio Bartocci, Joost-Pieter Katoen, and Laura Kov\u00e1cs. 2021. Automated Termination Analysis of Polynomial Probabilistic Programs. In ESOP (Lecture Notes in Computer Science, Vol. 12648). Springer, 491\u2013518."},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192394"},{"key":"e_1_2_1_37_1","volume-title":"ITP (Lecture Notes in Computer Science","volume":"324","author":"Nipkow Tobias","year":"2015","unstructured":"Tobias Nipkow . 2015 . Amortized Complexity Verified . In ITP (Lecture Notes in Computer Science , Vol. 9236). Springer, 310\u2013 324 . Tobias Nipkow. 2015. Amortized Complexity Verified. In ITP (Lecture Notes in Computer Science, Vol. 9236). Springer, 310\u2013324."},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-018-9459-3"},{"key":"e_1_2_1_39_1","volume-title":"WADS (Lecture Notes in Computer Science","volume":"449","author":"Pugh William W.","year":"1989","unstructured":"William W. Pugh . 1989 . Skip Lists: A Probabilistic Alternative to Balanced Trees . In WADS (Lecture Notes in Computer Science , Vol. 382). Springer, 437\u2013 449 . William W. Pugh. 1989. Skip Lists: A Probabilistic Alternative to Balanced Trees. In WADS (Lecture Notes in Computer Science, Vol. 382). Springer, 437\u2013449."},{"key":"e_1_2_1_40_1","volume-title":"Markov Decision Processes: Discrete Stochastic Dynamic Programming","author":"Puterman Martin Lee","unstructured":"Martin Lee Puterman . 2005. Markov Decision Processes: Discrete Stochastic Dynamic Programming . John Wiley & Sons . Martin Lee Puterman. 2005. Markov Decision Processes: Discrete Stochastic Dynamic Programming. John Wiley & Sons."},{"key":"e_1_2_1_41_1","volume-title":"Proc. ACM Program. Lang., 5, POPL","author":"Rajani Vineet","year":"2021","unstructured":"Vineet Rajani , Marco Gaboardi , Deepak Garg , and Jan Hoffmann . 2021 . A unifying type-theory for higher-order (amortized) cost analysis . Proc. ACM Program. Lang., 5, POPL (2021), 1\u201328. Vineet Rajani, Marco Gaboardi, Deepak Garg, and Jan Hoffmann. 2021. A unifying type-theory for higher-order (amortized) cost analysis. Proc. ACM Program. Lang., 5, POPL (2021), 1\u201328."},{"key":"e_1_2_1_42_1","volume-title":"Proc. of the Annual Symposium on Logic in Computer Science (LICS). IEEE Computer Society, 55\u201374","author":"Reynolds John Charles","year":"2002","unstructured":"John Charles Reynolds . 2002 . Separation Logic: A Logic for Shared Mutable Data Structures . In Proc. of the Annual Symposium on Logic in Computer Science (LICS). IEEE Computer Society, 55\u201374 . John Charles Reynolds. 2002. Separation Logic: A Logic for Shared Mutable Data Structures. In Proc. of the Annual Symposium on Logic in Computer Science (LICS). IEEE Computer Society, 55\u201374."},{"key":"e_1_2_1_43_1","doi-asserted-by":"crossref","unstructured":"Daniel Dominic Sleator and Robert Endre Tarjan. 1985. Self-Adjusting Binary Search Trees. J. ACM 652\u2013686. \t\t\t\t  Daniel Dominic Sleator and Robert Endre Tarjan. 1985. Self-Adjusting Binary Search Trees. J. ACM 652\u2013686.","DOI":"10.1145\/3828.3835"},{"key":"e_1_2_1_44_1","series-title":"SIAM Journal on Algebraic Discrete Methods, 306\u2013318","volume-title":"Amortized Computational Complexity","author":"Tarjan Robert Endre","unstructured":"Robert Endre Tarjan . 1985. Amortized Computational Complexity . SIAM Journal on Algebraic Discrete Methods, 306\u2013318 . Robert Endre Tarjan. 1985. Amortized Computational Complexity. SIAM Journal on Algebraic Discrete Methods, 306\u2013318."},{"key":"e_1_2_1_45_1","volume-title":"Proc. ACM Program. Lang., 4, ICFP","author":"Wang Di","year":"2020","unstructured":"Di Wang , David M. Kahn , and Jan Hoffmann . 2020 . Raising expectations: automating expected cost analysis with types . Proc. ACM Program. Lang., 4, ICFP (2020), 110:1\u2013110:31. Di Wang, David M. Kahn, and Jan Hoffmann. 2020. Raising expectations: automating expected cost analysis with types. Proc. ACM Program. Lang., 4, ICFP (2020), 110:1\u2013110:31."}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3571260","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3571260","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T18:08:22Z","timestamp":1750183702000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3571260"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,1,9]]},"references-count":45,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2023,1,9]]}},"alternative-id":["10.1145\/3571260"],"URL":"https:\/\/doi.org\/10.1145\/3571260","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,1,9]]},"assertion":[{"value":"2023-01-11","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}