Formalisation d'une structure de données union-find persistante en Coq

• A Persistent Union-Find Data Structure (Workshop on ML 2007)
• Version française : Union-Find Persistant (PostScript) / Transparents (PDF)

Bibliothèques OCaml:

• Parray : Tableaux peristants (.mli / .ml)
• Puf : Union-Find persistant (.mli / .ml)

Le code présenté dans cet article a été formellement prouvé avec l'assistant de preuve Coq :

• Parcourir la formalisation (ou télécharger puf.v)

Fichiers Ocaml utilisés pour les tests présentés dans l'article

• Parcourir les fichiers
• Archive : bench.tar.gz ; une fois décompressée, faire ./configure, make et ./bench.opt