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.

License

BSD License

Topics

Related publications

Session Skew_Heap

Used by

Cite

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

Download

× Download latest

Older releases: