[Top][All Lists]

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

[Axiom-developer] COQ and Axiom

From: daly
Subject: [Axiom-developer] COQ and Axiom
Date: Sun, 12 Jul 2015 15:01:39 -0500

Axiom has a project goal of Proving Axiom Correct. This is
computational mathematics. It needs a solid foundation.

There are limits to what can be proven, of course, but the power
of the proof systems has really improved since Axiom was born.

Of the half-dozen or more proof systems and it appears that COQ 
is closest to Spad in spirit. COQ has the ability to handle dependent
types (e.g. specifying that an array has a fixed known length). COQ
has the ability to generate OCAML programs from proofs. This will
make it easy to compare with the Spad implementations. A major win
in the long term would be to auto-generate the Spad code but that's
a distant dream at the moment.

Axiom is being attacked from two directions. The first is from the
"categories down", trying to specify Axiom's category signatures in
COQ. The second is from the "bits up", trying to specify the lisp
functions that are implemented using only common lisp primitives.
These are marked in the interpreter already and will soon have
OCAML-like type signatures.

If anyone knows of prior work on either path, please let me know.

We have already gotten permission from Laurant Thery to use his work
on the proof of Buchberger's algorithm, some of which will show up
in Volume 13. I have to reverse-engineer his proof into the Spad


reply via email to

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