Source language

• EpsML
• Semantics equivalence

Constructor numbering :

• EpsML#
• Translation
• Proof helpers
• Semantics preservation

Uncurrying :

• nML
• Translation
• Semantics preservation

Letrec elimination :

• nML'
• Semantics based on substitution
• Semantics equivalence
• Translation
• Semantics preservation

CPS conversion :

• CPS intermediate language with two kinds of de Bruijn indices
• CPS intermediate language
• Semantics based on substitution
• Semantics with environments
• Semantics equivalence
• The naive CPS conversion (only for proofs)
• Translation
• Proof helpers
• Proof helpers
• Semantics preservation
• The optimizing CPS conversion
• Translation
• One step beta v equivalence
• The transitive and reflexive closure of beta v equivalence
• Semantics preservation
• Come-back to nML
• Flatting 2 kinds of variables into one
• Semantics preservation

Closure conversion :

• fml
• Translation
• Semantics preservation

Conversion to the intermediate monadic form:

• the intermediate monadic form
• Translation
• Semantics preservation
• the roots computation

Materializing the set of roots :

• the Fminor intermediate language
• Translation
• Semantics preservation
• the well-bound relation of Fminor terms

Generation of Cminor code :

• Cminor: the first intermediate languge of the CompCert back-end
• Translation
• Proof helpers
• Specification of the behavior of a GC on memory
• Simulation scheme
• Semantics preservation

Composition of the front-end