As part of the ADT Coq-API, we are now offering a 2-year position for a specialized engineer.
For more details, see http://www.pps.univ-paris-diderot.fr/~letouzey/coq-api-position.html
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.
After the ACM SIGPLAN Programming Languages Sofware 2013 Award, Coq received the ACM Software System 2013 award.
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.
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.