An implementation and a proof of a purely functional data structure that combines the benefits of a list and an array. Everything is done in Coq and then extracted in OCaml. Dependent types are used to guide the thinking process, get a shorter development and more efficient extraction.
Source code in Coq: theories.
Extraction to OCaml: extraction.
Paper: paper/main.pdf.