Formalisation d'une bibliothèque d'ensembles finis en Coq

Auteurs: Pierre Letouzey and Jean-Christophe Filliâtre

Cette page présente une formalisation dans l'assistant de preuve Coq d'une bibliothèque d'ensemble finis. Elle contient en fait trois codages différents des ensembles finis : à l'aide de listes triées, d'arbres rouges et noirs et d'AVLs. Cette formalisation fait un grand usage des modules et des foncteurs, une nouveauté de Coq 7.4, et en démontre la puissance en tant qu'outil de preuve autant qu'en tant qu'outil de programmation.

Transparents en Français : Active DVI et PostScript (exposé du 3 juillet 2003)
Rapport de recherche LRI : Functors for Proofs and Programs (PostScript file). Sera présenté à ESOP 2004

Code Ocaml de départ

Code Ocaml obtenu par extraction

Sources Coq


American Generated on 1/12/2021.