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.


BSD License


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.


Related publications

Session Amortized_Complexity