In the context of mechanized verification of a compiler for a functional language, we have experienced the influence of the semantic preservation proof on the definition of intermediate languages and their semantics.

This is a compiler for the purely functional fragment of untyped ML, formally verified into the Coq system. In the spirit of the CompCert compiler, our compiler is realistic. On top of being an expressive language (recursive functions, pattern matching) and capable of optimizations such as uncurrying, CPS and tailcall compilation optimization, the generated code is also able to interact with an automatic memory manager using a GC

Concretly, we developed a frontend which target language is the first intermediate language of the CompCert backend (Cminor). That allows us to produce PowerPC assembly code. The mini-ML frontend is a chain of successive transformations. For each transformation, we have prooved that it preserves semantics. Composing the proof of semantics preservation of all transformation gives us the semantics preservation of the frontend. This talk is about an overview of the frontend for miniML, with two zoom. First, we will focus on the uncurrying optimisation which is implemented as in the Objective Caml system. Secondly, we decribe the interaction with an automatic memory manager into two transformations using two purely functional languages.