For the Coq Proof Assistant System that provides interactive software for the development of formal proofs, using a powerful logic known as the Calculus of Inductive Constructions.
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.Scroll Up
Coq Selected As Recipient Of The 2013 Software System Award
Coq is a software tool for the interactive development of formal proofs, which is a key enabling technology for certified software. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs. An open source product, Coq has played an influential role in formal methods, programming languages, program verification and formal mathematics. As certification gains importance in academic and industrial arenas, Coq plays a critical role as a primary programming and certification tool. Coq’s first implementation was in 1985, when it was named CoC (the acronym for the logic it implemented: the Calculus of Constructions). This system was developed by the Coq Development Team whose primary members were Thierry Coquand, University of Gothenburg; Gérard Huet, INRIA Paris - Rocquencourt; Christine Paulin-Mohring, University Paris Sud/INRIA Saclay; Bruno Barras, INRIA Saclay/École Polytechnique; Jean-Christophe Filliâtre, CNRS/INRIA Saclay; Hugo Herbelin, INRIA Paris - Rocquencourt; Chet Murthy, Google Inc.; Yves Bertot, INRIA Sophia; and Pierre Castéran, University of Bordeaux.