Compcert uses small-step operational semantics for both the source language and the assembly output (and intermediate languages that are irrelevant to the final

Compcert uses small-step operational semantics for both the source language and the assembly output (and intermediate languages that are irrelevant to the final statement of the semantic preservation theorem). Specifying such a semantics is basically like writing a very simple functional interpreter for the language. I don't see how it could get much simpler. Here is the description of the semantics for their input language: http://compcert.inria.fr/doc/html/Csem.html http://compcert.inria.fr/doc/html/Csem.html and their PPC output: http://compcert.inria.fr/doc/html/Asm.html http://compcert.inria.fr/doc/html/Asm.html