Guyslain Naves & Arnaud Spiwack
Starting with an algorithm to turn lists into full trees which uses non-obvious invariants and partial functions, we progressively encode the invariants in the types of the data, removing most of the burden of a correctness proof.
The invariants are encoded using non-uniform inductive types which parallel numerical representations in a style advertised by Okasaki, and a small amount of dependent types.
The source files containing the full programs in Ocaml and Coq can be found in the src repository.
To build the article, you need to have a Latex distribution installed, as well as Ocaml (version 3.12 or later) and the melt text processing tool. The command line to run is ocamlbuild fulltrees.pdf. You can then find the pdf file in _build/fulltrees.pdf
The content of this repository is distributed under Creative Commons licence CC BY 3.0.