A Typed C11 Semantics for Interactive Theorem Proving

We present a semantics of a significant fragment of the C programming language as described by the C11 standard. It consists of a small step semantics of a core language, which uses a structured memory model to capture subtleties of C11, such as strict-aliasing restrictions related to unions, that have not yet been addressed by others. The semantics of actual C programs is defined by translation into this core language. We have an explicit type system for the core language, and prove type preservation and progress, as well as type correctness of the translation. Due to unspecified order of evaluation, our operational semantics is non-deterministic. To explore all defined and undefined behaviors, we present an executable semantics that computes a stream of finite sets of reachable states. It is proved sound and complete with respect to the operational semantics. Both the translation into the core language and the executable semantics are defined as Coq programs. Extraction to OCaml is used to obtain a C interpreter to run and test the semantics on actual C programs. All proofs are fully formalized in Coq.