The Coq proof assistant

Coq is a formal proof management system. 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. Typical applications include the [certification of properties of programming languages](https://coq.inria.fr/cocorico/List%20of%20Coq%20PL%20Projects) (e.g. the [CompCert](http://compcert.inria.fr/) compiler certification project, or the [Bedrock](http://plv.csail.mit.edu/bedrock/) verified low-level programming library), the [formalization of mathematics](https://coq.inria.fr/cocorico/List%20of%20Coq%20Math%20Projects) (e.g. the full formalization of the [Feit-Thompson theorem](http://www.msr-inria.fr/news/feit-thomson-proved-in-coq/) or [homotopy type theory](https://coq.inria.fr/cocorico/CoqInTheClassroom)) and [teaching](https://coq.inria.fr/cocorico/CoqInTheClassroom).

Coq implements a program specification and mathematical higher-level language called Gallina that is based on an expressive formal language called the Calculus of Inductive Constructions that itself combines both a higher-order logic and a richly-typed functional programming language. Through a vernacular language of commands, Coq allows:

- to define functions or predicates, that can be evaluated efficiently;

- to state mathematical theorems and software specifications;

- to interactively develop formal proofs of these theorems;

- to machine-check these proofs by a relatively small certification "kernel";

- to extract certified programs to languages like Objective Caml, Haskell or Scheme.

As a proof development system, Coq provides interactive proof methods, decision and semi-decision algorithms, and a tactic language for - letting the user define its own proof methods. Connection with external computer algebra system or theorem provers is available.

As a platform for the formalization of mathematics or the development of programs, Coq provides support for high-level notations, implicit contents and various other useful kinds of macros.