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