Skew Heap

Tobias Nipkow

13 August 2014

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

Used by

Topics

Related Entries

Theories

Cite

×
@article{Skew_Heap-AFP,
  author  = {Tobias Nipkow},
  title   = {Skew Heap},
  journal = {Archive of Formal Proofs},
  month   = August,
  year    = 2014,
  note    = {\url{http://isa-afp.org/entries/Skew_Heap.html},
            Formal proof development},
  ISSN    = {2150-914x},
}
Download