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.
July 14, 2016Moved pairing heaps from here to the new Pairing_Heap
July 12, 2016Moved splay heaps from here to Splay_Tree
March 17, 2015Added pairing heaps by Hauke Brinkop.
Theories of Amortized_Complexity