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

L'article suivant présente une structure de données persistante pour le problème union-find :

Bibliothèques Ocaml:

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

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


American Homepage Generated on 9/4/2014.