Amortized Complexity swMATH ID: 28606 Software Authors: Tobias Nipkow Description: Amortized Complexity Verified. A framework for the analysis of the amortized complexity of functional data structures is formalized in Isabelle/HOL and applied to a number of standard examples and to the folowing non-trivial ones: skew heaps, splay trees, splay heaps and pairing heaps. A preliminary version of this work (without pairing heaps) is described in a paper published in the proceedings of the conference on Interactive Theorem Proving ITP 2015. An extended version of this publication is available here. Homepage: https://www.isa-afp.org/entries/Amortized_Complexity.html Dependencies: Isabelle Related Software: Isabelle/HOL; Archive Formal Proofs; HOL; Isabelle; Coq; Root Balanced Tree; Density Compiler; Random BSTs; Treaps; QuickSort Cost; CryptHOL; Ergodic theory; Splay Tree; ACE; OCaml; Separation Logic; Isar; TcT; OptiMathSAT; TiML Cited in: 8 Publications Standard Articles 1 Publication describing the Software, including 1 Publication in zbMATH Year Amortized complexity verified. Zbl 1465.68059Nipkow, Tobias 2015 all top 5 Cited by 11 Authors 5 Nipkow, Tobias 2 Eberl, Manuel 2 Haslbeck, Max W. 1 Brinkop, Hauke 1 Charguéraud, Arthur 1 Lammich, Peter 1 Leutgeb, Lorenz 1 Moser, Georg 1 Pottier, François 1 Sefidgar, S. Reza 1 Zuleger, Florian Cited in 1 Serial 4 Journal of Automated Reasoning Cited in 4 Fields 8 Computer science (68-XX) 1 Mathematical logic and foundations (03-XX) 1 Combinatorics (05-XX) 1 Operations research, mathematical programming (90-XX) Citations by Year