[Top][All Lists]

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Axiom-developer] Re: Ocaml, Coq, and ACL2

From: C Y
Subject: [Axiom-developer] Re: Ocaml, Coq, and ACL2
Date: Thu, 20 Oct 2005 09:33:56 -0700 (PDT)

--- "Page, Bill" <address@hidden> wrote:

> I already have Ocaml and Coq running on the
> server. If there is some interest, it would not be difficult for
> me to [snip] 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.

Sounds interesting, but it might not be needed for a while yet, if at
all - I certainly have a long learning curve ahead of me with regards
to coq.  

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

Know that feeling...

> 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.

Fair enough.  OK, I'll start digging.

> 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.

Yes, ACL2 and HOL were my other main interests in this department, with
Otter being of possible interest due to a somewhat different approach
(I still don't fully understand all the differences.)  However, proof
logic is a topic in and of itself so clearly there is a lot to learn to
be able to use any of these tools to do anything interesting/useful, so
I guess I'd better focus on the dimension and unit stuff first rather
than get sucked into proof issues.  


Yahoo! Music Unlimited 
Access over 1 million songs. Try it free.

reply via email to

[Prev in Thread] Current Thread [Next in Thread]