From: Jean-Christophe Filliatre <Jean-Christophe.Filliatre@lri.fr>
To: willb@cs.wisc.edu
Cc: caml-list@inria.fr
Subject: Re: [Caml-list] ACL2 equivalent in Caml?
Date: Tue, 21 Sep 2004 09:08:24 +0200 [thread overview]
Message-ID: <16719.54120.335633.398220@gargle.gargle.HOWL> (raw)
In-Reply-To: <f3e76cab040917083711002157@mail.gmail.com>
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
next prev parent reply other threads:[~2004-09-21 7:08 UTC|newest]
Thread overview: 4+ messages / expand[flat|nested] mbox.gz Atom feed top
2004-09-17 15:37 Will Benton
2004-09-21 7:08 ` Jean-Christophe Filliatre [this message]
2004-09-21 13:34 ` Christophe Raffalli
2004-09-21 15:04 ` [Caml-list] " Will Benton
Reply instructions:
You may reply publicly to this message via plain-text email
using any one of the following methods:
* Save the following mbox file, import it into your mail client,
and reply-to-all from there: mbox
Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
--in-reply-to=16719.54120.335633.398220@gargle.gargle.HOWL \
--to=jean-christophe.filliatre@lri.fr \
--cc=caml-list@inria.fr \
--cc=willb@cs.wisc.edu \
/path/to/YOUR_REPLY
https://kernel.org/pub/software/scm/git/docs/git-send-email.html
* If your mail client supports setting the In-Reply-To header
via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).