Verification of software is used to eliminate bugs, discover code's properties (e.g. performance bounds), and ease the refactoring thereof. Making use of proof assistants (e.g. Coq) in this endeavor adds to the validity of such verification, as the proofs about the software can be directly tied to it. Moreover, it helps reduce human error that can easily occur in hand-written reasoning.
The work aims to develop faithful high-level programming language implementations that are easily mechanized in Coq; as such, it will not only provide more insight into the compilation of high-level languages, but it will also further the trustworthiness of correctness tools.