The C standard formalized in Coq (http://robbertkrebbers.nl/thesis.html)
This thesis describes a formal specification of the sequential fragment of the C programming language based on the official description of the C language, the C11 standard. Axiom uses GCL which compiles to C. Axiom has a graphics package written in C. The tools are becoming available, Coq for Spad, ACL2 for Lisp, and now Coq for C. Axiom has been restructured to automate the Coq and ACL2 proof machinery. These proofs are run on request at build time. Ultimately this will lead to higher quality software as well as a deeper understanding of questions like simplification and branch cuts. Proving computational mathematics correct is a long term but vital goal. Tim _______________________________________________ Axiom-developer mailing list Axiom-developer@nongnu.org https://lists.nongnu.org/mailman/listinfo/axiom-developer
