News about Coq

As part of the ADT Coq-API, we are now offering a 2-year position for a specialized engineer.
For more details, see

Version 8.4pl4 of Coq fixes several bugs of version 8.4pl3 including 3 critical ones. More information to be found in the CHANGES file.

WARNING: The current logic of Coq is now known to be inconsistent with Axiom prop_extensionality :
forall A B:Prop, (A <-> B) -> A = B.

The main source repository for Coq on is now using git instead of subversion.

For accessing this new repository, see the "sources" page of the coq project on gforge.

More details could be found on the wiki page about this transition.

Happy git cloning :-)

The development of Coq has been initiated in 1984 at INRIA by Thierry Coquand and Gérard Huet, then joined by Christine Paulin-Mohring and more than 40 direct contributors.

The first public release was CoC 4.10 in 1989. Extended with native inductive types, it was renamed Coq in 1991.

Since then, a growing community of users has shared its enthousiasm in the originality of the concepts of Coq and of its various features, as a richly-typed programming language and as an interactive theorem prover.

The final release of Coq 8.4 is now available. Its features among other things a modular and uniform extension of the arithmetical libraries and a new proof engine providing bullets. See the dedicated page or download page for more details.

Coq 8.4 is available as a release candidate. More on the Coq 8.4 web page...

Coq 8.4 is available for beta-testing. More on the Coq 8.4 web page...

Version 8.3pl3 of Coq fixes several bugs of version 8.3pl2. At the same time, new patch-level releases of 8.1 and 8.2 have been released to fix critical bugs related to sort-polymorphism of inductive types.

For 8.3pl3, see the CHANGES file for a selected list of changes since 8.3pl2.

The Coq Workshop 201! will be held on August 26 at Nijmegen, as part of ITP 2011.

Syndicate content