[Top][All Lists]

[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.



reply via email to

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