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

[Martin Rubey]

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

http://focal.inria.fr/site/manual.html

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/

Martin