# Functional Binomial Queues

 Title: Functional Binomial Queues Author: René Neumann (rene /dot/ neumann /at/ in /dot/ tum /dot/ de) Submission date: 2010-10-28 Abstract: 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. BibTeX: @article{Binomial-Queues-AFP, author = {René Neumann}, title = {Functional Binomial Queues}, journal = {Archive of Formal Proofs}, month = oct, year = 2010, note = {\url{https://isa-afp.org/entries/Binomial-Queues.html}, Formal proof development}, ISSN = {2150-914x}, } License: BSD License Status: [ok] This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.