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.
- 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.
- Nipkow, T., & Brinkop, H. (2018). Amortized Complexity Verified. Journal of Automated Reasoning, 62(3), 367–391. https://doi.org/10.1007/s10817-018-9459-3
- Author's copy