I picked up two books that seem to be useful in the task of trying
to prove at least one algorithm in Axiom "correct", for some
philosophical version of correct.
I'd really like to show an automated proof of Axiom's GCD algorithm.
Pointers to published work on GCD proofs would be really useful.
Yves and Pierre [0] has a whole chapter on "Infinite Objects and
Proofs" with a section on co-inductive types (streams, lazy lists,
lazy binary trees).
Chandy and Misra [1] has a section on prime number generation by sieving.
Suggestions of other reading material is most welcome.
[0] Bertot, Yves; Casteran, Pierre
"Interactive Theorem Proving and Program Development"
ISBN 3-540-20854-2
[1] Chandy, Mani ; Misra, Jayadev
"Parallel Program Design"
ISBN 0-201-05866-9
_______________________________________________
Axiom-developer mailing list
Axiom-developer@nongnu.org
https://lists.nongnu.org/mailman/listinfo/axiom-developer
