Coq

Website: coq.inria.fr

Coq is an interactive theorem prover first released in 1989.

It allows for expressing mathematical assertions, mechanically checks proofs of these assertions, helps find formal proofs, and extracts a certified program from the constructive proof of its formal specification.

Coq works within the theory of the calculus of inductive constructions, a derivative of the calculus of constructions.

Coq is not an automated theorem prover but includes automatic theorem proving tactics (procedures) and various decision procedures.

The Association for Computing Machinery awarded Thierry Coquand, Gérard Huet, Christine Paulin-Mohring, Bruno Barras, Jean-Christophe Filliâtre, Hugo Herbelin, Chetan Murthy, Yves Bertot, and Pierre Castéran with the 2013 ACM Software System Award for Coq.

The name “Coq” is a wordplay on the name of Thierry Coquand, Calculus of Constructions or “CoC” and follows the French computer science tradition of naming software after animals (coq in French meaning rooster).