Finger Trees

Benedikt Nordhoff 📧, Stefan Körner 📧 and Peter Lammich 🌐

October 28, 2010

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


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.


BSD License


Session Finger-Trees