Finger Trees: A Simple General-purpose Data Structure. Ralf Hinze and Ross Paterson J. Funct. Program. 16 (2), 2006, pp.197--217.
Dependent Finger Trees in Coq
We prove the correctness of an implementation of Finger Trees  in Coq, using Russell to develop the dependently typed programs associated with this datastructure. I've written a walkthrough  of the development. I also gave a talk  about it at TYPES'07.
Program-ing Finger Trees in Coq in ICFP'07: Proceedings of the 2007 ACM SIGPLAN International Conference on Functional Programming. Matthieu Sozeau. Freiburg, Germany:
ACM Press, 2007, pp.13--24.
ACM, 2007. This is the author's version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version was published in ICFP'07, http://doi.acm.org/10.1145/1291151.1291156
A journey with Russell: Programming Dependent Finger Trees in Coq. Matthieu Sozeau, Talk given at TYPES'07, Cividale Del Friuli, Italy, 2-5 May 2007.