The design and implementation of the linear verified compiler (LVC) is my PhD project.
In my master's thesis, I developed a term-based approach to static single assignment that leverages that SSA is functional programming (Appel, Kelsey). LVC is a verified compiler that uses this approach to realize SSA-based optimizations, in particular sparse conditional constant propagation (Wegman, Zadeck) and SSA-based register allocation including spilling (Rosemann, Schneider, Hack). LVC realizes compilation as program transformation to a low-level fragment of the intermediate language (Kelsey, Hudak). LVC's intermediate language IL supports this approach by providing two semantic interpretations, a functional one (variables are binders) and an imperative one (variables are imperative locations). The two semantic interpretations provide a semantic framework for SSA programs, in particular, we claim IL makes it easier to rename apart an imperative program as the usual dominance-based approach.
The development of LVC is available at GitHub. I extended the intermediate language in the formal development with mutually recursive function definitions to be more realistic - a time-consuming mistake. The preliminary CoqDoc is available here.
The write-up of my PhD thesis is currently in progress, and I hope to finish early in 2018.