Priority Queues Based on Braun Trees

Tobias Nipkow 🌐

September 4, 2014

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


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.


BSD License


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


Related publications

Session Priority_Queue_Braun