The Vélus compiler is implemented in a mix of Coq
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
The syntax and semantics of the intermediate languages are specified in Coq.
The transformations are specified as functional programs that manipulate
Each is accompanied by a correctness proof showing the preservation of
input/output traces in the semantic models.