My JFP article on the certifying compiler and type system of the systems PL Cogent, which enables equational reasoning to apply by refinement proof to generated C code, has finally been published. This is a capstone paper for all the work I did for my PhD.
