Functional Binomial Queues

RenĂ© Neumann đŸ“§

October 28, 2010

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


Priority queues are an important data structure and efficient implementations of them are crucial. We implement a functional variant of binomial queues in Isabelle/HOL and show its functional correctness. A verification against an abstract reference specification of priority queues has also been attempted, but could not be achieved to the full extent.


BSD License


Session Binomial-Queues