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 JAA26284; Tue, 21 Sep 2004 09:08:26 +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 JAA26861 for ; Tue, 21 Sep 2004 09:08:25 +0200 (MET DST) Received: from ext.lri.fr (ext.lri.fr [129.175.15.4]) by nez-perce.inria.fr (8.13.0/8.13.0) with ESMTP id i8L78OVZ000385 (version=TLSv1/SSLv3 cipher=EDH-RSA-DES-CBC3-SHA bits=168 verify=NO) for ; Tue, 21 Sep 2004 09:08:24 +0200 Received: from localhost (localhost [127.0.0.1]) by ext.lri.fr (Postfix) with ESMTP id 9CD7719E6F7; Tue, 21 Sep 2004 09:08:24 +0200 (CEST) Received: from ext.lri.fr ([127.0.0.1]) by localhost (ext.lri.fr [127.0.0.1]) (amavisd-new, port 10024) with ESMTP id 24654-06; Tue, 21 Sep 2004 09:08:24 +0200 (CEST) Received: from smtp.lri.fr (serveur3-5 [129.175.3.5]) by ext.lri.fr (Postfix) with ESMTP id 87F5E19E6DE; Tue, 21 Sep 2004 09:08:24 +0200 (CEST) Received: from pc8-142 (pc8-142 [129.175.8.142]) by smtp.lri.fr (Postfix) with ESMTP id 744B6CEE04; Tue, 21 Sep 2004 09:08:24 +0200 (CEST) Received: from filliatr by pc8-142 with local (Exim 3.36 #1 (Debian)) id 1C9elE-0006qX-00; Tue, 21 Sep 2004 09:08:24 +0200 MIME-Version: 1.0 Content-Type: text/plain; charset=iso-8859-1 Content-Transfer-Encoding: 8bit Message-ID: <16719.54120.335633.398220@gargle.gargle.HOWL> Date: Tue, 21 Sep 2004 09:08:24 +0200 To: willb@cs.wisc.edu Cc: caml-list@inria.fr Subject: Re: [Caml-list] ACL2 equivalent in Caml? In-Reply-To: References: X-Mailer: VM 7.18 under Emacs 21.3.1 From: Jean-Christophe Filliatre X-Virus-Scanned: by amavisd-new at lri.fr X-Miltered: at nez-perce with ID 414FD368.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Loop: caml-list@inria.fr X-Spam: no; 0.00; caml-list:01 filliatre:01 filliatre:01 lri:01 benton:01 tactics:99 lri:01 filliatr:01 hol-light:01 caml:01 caml:01 lisp:01 writes:01 coq:02 coq:02 Sender: owner-caml-list@pauillac.inria.fr Precedence: bulk Will Benton writes: > > I'm looking for an automated reasoning system like Moore's ACL2, > except using the pure subset of Caml instead of pure Lisp. Does such > a tool exist? There are (at least) three proof assistants written in Caml, namely Coq, HOL Light and MetaPRL (URLs below). Caml is their metalanguage, that is you can write proof tactics in Caml for instance. But contrary to ACL2 these are not _directly_ programming languages on which you can reason about. Yet you can use these systems to prove programs correct. Coq for instance (this is the one I know) has an extraction mechanism which automatically generates Caml programs from constructive proofs of their specifications, thus correct by construction. Regards, -- Jean-Christophe Filliātre (http://www.lri.fr/~filliatr) http://coq.inria.fr/ http://www.cl.cam.ac.uk/users/jrh/hol-light/ http://cvs.metaprl.org:12000/metaprl/default.html ------------------- 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