Finger Trees

Title:	Finger Trees
Authors:	Benedikt Nordhoff (b_nord01 /at/ uni-muenster /dot/ de), Stefan Körner (s_koer03 /at/ uni-muenster /dot/ de) and Peter Lammich
Submission date:	2010-10-28
Abstract:	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 Hinze and Paterson. The code generator can be used to get efficient, verified code.
BibTeX:	@article{Finger-Trees-AFP, author = {Benedikt Nordhoff and Stefan Körner and Peter Lammich}, title = {Finger Trees}, journal = {Archive of Formal Proofs}, month = oct, year = 2010, note = {\url{http://isa-afp.org/entries/Finger-Trees.html}, Formal proof development}, ISSN = {2150-914x}, }
License:	BSD License
Used by:	Collections, Containers, JinjaThreads
Status: [ok]	This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.