Mechanized Metatheory and Certified Compilation for The Rocq Prover

The work presented in this habilitation thesis focuses on the verification of the logical core of the Rocq Prover, as well as its original mechanism for compiling to usual functional programming languages. The objective of this work is to obtain formal safety guarantees for the underlying theory of the Rocq prover, for the implementation of the proof verifier for this theory, and for the procedure of program extraction that enables the efficient execution of code verified by Rocq. This work lies at the intersection of the meta-theory of type theory and the formal verification of type inference and compilation algorithms.We present MetaRocq, a formal development of specifications and verified programs, representing a large fragment of Rocq within Rocq itself. This combines techniques for meta-programming and large-scale language metatheory proofs, as well as certified compilation techniques.We formally develop in Rocq a formal specification of Rocq's type theory and its equivalent algorithmic variant, a typing algorithm that is correct and complete with respect to these specifications, a correct proof erasure algorithm, and a compilation chain from Rocq to OCaml that preserves the semantics of the source language.The results obtained here allow us to shift the paradigm regarding the safety of the results obtained in the proof assistant and produced by extraction, moving from a notion of a trusted code base — the current unverified kernel — to a notion of trusted theory base — the formal specification of Rocq's theory in Rocq that we have introduced. We discuss the impact and limitations of our work to obtain maximal correctness guarantees for the formal developments carried out in the proof assistant.