Priority Queues Based on Braun Trees

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.

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

Computer science/Data structures

Related publications

Nipkow, T., & Sewell, T. (2020). Proof pearl: Braun trees. Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, 18–31. https://doi.org/10.1145/3372885.3373834
Author's copy
Chapter Priority Queues via Braun Trees in Functional Data Structures and Algorithms

Session Priority_Queue_Braun

Priority_Queue_Braun
Priority_Queue_Braun2
Sorting_Braun