Topic of my Ph. D. thesis

As part of formal verification of critical software, preserving properties established on the source code in the executable code seems to be crucial. To have this preservation, the compiler has to be verified itself. A compiler is formally verified if it is joined with a proof of semantic preservation: the behavior of the compiled code preserves the source code behavior, if the compilation succeeds.

The CompCert project investigates the formal verification of realistic compilers usable for critical embedded software. The project designs, develops and mechanically verifies compilers within the Coq Proof Assistant. By this method, a C compiler producing PowerPC assembly code has already be developed and verified. Using the extraction mechanism of Coq, the compiler is automatically extracted into OCaml code, which is compiled by the Objective Caml system. Actually, the production of the executable compiler uses (or used to use) two unverified processes: the extraction mechanism and the Objective Caml compiler. In fact, this is true for any specified development in the Coq Proof Assistant when the target is to obtain an executable.

My thesis deals with the design, development and mechanized verification, in the Coq Proof Assistant, of a compiler for the purely functional fragment of ML, which is the language of extracted from Coq extraction. Concretely, a front-end from miniML (lambda-calculus, let, letrec, pattern-matching) to Cminor has been developed. Cminor is a low-level C-like language, that is the first intermediate language of the CompCert back-end.

Such as the source language is expressive, the compiler is realistic. Classical functional language compilation optimizations are done: uncurrying (the same optimization as in OCaml), uniform data structure representation (as numbering constructor and closure conversion) and an optimizing CPS translation. As in modern compiler for high-level languages, the miniML compiler can interact with a memory manager. This interaction has been mechanized verified.