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 [1] of the development. I also gave a talk [2] about it at TYPES'07.
Here's the
coqdoc
generated documentation. You can also browse the sources.
1
Program-ing Finger Trees in Coq in ICFP'07. Matthieu Sozeau. Freiburg, Germany: ACM Press, 2007, pp.13-24.
2
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.
Valid XHTML 1.1! Valid CSS!