Version franēaise
Home     About     Download     Resources     Contact us    

This site is updated infrequently. For up-to-date information, please visit the new OCaml website at

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: 2003-07-15 (11:42)
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

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

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 Archives:
Bug reports: FAQ:
Beginner's list: