The Science of Deep Specification

CertiCoq: Principled Optimizing Compilation of Dependently Typed Programs

The CertiCoq project aims to build a proven-correct compiler for dependently-typed, functional languages, such as Gallina—the core language of the Coq proof assistant. A proved-correct compiler consists of a high-level functional specification, machine-verified proofs of important properties, such as safety and correctness, and a mechanism to transport those proofs to the generated machine code. The project exposes both engineering challenges and foundational questions about compilers for dependently-typed languages.

CertiCoq project website