[Axiom-developer] ACL2/Axiom recommendation

[daly]

Matt and J,

I've been looking at ACL2 in order to look at proving Axiom programs correct. 

Besides the proof mechanism, ACL2 has the desirable property that it
can co-exist with Axiom in the same image and thus have direct access
to internal Axiom data structures. The idea would be to decorate domains
with theorems and look at automatically propagating the theorems,
bringing theorems in and out of scope, based on the hierarchy.

I'm undecided what the most productive area might be to concentrate upon.
Perhaps you can make a suggestion.

Data Structure -- this might be useful because there is a large body
of literature about the issue of proving sorting correct.

Rational Arithmetic -- this has properties that fit in areas that ACL2
already knows, such as the properties of abs().

Special Functions -- this has properties of manipulation of floating point
values which ACL2 has already explored.

Finite Fields -- this might be easier due to the limits of the size and
number of elements under consideration.

Given your experience can you give me some high level advice and 
potential pointers to previous work?

Tim Daly
address@hidden