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.

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.

License

BSD License

Topics

Session Binomial-Queues

Cite

× 
@article{Binomial-Queues-AFP,
  author  = {René Neumann},
  title   = {Functional Binomial Queues},
  journal = {Archive of Formal Proofs},
  month   = {October},
  year    = {2010},
  note    = {\url{https://isa-afp.org/entries/Binomial-Queues.html},
             Formal proof development},
  ISSN    = {2150-914x},
}
Download

Download

× Download latest

Older releases: