Pairing Heap

Hauke Brinkop 📧 and Tobias Nipkow 🌐

July 14, 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

Extra 0

Origin: This library was extracted from Amortized Complexity and extended.

Topics

Theories of Pairing_Heap

Used by

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{https://isa-afp.org/entries/Pairing_Heap.html},
            Formal proof development},
  ISSN    = {2150-914x},
}
Download

Download

× Download latest