Formalization of a persistent union-find data structure in Coq

• A Persistent Union-Find Data Structure (Workshop on ML 2007)
• French version : Union-Find Persistant (PostScript) / Slides (PDF)

Related Ocaml data structures:

• Parray : Persistent arrays (.ml / .mli)
• Puf : Persistent Union-Find (.ml / .mli)

The code presented in this article has been formally proved using the Coq proof assistant :

• Browse the Coq sources (or download puf.v)

Ocaml files used to make the benchmarks presented in the article

• Browse the files
• Archive : bench.tar.gz ; once uncompressed, do ./configure, make and ./bench.opt