|
Finger
Trees
Title: |
Finger Trees |
Authors:
|
Benedikt Nordhoff (b /dot/ n /at/ wwu /dot/ de),
Stefan Körner (s_koer03 /at/ uni-muenster /dot/ de) and
Peter Lammich (lammich /at/ in /dot/ tum /dot/ de)
|
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{https://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.
|
|