Priority Queues Based on Braun Trees

Tobias Nipkow 🌐

September 4, 2014

Abstract

This entry verifies priority queues based on Braun trees. Insertion and deletion take logarithmic time and preserve the balanced nature of Braun trees. Two implementations of deletion are provided.

License

BSD License

History

December 16, 2019
Added theory Priority_Queue_Braun2 with second version of del_min

Topics

Related publications

Session Priority_Queue_Braun

Cite

× 
@article{Priority_Queue_Braun-AFP,
  author  = {Tobias Nipkow},
  title   = {Priority Queues Based on Braun Trees},
  journal = {Archive of Formal Proofs},
  month   = {September},
  year    = {2014},
  note    = {\url{https://isa-afp.org/entries/Priority_Queue_Braun.html},
             Formal proof development},
  ISSN    = {2150-914x},
}
Download

Download

× Download latest

Older releases: