The Coq proof assistant

Coq 8.1

This is a new evolution of the Coq system that provides the following main new features:

• efficient evaluation for proofs requiring intensive computations;
• inductive types with recursively non uniform parameters;
• sort-polymorphism for inductive definitions in Type;
• a new implementation of the ring and field tactics;
• a new implementation of the setoid_* tactics;
• new standard libraries (finite sets, finite maps, rational arithmetic and strings);
• Function: a new command for advanced recursive definitions;
• support for communication with external tools (provers, computer algebra systems, ...);
• a new experimental declarative mode for writing proofs.

Changelog, Download

News

A new web site for Coq is currently under development, and will soon be available. We invite you to visit this page and send your comments to webmaster_@_logical.futurs.inria.fr.

The beta release of Coq 8.2 is now out. If you want to get a taste of what Coq 8.2 will be, you should look at this page.

September 2007: a big step in program certification in the real world: The Technology and Innovation group at Gemalto has successfully completed a Common Criteria (CC) evaluation on a Java Card based commercial product. This evaluation is the world's first CC certificate of a Java product involving EAL7 components (the official press release).

A new minor release of Coq 8.1 is out ! It fixes some bugs of Coq 8.1. You can get it from the download page.

Coq 8.1 is now available as the new stable version of the Coq system! See the download page to get it.

A new version of the 8.0 series is available! It is 8.0pl4, and it fixes some bugs of previous release. It is available from this page

New user contributions 2005-2007: another approach of proof by reflexion for first-order logic (1/2007), persistent union-find library (11/2006), Micromega (a reflexive tactics for Presburger arithmetic and more) (11/2006), up-to techniques for weak bisimulation (9/2006), Chou-Gao-Zhang area method for deciding affine geometry (8/2006), CoLoR (a library on rewriting and termination) (5/2006), case study on square matrices (3/2006), embedding intuitionistic ZF set theory in Coq + intuitionistic choice (3/2006), certified Sudoku solver (2/2006), higher-order syntax from modules over monads (1/2006), modelization of random programs (1/2006), proof of the Fairisle 4x4 Switch Element (1/2006), intuitionistic propositional checker (10/2005), Tait-style normalizability for simply-typed lambda-calculus (10/2005), Karatsuba multiplication on binary numbers (9/2005), Diophantus' 20th Problem and Fermat's last theorem for n=4 (7/2005).

A C compiler back-end to PowerPC assembly has been certified in Coq as part of the CompCert project headed by Xavier Leroy. The main result states the preservation of the semantics of an intermediate language called Cminor through about 10 compilation passes ending in PowerPC code.

Full formalization of the 4 colors theorem in Coq has been completed in December 2004. Started in 1999 at INRIA-Rocquencourt by Georges Gonthier et Benjamin Werner, the project has been completed by Georges Gonthier who found support at Cambridge Microsoft Research. The formalization, based on Robertson, Sanders, Seymour and Thomas proof from 1995 has been done in Coq V7.3. Port to Coq 8.0 is ongoing. The project has motivated new extensions of Coq. Especially, a new optimized reduction machine dedicated to computation of reflexion tactics will be available in the next released version of Coq (more).

New user contributions 2004-2005: Kildall's data-flow analysis (7/2005), Cantor Normal Form of ordinals and Goodstein sequences (6/2005), natural deduction for first-order logic (5/2005), divide-and-conquer for binary tree diameter computation (3/2005), characterization of the numbers that are sum of two square numbers (1/2005), category theory in set theory (11/2004), the Godel-Rosser 1st incompleteness theorem (5/2004), bisimulation for the spi-calculus (4/2004).

Pierre Castéran updated Eduardo Giménez's tutorial on recursive types to Coq V8. It is available in the documentation section.

New user contributions 2003-2004: dictionaries, c-corn, coqoban, gc, higman, lambek-calculus, linalg, qarith, fsets, geometry, huffman, matrices. Browse the contribution section for an overview !

Trusted Logic announces (press release of November 18th, 2003) that the DCSSI has successfully evaluated its security methodology applied to the Java Card™ System at the Common Criteria EAL7 level, in a report published earlier this year.

Coq is the proof engine used by Trusted Logics, and was chosen for its expressiveness. As a part of the certification process, it is being acknowledged as trustworthy by the DCSSI.

Yves Bertot and Pierre Castéran's Coq'Art will be published by Springer-Verlag. It should be on the shelves at the beginning of 2004.
"This book provides a pragmatic introduction to the development of proofs and certified programs using Coq. With its large collection of examples and exercises it is an invaluable tool for researchers, students, and engineers interested in formal methods and the development of zero-default software."

Ccsd publishes a paper by Carlos Simpson on "Computer theorem proving in math", available here. It provides an overview of issues surrounding computer-verified theorem proving in the standard pure-mathematical context. This paper includes proofs in Coq.