[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: Mon, 30 Nov 2015 19:46:52 -0500 (EST)

The C standard formalized in Coq (

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. 


reply via email to

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