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 [1] in Coq,
using Russell to develop the dependently typed programs associated
with this datastructure.
I've written a walkthrough [2] of the
development. I also gave a talk [3] 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.
