This library defines three different versions of pairing heaps: a functional version of the original design based on binary trees [Fredman et al. 1986], the version by Okasaki  and a modified version of the latter that is free of structural invariants.
The amortized complexity of pairing heaps is analyzed in the AFP article Amortized Complexity.
Origin: This library was extracted from Amortized Complexity and extended.
- Pairing Heaps in Functional Algorithms, Verified!