Email Gateway (Aug 18 2022 at 16:17): Email Gateway (Aug 18 2022 at 16:17):From: Tobias Nipkow <nipkow@in.tum.de>
We have received 3 new AFP entries yesterday, among them 2 for binomial
heaps!
Binomial Heaps and Skew Binomial Heaps
Rene Meis, Finn Nielsen and Peter Lammich
http://afp.sourceforge.net/entries/Binomial-Heaps.shtml
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.
Finger Trees
Benedikt Nordhoff, Stefan Körner and Peter Lammich
http://afp.sourceforge.net/entries/Finger-Trees.shtml
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
code.
Only in the development version of the AFP:
Functional Binomial Queues
René Neumann
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.
Many thanks to the authors!
Last updated: Apr 26 2024 at 08:19 UTC