The CompCert verified compilerThe CompCert verified compiler Commented Coq development Version 3.13, 2023-07-04 Introduction CompCert is a compiler that generates ARM, PowerPC, RISC-V and x86 assembly code from CompCert C, a large subset of the C programming language. The particularity of this compiler is that it is written mostly within the specification language of the Coq proof assistant, and its correctness --- the fact th
