[Top][All Lists]
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [Axiom-developer] Ocaml, Coq, and ACL2
From: |
C Y |
Subject: |
Re: [Axiom-developer] Ocaml, Coq, and ACL2 |
Date: |
Thu, 20 Oct 2005 09:26:40 -0700 (PDT) |
--- Martin Rubey <address@hidden> wrote:
> I'd just like to add that Renaud Rioboo is working on Focal, which
> seems to be exactly what Cliff Yapp is looking for. However, it is
> (and will stay) disconnected from Axiom.
Neat!
> As far as I know it is based on Coq and Ocaml. See
>
> http://focal.inria.fr/site/manual.html
I'll add that to my reading list.
> I have no idea in what sense a theorem prover would be useful in a
> CAS-context. Maybe Bruno Buchberger has some answers:
>
> http://www.risc.uni-linz.ac.at/research/theorema/description/
I've seen a couple efforts along those lines scattered around, but I
haven't taken the time to study them in depth. Guess I should do that
before anything else.
Cheers, and thanks!
CY
__________________________________
Yahoo! Music Unlimited
Access over 1 million songs. Try it free.
http://music.yahoo.com/unlimited/
- [Axiom-developer] Ocaml, Coq, and ACL2, Page, Bill, 2005/10/20
- Re: [Axiom-developer] Ocaml, Coq, and ACL2, Martin Rubey, 2005/10/20
- Re: [Axiom-developer] Ocaml, Coq, and ACL2,
C Y <=
- [Axiom-developer] Re: Ocaml, Coq, and ACL2, C Y, 2005/10/20