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.
- 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
- Chapter Skew Heaps in Functional Data Structures and Algorithms