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 nontrivial 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.isaafp.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.68059 Nipkow, 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 (68XX) 
1  Mathematical logic and foundations (03XX) 
1  Combinatorics (05XX) 
1  Operations research, mathematical programming (90XX) 