Pairing Heap

Hauke Brinkop and Tobias Nipkow

14 July 2016

Abstract

This library defines three different versions of pairing heaps: a functional version of the original design based on binary trees [Fredman et al. 1986], the version by Okasaki [1998] and a modified version of the latter that is free of structural invariants.

The amortized complexity of pairing heaps is analyzed in the AFP article Amortized Complexity.

BSD License

Origin

This library was extracted from Amortized Complexity and extended.

Used by

Topics

Theories

Cite

×
@article{Pairing_Heap-AFP,
  author  = {Hauke Brinkop and Tobias Nipkow},
  title   = {Pairing Heap},
  journal = {Archive of Formal Proofs},
  month   = July,
  year    = 2016,
  note    = {\url{http://isa-afp.org/entries/Pairing_Heap.html},
            Formal proof development},
  ISSN    = {2150-914x},
}
Download