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 (.ml / .mli)
• Puf : Union-Find persistant (.ml / .mli)

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