[Axiom-developer] Ocaml, Coq, and ACL2

[Page, Bill]

On Wednesday, October 19, 2005 9:52 AM C Y wrote:
> ... 
> With apologies to Camm, there is one sense in which arriving at
> ocaml is neither full circle nor unattractive, and that is the
> coq theorem prover.  If there is indeed serious interest in
> backing Axiom with a powerful theorem prover, COQ is definitely
> up there on the list of candidates.  In fact, some work was done
> in France a while back on coq+Axiom - as yet I have not yet
> located a copy of that thesis, unfortunately.

I already have Ocaml and Coq running on the axiom-developer.org
server. If there is some interest, it would not be difficult for
me to provide:

\begin{ocaml}
...
\end{ocaml}

and

\begin{coq}
...
\end{coq}

on MathAction to allow these to be accessed through the web
like {axiom} {spad} {aldor} and {reduce}. This would not
provide axiom/coq integration as such, but at least it would
provide the possibility of exhibiting a coq proof along with
some Axiom code should an author wish to do that.

> I think I posted here about it and got no response.

I am definitely interested by lack time right now to do
anything serious.

> ... 
> I know the interest in this topic is spotty, but this is the
> time and place to raise the question - if we DO want to be
> able to back Axiom with formal provers, what are the design
> considerations that need to be taken into account?  What
> precisely will the prover be used to do, how would we interact
> with it, and how would we store and use the results?

As you know, I am rather put-off by just "talking" about doing
these things. Since quite a lot of code is freely available and
easily accessed, I would prefer to just to dig-in and work/play
with one or more of these tools ... then, maybe later, decide on
which might be best and what if anything we really want to do
with Axiom and theorem proving software.

The "other" proof system is obviously of interest would be ACL2.
Camm and some of the other lisp developer have a good connection
to that project and so if we were to work with ACL2 and Axiom,
I think we could expect a lot of support.

So far I have not installed ACL2 on the axiom-developer server
yet, but if even one other person says they are interested then
I would be glad to do that and also make in available on MathAction
via

\begin{acl2}
...
\end{acl2}

Regards,
Bill Page