Browse thread
[Caml-list] ACL2 equivalent in Caml?
-
Will Benton
- Jean-Christophe Filliatre
- Christophe Raffalli
- Will Benton
[
Home
]
[ Index:
by date
|
by threads
]
[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: | 2004-09-21 (07:08) |
From: | Jean-Christophe Filliatre <Jean-Christophe.Filliatre@l...> |
Subject: | Re: [Caml-list] ACL2 equivalent in Caml? |
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