Version franēaise
Home     About     Download     Resources     Contact us    
Browse thread
[Caml-list] formal proof of ocaml's Set module
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: -- (:)
From: Jean-Christophe Filliatre <Jean-Christophe.Filliatre@l...>
Subject: [Caml-list] formal proof of ocaml's Set module 

Dear all,

For those interested about formal  proofs: ocaml's Set module has been
formally proved correct using the  Coq proof assistant. Details can be
checked out from http://www.lri.fr/~filliatr/fsets/

During  the process  of verification,  two small  mistakes  were found
(AVLs incorrectly  balanced), which are  already fixed in  ocaml's CVS
sources.

This formalization also includes  the developement and formal proof of
a similar library (i.e. same interface) using red-black trees.

-- 
Jean-Christophe Filliātre

-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners