* [Caml-list] formal proof of ocaml's Set module
@ 2003-07-15 11:35 Jean-Christophe Filliatre
2003-07-15 18:40 ` Ken Rose
0 siblings, 1 reply; 2+ messages in thread
From: Jean-Christophe Filliatre @ 2003-07-15 11:35 UTC (permalink / raw)
To: caml-list
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
^ permalink raw reply [flat|nested] 2+ messages in thread
* Re: [Caml-list] formal proof of ocaml's Set module
2003-07-15 11:35 [Caml-list] formal proof of ocaml's Set module Jean-Christophe Filliatre
@ 2003-07-15 18:40 ` Ken Rose
0 siblings, 0 replies; 2+ messages in thread
From: Ken Rose @ 2003-07-15 18:40 UTC (permalink / raw)
To: Jean-Christophe Filliatre; +Cc: caml-list
Jean-Christophe Filliatre wrote:
> http://www.lri.fr/~filliatr/fsets/
This link doesn't work right
- ken
-------------------
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
^ permalink raw reply [flat|nested] 2+ messages in thread
end of thread, other threads:[~2003-07-15 18:40 UTC | newest]
Thread overview: 2+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2003-07-15 11:35 [Caml-list] formal proof of ocaml's Set module Jean-Christophe Filliatre
2003-07-15 18:40 ` Ken Rose
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).