*To*: Isabelle <cl-isabelle-users at lists.cam.ac.uk>*Subject*: [isabelle] New AFP entries for functional data structures*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Thu, 28 Oct 2010 18:07:24 +0200*User-agent*: Thunderbird 2.0.0.24 (Macintosh/20100228)

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!

- Previous by Date: Re: [isabelle] installing Isabelle under polyml-5
- Next by Date: Re: [isabelle] Advertise your work on the mailing list
- Previous by Thread: Re: [isabelle] Isabelle 2009-2, ProofGeneral, xemacs under CygWin with XWin
- Next by Thread: [isabelle] Specializing types in locales
- Cl-isabelle-users October 2010 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list