M Hugo Herbelin

The Coq Proof Assistant System, which has been under continuous development for nearly 30 years, is a formal proof management system that supports a rich higher-order logic with powerful inductive definitions. The programming language incorporates a rich dependent type system, applicable to a range of needs from compilers to models of foundational mathematics. Because it can be used to state mathematical theorems and software specifications alike, Coq is a key enabling technology for certified software. The system is open source, is supported by a substantial and useful library as well as full documentation, and has attracted a large and active user community. Since the project started, more than 40 people took part to various theoretical, implementational and pedagogical works leading to the Coq system as it is now (see Who did What in Coq?). Coq has played an extremely influential role in several disciplines including as formal methods, programming languages, program verification, and formal mathematics. With increasing emphasis on the design and development of secure applications, certification has become important to the academic community as well as industry. Coq, which serves as a primary programming and certification tool, is instrumental to many of those efforts. Some of the significant results that were accomplished using Coq are proofs for the four color theorem, the development of CompCert (a fully verified compiler for C), the development at Harvard of a verified version of Google's software fault isolation, and most recent, the fully specified and verified hypervisor OS kernel CertiKOS.