Skew Heap

Tobias Nipkow 🌐

August 13, 2014

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.

Abstract

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.

BSD License

Topics

Theories of Skew_Heap