Amortized Complexity Verified

Tobias Nipkow

7 July 2014


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.

BSD License

Change history

[2015-03-17] Added pairing heaps by Hauke Brinkop.
[2016-07-12] Moved splay heaps from here to Splay_Tree
[2016-07-14] Moved pairing heaps from here to the new Pairing_Heap

Depends On

Used by


Related Entries