Formalization of a finite sets library in Coq

Authors: Pierre Letouzey and Jean-Christophe Filliātre

This page presents the formalization in the Coq proof assistant of a finite sets library. It actually contains three different implementations of finite sets: using ordered lists, red-black trees and AVLs. This formalization heavily uses modules and functors, a novelty in Coq 7.4, demonstrating their power in the context of proof, as well as in the context of programming.

LRI Research report: Functors for Proofs and Programs (PostScript file). To be presented at ESOP 2004

Original Ocaml code

Ocaml code obtained by extraction

Coq sources

Franēais Generated on 25/3/2017.