From mboxrd@z Thu Jan 1 00:00:00 1970 Received: (from majordomo@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id NAA07941; Tue, 15 Jul 2003 13:42:16 +0200 (MET DST) X-Authentication-Warning: pauillac.inria.fr: majordomo set sender to owner-caml-list@pauillac.inria.fr using -f Received: from nez-perce.inria.fr (nez-perce.inria.fr [192.93.2.78]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id NAA25662 for ; Tue, 15 Jul 2003 13:42:15 +0200 (MET DST) Received: from lri.lri.fr (lri.lri.fr [129.175.15.1]) by nez-perce.inria.fr (8.11.1/8.11.1) with ESMTP id h6FBgET20699 for ; Tue, 15 Jul 2003 13:42:14 +0200 (MET DST) Received: from pc8-123 (pc8-123 [129.175.8.123]) by lri.lri.fr (8.11.6p2/jtpda-5.3.2) with ESMTP id h6FBZxt22472 for ; Tue, 15 Jul 2003 13:35:59 +0200 (MEST) Received: from filliatr by pc8-123 with local (Exim 3.35 #1 (Debian)) id 19cO6A-0002Zv-00 for ; Tue, 15 Jul 2003 13:35:58 +0200 From: Jean-Christophe Filliatre MIME-Version: 1.0 Content-Type: text/plain; charset=iso-8859-1 Content-Transfer-Encoding: 8bit Message-ID: <16147.59166.784838.587663@gargle.gargle.HOWL> Date: Tue, 15 Jul 2003 13:35:58 +0200 To: caml-list@inria.fr Subject: [Caml-list] formal proof of ocaml's Set module X-Mailer: VM 7.03 under Emacs 20.7.2 Reply-To: Jean-Christophe.Filliatre@lri.fr (Jean-Christophe Filliatre) X-MailScanner: Found to be clean X-Loop: caml-list@inria.fr X-Spam: no; 0.00; filliatre:01 lri:01 ocaml's:01 filliatr:01 incorrectly:01 developement:01 red-black:01 coq:02 module:03 interface:03 library:03 proofs:05 cvs:05 balanced:07 www:91 Sender: owner-caml-list@pauillac.inria.fr Precedence: bulk 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