Amortized Complexity Verified

Tobias Nipkow 🌐

July 7, 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

July 14, 2016

Moved pairing heaps from here to the new Pairing_Heap

July 12, 2016

Moved splay heaps from here to Splay_Tree

March 17, 2015

Added pairing heaps by Hauke Brinkop.


Theories of Amortized_Complexity