News about Coq

The main source repository for Coq on gforge.inria.fr 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 3rd Asian-Pacific Summer School on Formal Methods will be held in Suzhou, China in August 13-21, 2011.

The objective is to teach students the principles and practice of programming with the proof assistant Coq, as in previous years (2009 and 2010), and to show them the state of art applications of proof assistants and theorem provers in formal methods.

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

Version 8.3pl2 of Coq fixes several bugs of version 8.3pl1. In particular, it provides compatibility for compiling Coq from sources with the latest versions of Objective Caml and Camlp5. More information to be found in the CHANGES file.

Syndicate content