Reference:

Rene Neumann. Functional binomial queues. Archive of Formal Proofs, October 2010. Formal proof development.

Suggested BibTeX entry:

@article{Binomial-Queues-AFP,
    author = {Rene Neumann},
    journal = {Archive of Formal Proofs},
    month = {October},
    note = {Formal proof development},
    title = {Functional Binomial Queues},
    year = {2010}
}