[isabelle] New AFP entries for functional data structures
We have received 3 new AFP entries yesterday, among them 2 for binomial
Binomial Heaps and Skew Binomial Heaps
Rene Meis, Finn Nielsen and Peter Lammich
We implement and prove correct binomial heaps and skew binomial heaps.
Both are data-structures for priority queues. While binomial heaps have
logarithmic findMin, deleteMin, insert, and meld operations, skew
binomial heaps have constant time findMin, insert, and meld operations,
and only the deleteMin-operation is logarithmic. This is achieved by
using skew links to avoid cascading linking on insert-operations, and
data-structural bootstrapping to get constant-time findMin and meld
operations. Our implementation follows the paper by Brodal and Okasaki.
Benedikt Nordhoff, Stefan Körner and Peter Lammich
We implement and prove correct 2-3 finger trees. Finger trees are a
general purpose data structure, that can be used to efficiently
implement other data structures, such as priority queues. Intuitively, a
finger tree is an annotated sequence, where the annotations are elements
of a monoid. Apart from operations to access the ends of the sequence,
the main operation is to split the sequence at the point where a
monotone predicate over the sum of the left part of the sequence becomes
true for the first time. The implementation follows the paper of Hintze
and Paterson. The code generator can be used to get efficient, verified
Only in the development version of the AFP:
Functional Binomial Queues
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
Many thanks to the authors!
This archive was generated by a fusion of
Pipermail (Mailman edition) and