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.
- December 16, 2019
- Added theory Priority_Queue_Braun2 with second version of del_min
- Nipkow, T., & Sewell, T. (2020). Proof pearl: Braun trees. Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs. https://doi.org/10.1145/3372885.3373834
- Open access