Priority Queues Based on Braun Trees

 

Title: Priority Queues Based on Braun Trees
Author: Tobias Nipkow
Submission date: 2014-09-04
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.
Change history: [2019-12-16]: Added theory Priority_Queue_Braun2 with second version of del_min
BibTeX:
@article{Priority_Queue_Braun-AFP,
  author  = {Tobias Nipkow},
  title   = {Priority Queues Based on Braun Trees},
  journal = {Archive of Formal Proofs},
  month   = sep,
  year    = 2014,
  note    = {\url{http://isa-afp.org/entries/Priority_Queue_Braun.html},
            Formal proof development},
  ISSN    = {2150-914x},
}
License: BSD License