[Top][All Lists]

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [Axiom-developer] Proving Axiom Correct -- at the C level

From: Tim Daly
Subject: Re: [Axiom-developer] Proving Axiom Correct -- at the C level
Date: Fri, 31 Mar 2017 23:16:13 -0400

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 (
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? :-)


reply via email to

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