[Top][All Lists]

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

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

From: Martin Rubey
Subject: Re: [Axiom-developer] Ocaml, Coq, and ACL2
Date: Thu, 20 Oct 2005 17:45:46 +0200

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.

As far as I know it is based on Coq and Ocaml. See

I have no idea in what sense a theorem prover would be useful in a
CAS-context. Maybe Bruno Buchberger has some answers:


reply via email to

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