[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
## [Axiom-developer] Proving Axiom correct

**From**: |
daly |

**Subject**: |
[Axiom-developer] Proving Axiom correct |

**Date**: |
Fri, 30 Jan 2015 04:36:56 -0600 |

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

[Prev in Thread] |
**Current Thread** |
[Next in Thread] |

**[Axiom-developer] Proving Axiom correct**,
*daly* **<=**