Functional Binomial Queues

RenĂ© Neumann đŸ“§

October 28, 2010


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