Re: Proving Axiom Correct -- at the C level
Tim Daly <[email protected]>
| Newsgroups | gmane.comp.mathematics.axiom.devel |
|---|---|
| Message-ID | <CAJn5L=KZojuZudaxXy5RjUiS5nFN-wW=gyaDaTBhR-kHt-3aCw@mail.gmail.com> |
I previously mentioned the "proof tower" approach to the question of proving code at many different layers. Spad code proven in COQ, Lisp code in ACL2, and Intel code in CCAs. The missing step in the tower was C. Apparently there is work in COQ (http://robbertkrebbers.nl/research/ch2o/) on the CH2O formalization of ISO C11 by Robbert Krebbers. CH2) provides an operational, executable, and axiomatic semantics for a significant fragment of C11. So this provides COQ support for the missing layer in the proof tower. Now all we need are Category props and Domain proofs. What could be easier? :-) Tim _______________________________________________ Axiom-developer mailing list [email protected] https://lists.nongnu.org/mailman/listinfo/axiom-developer