Abstract: |
We implement and prove correct binomial heaps and skew binomial heaps.
Both are data-structures for priority queues.
While binomial heaps have logarithmic findMin, deleteMin,
insert, and meld operations,
skew binomial heaps have constant time findMin, insert,
and meld operations, and only the deleteMin-operation is
logarithmic. This is achieved by using skew links to avoid
cascading linking on insert-operations, and data-structural
bootstrapping to get constant-time findMin and meld
operations. Our implementation follows the paper by Brodal and Okasaki. |
BibTeX: |
@article{Binomial-Heaps-AFP,
author = {Rene Meis and Finn Nielsen and Peter Lammich},
title = {Binomial Heaps and Skew Binomial Heaps},
journal = {Archive of Formal Proofs},
month = oct,
year = 2010,
note = {\url{http://isa-afp.org/entries/Binomial-Heaps.shtml},
Formal proof development},
ISSN = {2150-914x},
}
|