The Vélus compiler is implemented in a mix of Coq and OCaml. A program is parsed from a source file and successively transformed through several intermediate languages. The final transformation produces a Clight program for CompCert to compile into one of its supported assembly languages.
The syntax and semantics of the intermediate languages are specified in Coq. The transformations are specified as functional programs that manipulate syntactic terms. Each is accompanied by a correctness proof showing the preservation of input/output traces in the semantic models.
|Lustre||normalization (not yet implemented)|