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