{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T20:59:39Z","timestamp":1760043579456,"version":"3.37.3"},"reference-count":47,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2018,3,13]],"date-time":"2018-03-13T00:00:00Z","timestamp":1520899200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"publisher","award":["NI 491\/16-1"],"award-info":[{"award-number":["NI 491\/16-1"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2019,3]]},"DOI":"10.1007\/s10817-018-9459-3","type":"journal-article","created":{"date-parts":[[2018,3,13]],"date-time":"2018-03-13T11:14:43Z","timestamp":1520939683000},"page":"367-391","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":17,"title":["Amortized Complexity Verified"],"prefix":"10.1007","volume":"62","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0730-515X","authenticated-orcid":false,"given":"Tobias","family":"Nipkow","sequence":"first","affiliation":[]},{"given":"Hauke","family":"Brinkop","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2018,3,13]]},"reference":[{"key":"9459_CR1","doi-asserted-by":"publisher","first-page":"2","DOI":"10.2168\/LMCS-7(2:17)2011","volume":"7","author":"R Atkey","year":"2011","unstructured":"Atkey, R.: Amortised resource analysis with separation logic. Log. Methods Comput. Sci. 7, 2 (2011)","journal-title":"Log. Methods Comput. Sci."},{"issue":"1\u20132","key":"9459_CR2","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1016\/j.tcs.2003.10.022","volume":"318","author":"R Benzinger","year":"2004","unstructured":"Benzinger, R.: Automated higher-order complexity analysis. Theor. Comput. Sci. 318(1\u20132), 79\u2013103 (2004)","journal-title":"Theor. Comput. Sci."},{"unstructured":"Brinkop, H., Nipkow, T.: Pairing heap. Archive of Formal Proofs (2016). Formal proof development. http:\/\/isa-afp.org\/entries\/Pairing_Heap.html","key":"9459_CR3"},{"key":"9459_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"64","DOI":"10.1007\/978-3-319-63390-9_4","volume-title":"Computer Aided Verification, CAV 2017, Part II","author":"Q Carbonneaux","year":"2017","unstructured":"Carbonneaux, Q., Hoffmann, J., Reps, T.W., Shao, Z.: Automated resource analysis with Coq proof objects. In: Majumdar, R., Kuncak, V. (eds.) Computer Aided Verification, CAV 2017, Part II. Lecture Notes in Computer Science, vol. 10427, pp. 64\u201385. Springer, Berlin (2017)"},{"unstructured":"Chargu\u00e9raud, A., Pottier, F.: Verifying the correctness and amortized complexity of a union-find implementation in separation logic with time credits. J. Autom. Reason. To appear","key":"9459_CR5"},{"doi-asserted-by":"crossref","unstructured":"Chargu\u00e9raud, A., Pottier, F.: Machine-checked verification of the correctness and amortized complexity of an efficient union-find implementation. In: Urban, C., Zhang, X. (eds.) ITP 2015, volume 9236 of LNCS, pp. 137\u2013153. Springer, Berlin (2015)","key":"9459_CR6","DOI":"10.1007\/978-3-319-22102-1_9"},{"key":"9459_CR7","volume-title":"Introduction to Algorithms","author":"TH Cormen","year":"1990","unstructured":"Cormen, T.H., Leiserson, C.E., Rivest, R.L.: Introduction to Algorithms. MIT Press, Cambridge (1990)"},{"doi-asserted-by":"crossref","unstructured":"Crary, K., Weirich, S.: Resource bound certification. In: Proceeding of the 27th Symposium on Principles of Programming Languages, POPL \u201900, pp. 184\u2013198. ACM (2000)","key":"9459_CR8","DOI":"10.1145\/325694.325716"},{"doi-asserted-by":"crossref","unstructured":"Danielsson, N. A.: Lightweight semiformal time complexity analysis for purely functional data structures. In: Proceeding of the 35th Symposium on Principles of Programming Languages, POPL \u201908, pp. 133\u2013144. ACM (2008)","key":"9459_CR9","DOI":"10.1145\/1328438.1328457"},{"doi-asserted-by":"crossref","unstructured":"Danner, N., Licata, D. R., Ramyaa, R.: Denotational cost semantics for functional languages with inductive types. In: Proceedings of the International Conference on Functional Programming, ICFP 2015, pp. 140\u2013151. ACM (2015)","key":"9459_CR10","DOI":"10.1145\/2784731.2784749"},{"doi-asserted-by":"crossref","unstructured":"Danner, N., Paykin, J., Royer, J.: A static cost analysis for a higher-order language. In: Proceeding of the Workshop Programming Languages Meets Program Verification, PLPV \u201913, pp. 25\u201334. ACM (2013)","key":"9459_CR11","DOI":"10.1145\/2428116.2428123"},{"issue":"1","key":"9459_CR12","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1016\/0304-3975(91)90145-R","volume":"79","author":"P Flajolet","year":"1991","unstructured":"Flajolet, P., Salvy, B., Zimmermann, P.: Automatic average-case analysis of algorithms. Theor. Comput. Sci. 79(1), 37\u2013109 (1991)","journal-title":"Theor. Comput. Sci."},{"issue":"1","key":"9459_CR13","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1007\/BF01840439","volume":"1","author":"ML Fredman","year":"1986","unstructured":"Fredman, M.L., Sedgewick, R., Sleator, D., Tarjan, R.: The pairing heap: a new form of self-adjusting heap. Algorithmica 1(1), 111\u2013129 (1986)","journal-title":"Algorithmica"},{"issue":"6","key":"9459_CR14","doi-asserted-by":"publisher","first-page":"1463","DOI":"10.1137\/100785351","volume":"40","author":"B Haeupler","year":"2011","unstructured":"Haeupler, B., Sen, S., Tarjan, R.E.: Rank-pairing heaps. SIAM J. Comput. 40(6), 1463\u20131485 (2011)","journal-title":"SIAM J. Comput."},{"doi-asserted-by":"crossref","unstructured":"Haftmann, F., Nipkow, T.: Code generation via higher-order rewrite systems. In: Blume, M., Kobayashi, N., Vidal, G. (eds.) Functional and Logic Programming (FLOPS 2010). Springer, Berlin (2010)","key":"9459_CR15","DOI":"10.1007\/978-3-642-12251-4_9"},{"doi-asserted-by":"crossref","unstructured":"Harrison, J.: Verifying nonlinear real formulas via sums of squares. In: Schneider, K., Brandt, J. (eds.) TPHOLs 2007, volume 4732 of LNCS, pp. 102\u2013118. Springer, Berlin (2007)","key":"9459_CR16","DOI":"10.1007\/978-3-540-74591-4_9"},{"issue":"1","key":"9459_CR17","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1145\/42267.42275","volume":"35","author":"T Hickey","year":"1988","unstructured":"Hickey, T., Cohen, J.: Automating program analysis. J. ACM 35(1), 185\u2013220 (1988)","journal-title":"J. ACM"},{"issue":"3","key":"9459_CR18","doi-asserted-by":"publisher","first-page":"14","DOI":"10.1145\/2362389.2362393","volume":"34","author":"J Hoffmann","year":"2012","unstructured":"Hoffmann, J., Aehlig, K., Hofmann, M.: Multivariate amortized resource analysis. ACM Trans. Program. Lang. Syst. 34(3), 14 (2012)","journal-title":"ACM Trans. Program. Lang. Syst."},{"doi-asserted-by":"crossref","unstructured":"Hoffmann, J., Das, A., Weng, S.-C.: Towards automatic resource bound analysis for OCaml. In: Proceeding of the 44th Symposium on Principles of Programming Languages, POPL \u201917, pp. 359\u2013373. ACM (2017)","key":"9459_CR19","DOI":"10.1145\/3009837.3009842"},{"doi-asserted-by":"crossref","unstructured":"Hofmann, M., Jost, S.: Static prediction of heap space usage for first-order functional programs. In: Proceeding of the 30th ACM Symposium Principles of Programming Languages, pp. 185\u2013197 (2003)","key":"9459_CR20","DOI":"10.1145\/604131.604148"},{"doi-asserted-by":"crossref","unstructured":"Hupel, L., Nipkow, T.: A verified compiler from Isabelle\/HOL to CakeML. In: Ahmed, A. (eds.) European Symposium on Programming (ESOP 2018), volume of LNCS, Springer, Berlin (2018)","key":"9459_CR21","DOI":"10.1007\/978-3-319-89884-1_35"},{"doi-asserted-by":"crossref","unstructured":"Iacono, J.: Improved upper bounds for pairing heaps. In: M. M. Halld\u00f3rsson (ed.) Algorithm Theory - SWAT 2000, volume 1851 of LNCS, pp. 32\u201345. Springer (2000)","key":"9459_CR22","DOI":"10.1007\/3-540-44985-X_5"},{"key":"9459_CR23","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 top-down skew heaps. Inf. Process. Lett. 37, 265\u2013271 (1991)","journal-title":"Inf. Process. Lett."},{"key":"9459_CR24","first-page":"589","volume-title":"Automated Reasoning (IJCAR 2006), volume 4130 of LNCS","author":"A Krauss","year":"2006","unstructured":"Krauss, A.: Partial recursive functions in higher-order logic. In: Furbach, U., Shankar, N. (eds.) Automated Reasoning (IJCAR 2006), volume 4130 of LNCS, pp. 589\u2013603. Springer, Berlin (2006)"},{"doi-asserted-by":"crossref","unstructured":"Kumar, R., Myreen, M. O., Norrish, M., Owens, S.: CakeML: A verified implementation of ML. In: Symposium Principles of Programming Languages, POPL \u201914, pp. 179\u2013191. ACM (2014)","key":"9459_CR25","DOI":"10.1145\/2535838.2535841"},{"issue":"2","key":"9459_CR26","doi-asserted-by":"publisher","first-page":"248","DOI":"10.1145\/42190.42347","volume":"10","author":"D M\u00e9tayer Le","year":"1988","unstructured":"Le M\u00e9tayer, D.: ACE: an automatic complexity evaluator. ACM Trans. Program. Lang. Syst. 10(2), 248\u2013266 (1988)","journal-title":"ACM Trans. Program. Lang. Syst."},{"doi-asserted-by":"crossref","unstructured":"Madhavan, R., Kulal, S., Kuncak, V.: Contract-based resource verification for higher-order functions with memoization. In: Principles of Programming Languages (POPL) (2017)","key":"9459_CR27","DOI":"10.1145\/3009837.3009874"},{"doi-asserted-by":"crossref","unstructured":"McCarthy, J. A., Fetscher, B., New, M. S., Feltey, D., Findler, R. B.: A Coq library for internal verification of running-times. In: Kiselyov, O., King, A. (eds.) Functional and Logic Programming (FLOPS 2016), volume 9613 of LNCS, pp. 144\u2013162. Springer, Berlin (2016)","key":"9459_CR28","DOI":"10.1007\/978-3-319-29604-3_10"},{"doi-asserted-by":"crossref","unstructured":"Nipkow, T.: Amortized complexity verified. Archive of Formal Proofs, 2014. Formal proof development. http:\/\/isa-afp.org\/entries\/Amortized_Complexity.shtml","key":"9459_CR29","DOI":"10.1007\/978-3-319-22102-1_21"},{"unstructured":"Nipkow, T.: Skew heap. Archive of Formal Proofs, 2014. Formal proof development. http:\/\/isa-afp.org\/entries\/Skew_Heap.shtml","key":"9459_CR30"},{"unstructured":"Nipkow, T.: Splay tree. Archive of Formal Proofs, 2014. Formal proof development. http:\/\/isa-afp.org\/entries\/Splay_Tree.shtml","key":"9459_CR31"},{"doi-asserted-by":"crossref","unstructured":"Nipkow, T.: Amortized complexity verified. In: Urban, C., Zhang, X. (eds.) Interactive Theorem Proving (ITP 2015), volume 9236 of LNCS, pp. 310\u2013324. Springer, Berlin (2015)","key":"9459_CR32","DOI":"10.1007\/978-3-319-22102-1_21"},{"doi-asserted-by":"crossref","unstructured":"Nipkow, T.: Automatic functional correctness proofs for functional search trees. In: Blanchette, J., Merz, S. (eds.) Interactive Theorem Proving (ITP 2016), LNCS. Springer, Berlin (2016)","key":"9459_CR33","DOI":"10.1007\/978-3-319-43144-4_19"},{"unstructured":"Nipkow, T.: Pairing heap. Archive of Formal Proofs (2016). Formal proof development. http:\/\/isa-afp.org\/entries\/Pairing_Heap.shtml","key":"9459_CR34"},{"doi-asserted-by":"crossref","unstructured":"Nipkow, T.: Verified root-balanced trees. In: Chang, B.-Y. E. (ed.) Asian Symposium on Programming Languages and Systems, APLAS 2017, volume 10695 of LNCS, pp. 255\u2013272. Springer, Berlin (2017)","key":"9459_CR35","DOI":"10.1007\/978-3-319-71237-6_13"},{"doi-asserted-by":"crossref","unstructured":"Nipkow, T., Klein, G.: Concrete Semantics with Isabelle\/HOL. Springer (2014). http:\/\/concrete-semantics.org","key":"9459_CR36","DOI":"10.1007\/978-3-319-10542-0"},{"doi-asserted-by":"crossref","unstructured":"Nipkow, T., Paulson, L., Wenzel, M.: Isabelle\/HOL\u2014A Proof Assistant for Higher-Order Logic, volume 2283 of LNCS. Springer, Berlin (2002)","key":"9459_CR37","DOI":"10.1007\/3-540-45949-9"},{"key":"9459_CR38","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511530104","volume-title":"Purely Functional Data Structures","author":"C Okasaki","year":"1998","unstructured":"Okasaki, C.: Purely Functional Data Structures. Cambridge University Press, Cambridge (1998)"},{"doi-asserted-by":"crossref","unstructured":"Sands, D.: Complexity analysis for a lazy higher-order language. In: Jones, N. (eds.) European Symposium on Programming (ESOP), volume 432 of LNCS, pp. 361\u2013376. Springer, Berlin (1990)","key":"9459_CR39","DOI":"10.1007\/3-540-52592-0_74"},{"key":"9459_CR40","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1016\/0020-0190(93)90249-9","volume":"45","author":"B Schoenmakers","year":"1993","unstructured":"Schoenmakers, B.: A systematic analysis of splaying. Inf. Process. Lett. 45, 41\u201350 (1993)","journal-title":"Inf. Process. Lett."},{"issue":"3","key":"9459_CR41","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 32(3), 652\u2013686 (1985)","journal-title":"J. ACM"},{"issue":"1","key":"9459_CR42","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)","journal-title":"SIAM J. Comput."},{"issue":"2","key":"9459_CR43","doi-asserted-by":"publisher","first-page":"306","DOI":"10.1137\/0606031","volume":"6","author":"RE Tarjan","year":"1985","unstructured":"Tarjan, R.E.: Amortized complexity. SIAM J. Algebraic. Disc. Meth. 6(2), 306\u2013318 (1985)","journal-title":"SIAM J. Algebraic. Disc. Meth."},{"doi-asserted-by":"crossref","unstructured":"Traytel, D., Berghofer, S., Nipkow, T.: Extending Hindley\u2013Milner type inference with coercive structural subtyping. In: Yang, H. (eds.) APLAS 2011, volume 7078 of LNCS, pp. 89\u2013104. Springer, Berlin (2011)","key":"9459_CR44","DOI":"10.1007\/978-3-642-25318-8_10"},{"doi-asserted-by":"crossref","unstructured":"Vasconcelos, P. B., Hammond, K.: Inferring cost equations for recursive, polymorphic and higher-order functional programs. In: Trinder, P., Michaelson, G., Pena, R. (eds.) Implementation of Functional Languages, IFL 2003, volume 3145 of LNCS, pp. 86\u2013101. Springer, Berlin (2004)","key":"9459_CR45","DOI":"10.1007\/978-3-540-27861-0_6"},{"issue":"9","key":"9459_CR46","doi-asserted-by":"publisher","first-page":"528","DOI":"10.1145\/361002.361016","volume":"18","author":"B Wegbreit","year":"1975","unstructured":"Wegbreit, B.: Mechanical program analysis. Commun. ACM 18(9), 528\u2013539 (1975)","journal-title":"Commun. ACM"},{"unstructured":"Wenzel, M.: Isabelle\/Isar\u2014A Versatile Environment for Human-Readable Formal Proof Documents. PhD thesis, Institut f\u00fcr Informatik, Technische Universit\u00e4t M\u00fcnchen (2002)","key":"9459_CR47"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-018-9459-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-018-9459-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-018-9459-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,12]],"date-time":"2019-10-12T15:56:27Z","timestamp":1570895787000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-018-9459-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,3,13]]},"references-count":47,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2019,3]]}},"alternative-id":["9459"],"URL":"https:\/\/doi.org\/10.1007\/s10817-018-9459-3","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2018,3,13]]},"assertion":[{"value":"31 March 2017","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"2 March 2018","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"13 March 2018","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}