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