Leslie Lamport has an interesting talk on hierarchical proofs. If you have any interest in proving Spad programs correct then this is an interesting talk[1]
I've been looking at various tools to prove Spad algorithms at all layers (math->spad, spad->lisp, lisp->C, C->machine) In particular, I'm focusing on the GCD algorithm in EUCDOM as the proof of the algorithm is widely known. The first step of this kind of proof is to do the (math->spad) phase. Lamport has a system called TLA which allows hierarchical structuring of proofs in math. COQ does machine-checked proofs, especially those with types. Since Axiom is hierarchical it seems that TLA can structure the proof into sub-proofs (e.g. showing that unitCanonical is correct) and COQ can be used to focus on each layer. In any case, it is time to try to take baby-steps toward putting Axiom on a firm mathematical foundation. If you know of any other interesting lectures please let me know. Tim [1] http://hits.mediasite.com/mediasite/Play/29d825439b3c49f088d35555426fbdf81d _______________________________________________ Axiom-developer mailing list [email protected] https://lists.nongnu.org/mailman/listinfo/axiom-developer
