Skew heaps are an amazingly simple and lightweight implementation of priority queues. They were invented by Sleator and Tarjan [SIAM 1986] and have logarithmic amortized complexity. This entry provides executable and verified functional skew heaps.
The amortized complexity of skew heaps is analyzed in the AFP entry Amortized Complexity.
- Skew Heaps in Functional Algorithms, Verified!