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 PAA12509; Tue, 21 Sep 2004 15:34:59 +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 PAA11365 for ; Tue, 21 Sep 2004 15:34:58 +0200 (MET DST) Received: from post.bourget.univ-savoie.fr (post.bourget.univ-savoie.fr [193.48.120.73]) by nez-perce.inria.fr (8.13.0/8.13.0) with ESMTP id i8LDYvNk024033 (version=TLSv1/SSLv3 cipher=EDH-RSA-DES-CBC3-SHA bits=168 verify=NO) for ; Tue, 21 Sep 2004 15:34:58 +0200 Received: from univ-savoie.fr (d85.lama.univ-savoie.fr [193.48.123.85]) by post.bourget.univ-savoie.fr (8.12.3/jtpda-5.4) with ESMTP id i8LDYmsO006145 ; Tue, 21 Sep 2004 15:34:48 +0200 Message-ID: <41502DFB.4070300@univ-savoie.fr> Date: Tue, 21 Sep 2004 15:34:51 +0200 From: Christophe Raffalli User-Agent: Mozilla/5.0 (X11; U; Linux i686; en-US; rv:1.6) Gecko/20040115 X-Accept-Language: en-us, en MIME-Version: 1.0 To: willb@cs.wisc.edu CC: caml-list@inria.fr Subject: Re: [Caml-list] ACL2 equivalent in Caml? References: In-Reply-To: X-Enigmail-Version: 0.83.3.0 X-Enigmail-Supports: pgp-inline, pgp-mime Content-Type: multipart/signed; micalg=pgp-sha1; protocol="application/pgp-signature"; boundary="------------enig213676CDC33DA706AC8444E1" Content-Transfer-Encoding: 8bit X-Scanned-By: MIMEDefang 2.33 (www . roaringpenguin . com / mimedefang) X-Miltered: at nez-perce with ID 41502E01.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Loop: caml-list@inria.fr X-Spam: no; 0.00; raffalli:01 raffalli:01 univ-savoie:01 caml-list:01 openpgp:01 2440:01 3156:01 benton:01 phox:01 savoie:01 chablais:01 73376:01 univ-savoie:01 lama:01 enigmail:01 X-Attachments: type="application/pgp-signature" name="signature.asc" name="signature.asc" Sender: owner-caml-list@pauillac.inria.fr Precedence: bulk This is an OpenPGP/MIME signed message (RFC 2440 and 3156) --------------enig213676CDC33DA706AC8444E1 Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 8bit Will Benton wrote: > Hello, > > 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? > > I have a preliminary tool using PhoX for this (without modules, but with full pattern-matching). Mail me privately (or not privately) if you want more details. It is based on the idea of Sylvain Baro's phd and he also has an implementation. Mail Pascal Manoury (at Jussieu) for more info on his system. -- Christophe Raffalli Université de Savoie Batiment Le Chablais, bureau 21 73376 Le Bourget-du-Lac Cedex tél: (33) 4 79 75 81 03 fax: (33) 4 79 75 87 42 mail: Christophe.Raffalli@univ-savoie.fr www: http://www.lama.univ-savoie.fr/~RAFFALLI --------------------------------------------- IMPORTANT: this mail is signed using PGP/MIME At least Enigmail/Mozilla, mutt or evolution can check this signature --------------------------------------------- --------------enig213676CDC33DA706AC8444E1 Content-Type: application/pgp-signature; name="signature.asc" Content-Description: OpenPGP digital signature Content-Disposition: attachment; filename="signature.asc" -----BEGIN PGP SIGNATURE----- Version: GnuPG v1.2.4 (GNU/Linux) Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org iD8DBQFBUC4ESQDyWB/+xBwRArQxAJwPVaK9ucPdjsekWcke+14m7ouuQACff0bV Yjb3kI2YkNZy3QunWv30yzM= =CvBE -----END PGP SIGNATURE----- --------------enig213676CDC33DA706AC8444E1-- ------------------- 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