The Coq Proof Assistant

The Coq development team is proud to announce the immediate availability of the Coq Platform 2021.02.0

The Coq platform is a distribution of the Coq proof assistant together with a selection of Coq libraries. It provides a set of scripts to compile and install OPAM, Coq, Coq libraries and Coq plugins on MacOS, Windows and many Linux distributions in a reliable way with consistent results.

This release is based on Coq 8.13.1 and provides binary installers for Windows and Linux. We plan to release 2021.02.1 as soon as the MacOS installer is ready. The following point releases, starting with 2021.02.2, will focus on including more Coq libraries (and no breaking change).

The Coq development team is proud to announce the immediate availability of Coq 8.13.1

Hotfix:

• Fix arities of VM opcodes for some floating-point operations that could cause memory corruption

Please see the changelog to learn more about this release.

The Coq development team is proud to announce the immediate availability of Coq 8.13.0

Highlights:

• Introduction of primitive persistent arrays in the core language, implemented using imperative persistent arrays.
• Introduction of definitional proof irrelevance for the equality type defined in the SProp sort.
• Many improvements to the handling of notations, including number notations, recursive notations and notations with bindings. A new algorithm chooses the most precise notation available to print an expression, which might introduce changes in printing behavior.

Please see the changelog to learn more about this release.

We are happy to announce the release of Coq 8.12.2.

This release fixes two impacting 8.12 regressions (in notations and the implicit argument inference of the exists tactic). See the changelog for details.

The Coq development team is proud to announce the immediate availability of Coq 8.13+beta1

Here the full list of changes.

We encourage our users to test this beta release, in particular:

• The windows installer is now based on the Coq platform: This greatly simplifies its build process and makes it easy to add more packages. At the same time this new installer was only tested by two people, so if you use Windows please give us feedback on any problem you may encounter.
• The notation system received many fixes and improvements, in particular the way notations are selected for printing changed: Coq now prefers notations which match a larger part of the term to abbreviate, and takes into account the order in which notations are imported in the current scope only in a second instance. The new rules were designed together with power users, and tested by some of them, but our automatic testing infrastructure for regressions in notation printing is still weak. If your Coq library makes heavy use of notations, please give us feedback on any regression.

The 8.13.0 release is expected to occur about one month from now.

We are happy to announce the release of Coq 8.12.1.

This release contains numerous bug fixes and documentation improvements. Some bug fix highlights:

• Polymorphic side-effects inside monomorphic definitions were incorrectly handled as not inlined. This allowed deriving an inconsistency.
• Regression in error reporting after SSReflect's case tactic. A generic error message "Could not fill dependent hole in apply" was reported for any error following case or elim.
• Several bugs with Search.
• The details environment introduced in coqdoc in Coq 8.12 can now be used as advertised in the reference manual.
• View menu "Display parentheses" introduced in CoqIDE in Coq 8.12 now works correctly.

See the changelog for details and a more complete list.

We are happy to announce the release of Coq 8.12.0.

Some highlights from this release are:

• a new binder notation for non-maximal implicit arguments;
• an improved Search command which accepts more complex queries;
• many additions to the standard library;
• a restructured reference manual;
• the deprecation of the omega tactic in favor the lia tactic.

Please see the changelog to learn more about this release.

We are happy to announce the first beta release of Coq 8.12.

This new version integrates many usability improvements, in particular to notations, scopes and implicit arguments, along with many bug fixes and major improvements to the reference manual. See the changelog for details.

As usual, we are looking for feedback from beta testers. In addition, we are looking for beta readers of the updated reference manual.

The 8.12 improvements to the reference manual are the start of an effort to improve Coq documentation. We believe the documentation needs considerable work to better serve the needs of the Coq community. Better documentation will encourage more people to learn, teach and use Coq. We need your help for this. We're looking for volunteers who will help rewrite or add new material (such as better explanations and new examples) to the new pages. Writers do not have to be experts on their topic: we can pair writers with experts that can answer questions and provide examples. Indeed, it's a great way to learn more about Coq. We'd also appreciate specific feedback, perhaps detailed, on what needs to be improved, what's missing and what things to improve first. If you are willing to help, please see the dedicated wiki page to learn more.

The 8.11.2 release of Coq is available.

This version brings in a few minor fixes. See the changelog for more details.

The 8.11.1 release of Coq is available.

The most salient change in the 8.11.1 release is support for OCaml 4.10.0. See the changelog for more details.

The 8.11.0 release of Coq is available.

There are two main changes brought by Coq 8.11.

• It introduces Ltac2, a new tactic language for writing more robust larger scale tactics, with built-in support for datatypes and the multi-goal tactic monad.
• Primitive floats are integrated in terms and follow the binary64 format of the IEEE 754 standard, as specified in the `Coq.Float.Floats` library.

Many other cleanups and improvements have been performed and are further described in the reference manual.

The first beta release of Coq 8.11 is available for testing.

There are two main changes brought by Coq version 8.11. First, it introduces Ltac2, a new tactic language for writing more robust larger scale tactics, with built-in support for datatypes and the multi-goal tactic monad. Second, primitive floats are integrated in terms and follow the binary64 format of the IEEE 754 standard, as specified in the `Coq.Float.Floats` library. Many other cleanups and improvements have been performed and are further described in the reference manual.

Feedback and bug reports are extremely welcome.

The 8.10.2 release of Coq is available.

Main changes:

• Fixed a critical bug of template polymorphism and nonlinear universes
• Fixed a few anomalies
• Fixed an 8.10 regression related to the printing of coercions associated to notations
• Fixed uneven dimensions of CoqIDE panels when window has been resized
• Fixed queries in CoqIDE

All details can be found in the user manual.

Feedback and bug reports are extremely welcome.

The 8.10.1 release of Coq is available.

Main changes:

• fix proof of False when using SProp;
• fix an anomaly when unsolved evar in Add Ring;
• fix Ltac regression in binding free names in uconstr;
• fix handling of unicode input before space;
• fix custom extraction of inductives to JSON.

All details can be found in the user manual.

Feedback and bug reports are extremely welcome.

The 8.10.0 release of Coq is available.

Main changes:

• some quality-of-life bug fixes;
• a critical bug fix related to template polymorphism;
• native 63-bit machine integers;
• a new sort of definitionally proof-irrelevant propositions: SProp;
• private universes for opaque polymorphic constants;
• string notations and numeral notations;
• a new simplex-based proof engine for the tactics lia, nia, lra and nra;
• new introduction patterns for SSReflect;
• a tactic to rewrite under binders: under;
• easy input of non-ASCII symbols in CoqIDE, which now uses GTK3.

All details can be found in the user manual.

Feedback and bug reports are extremely welcome.

The third beta release of Coq 8.10 is available for testing.

This third β version includes various bug fixes and improvements, including:

• improved warning on coercion path ambiguity;
• support for OCaml extraction of primitive machine integers;
• fix for the soundness issue with template polymorphism;
• fix extraction of dependent record projections to OCaml.

More details are given in the user manual.

Feedback and bug reports are extremely welcome.

The second beta release of Coq 8.10 is available for testing.

This second β version includes many bug fixes and documentation improvements; more details are given in the reference manual.

Feedback and bug reports are extremely welcome.

The 8.9.1 release of Coq is available.

Main changes:

• some quality-of-life bug fixes,
• many improvements to the documentation,
• a critical bug fix related to primitive projections and native_compute,
• several additional Coq libraries shipped with the Windows installer.

Feedback and bug reports are extremely welcome.

The first beta release of Coq 8.10 is available for testing.

Coq version 8.10 contains two major new features: support for a native machine integer type and a new sort SProp, a definitionally proof irrelevant universe. It is also the result of refinements and stabilization of previous features, deprecations or removals of deprecated features, cleanups of the internals of the system and API, and many documentation improvements. This release includes many user-visible changes, including deprecations and new features. A more detailed list of changes appears in the reference manual.

Feedback and bug reports are extremely welcome.

The 8.9.0 release of Coq is available.

It features many quality-of-life improvements, including goal differences as well as numeral and custom notations. For details, see the CHANGES file.

Feedback and bug reports are extremely welcome.

The first beta release of Coq 8.9 is available for testing.

It features many quality-of-life improvements, including goal differences as well as numeral and custom notations. For details, see the CHANGES file.

Feedback and bug reports are extremely welcome.

The 8.8.2 release of Coq is available.

Main changes:

• The kernel does not tolerate capture of global universes by polymorphic universe binders, fixing a soundness break (triggered only through custom plugins)
• A PDF version of the reference manual is available once again.
• The coq-makefile targets print-pretty-timed, print-pretty-timed-diff, and print-pretty-single-time-diff now correctly label the "before" and "after" columns, rather than swapping them.
• The Windows installer now includes many more external packages that can be individually selected for installation.

Many other bug fixes and lots of documentation improvements (for details, see the 8.8.2 milestone).

Feedback and bug reports are extremely welcome.

The 8.8.1 release of Coq is available.

It includes four critical bug fixes, many other bug fixes, documentation improvements and user message improvements.

For details, see CHANGES and the 8.8.1 milestone. Feedback and bug reports are extremely welcome.

The final release of Coq 8.8.0 is available. It features better performances, tactic improvements, many enhancements for universe users, a new Export modifier for setting options, support for goal selectors in front of focusing brackets and a new experimental -mangle-names option for linting proof scripts. Feedback and bug reports are extremely welcome.

The first beta release of Coq 8.8 is available for testing. It features better performances, tactic improvements, many enhancements for universe users, a new Export modifier for setting options, support for goal selectors in front of focusing brackets and a new experimental -mangle-names option for linting proof scripts. Feedback and bug reports are extremely welcome.

Version 8.7.2 of Coq is available. It fixes a critical bug in the VM handling of universes. This bug affected all releases since 8.5.

Other changes include improved support for building with OCaml 4.06.0 and external num package, many other bug fixes, documentation improvements, and user message improvements (for details, see the 8.7.2 milestone).

The macOS installer for Coq 8.7.1 was updated on 2018-01-08 to fix frequent crashes of CoqIDE due to the use of an outdated dependency. Direct link to the new version: coq-8.7.1-1-installer-macos.dmg.

Version 8.7.1 of Coq is available. It brings compatibility with OCaml 4.06.0, many bug fixes, documentation improvements, and user message improvements (for details see the 8.7.1 milestone).

After several years of using GitHub specifically for its pull request system, the Coq development team has migrated the Coq bug tracker and Cocorico, the Coq wiki to GitHub as well.

More information about the migration of the Coq bug tracker may be found in this blog post.

More information about the migration of Cocorico, the Coq wiki, may be found on this wiki page.

Finally, the GitHub repository is now the repository we push to (as opposed to a mirror). Make sure that your git clone is tracking https://github.com/coq/coq.git to be always up-to-date.

The final release of Coq 8.7.0 is available. Coq 8.7 includes:

• A large amount of work on cleaning and speeding up the code base, notably the work of Pierre-Marie Pédrot on making the tactic-level system insensitive to existential variable expansion, providing a safer API to plugin writers and making the code more robust.
• New tactics:
  • Variants of tactics supporting existential variables eassert, eenough, etc. by Hugo Herbelin;
  • Tactics extensionality in H and inversion_sigma by Jason Gross;
  • specialize with accepting partial bindings by Pierre Courtieu.
• Cumulative Polymorphic Inductive Types, allowing cumulativity of universes to go through applied inductive types, by Amin Timany and Matthieu Sozeau.
• The SSReflect plugin by Georges Gonthier, Assia Mahboubi and Enrico Tassi was integrated (with its documentation in the reference manual) by Maxime Dénès, Assia Mahboubi and Enrico Tassi.
• The coq_makefile tool was completely redesigned to improve its maintainability and the extensibility of generated Makefiles, and to make _CoqProject files more palatable to IDEs by Enrico Tassi.

More information can be found in the CHANGES file. Feedback and bug reports are extremely welcome.

This is the second release of Coq developed on a time-based development cycle. Its development spanned 9 months from the release of Coq 8.6 and was based on a public road-map. It attracted many external contributions. Code reviews and continuous integration testing were systematically used before integration of new features, with an important focus given to compatibility and performance issues.

The second beta release of Coq 8.7 is available for testing. Coq 8.7 includes:

• A large amount of work on cleaning and speeding up the code base, notably the work of Pierre-Marie Pédrot on making the tactic-level system insensitive to existential variable expansion, providing a safer API to plugin writers and making the code more robust.
• New tactics:
  • Variants of tactics supporting existential variables eassert, eenough, etc. by Hugo Herbelin;
  • Tactics extensionality in H and inversion_sigma by Jason Gross;
  • specialize with accepting partial bindings by Pierre Courtieu.
• Cumulative Polymorphic Inductive Types, allowing cumulativity of universes to go through applied inductive types, by Amin Timany and Matthieu Sozeau.
• The SSReflect plugin by Georges Gonthier, Assia Mahboubi and Enrico Tassi was integrated (with its documentation in the reference manual) by Maxime Dénès, Assia Mahboubi and Enrico Tassi.
• The coq_makefile tool was completely redesigned to improve its maintainability and the extensibility of generated Makefiles, and to make _CoqProject files more palatable to IDEs by Enrico Tassi.

More information can be found in the CHANGES file. Feedback and bug reports are extremely welcome.

This is the second release of Coq developed on a time-based development cycle. Its development spanned 9 months from the release of Coq 8.6 and was based on a public road-map. It attracted many external contributions. Code reviews and continuous integration testing were systematically used before integration of new features, with an important focus given to compatibility and performance issues.

The first beta release of Coq 8.7 is available for testing. Coq 8.7 includes:

• A large amount of work on cleaning and speeding up the code base, notably the work of Pierre-Marie Pédrot on making the tactic-level system insensitive to existential variable expansion, providing a safer API to plugin writers and making the code more robust.
• New tactics:
  • Variants of tactics supporting existential variables eassert, eenough, etc. by Hugo Herbelin;
  • Tactics extensionality in H and inversion_sigma by Jason Gross;
  • specialize with accepting partial bindings by Pierre Courtieu.
• Cumulative Polymorphic Inductive Types, allowing cumulativity of universes to go through applied inductive types, by Amin Timany and Matthieu Sozeau.
• The SSReflect plugin by Georges Gonthier, Assia Mahboubi and Enrico Tassi was integrated (with its documentation in the reference manual) by Maxime Dénès, Assia Mahboubi and Enrico Tassi.
• The coq_makefile tool was completely redesigned to improve its maintainability and the extensibility of generated Makefiles, and to make _CoqProject files more palatable to IDEs by Enrico Tassi.

More information can be found in the CHANGES file. Feedback and bug reports are extremely welcome.

This is the second release of Coq developed on a time-based development cycle. Its development spanned 9 months from the release of Coq 8.6 and was based on a public road-map. It attracted many external contributions. Code reviews and continuous integration testing were systematically used before integration of new features, with an important focus given to compatibility and performance issues.

The alleged "hack" of coq.inria.fr that led to several days of downtime for investigations was nothing more than a spam bug report. More details here.

Version 8.6.1 of Coq is available. It fixes several bugs of version 8.6. More information can be found in the CHANGES file. Feedback and bug reports are extremely welcome.

The final release of Coq 8.6 is available. Coq 8.6 includes:

• A new, faster state-of-the-art universe constraint checker by Jacques-Henri Jourdan.
• In CoqIDE and other asynchronous interfaces, more fine-grained asynchronous processing and error reporting by Enrico Tassi, making Coq capable of recovering from errors and continuing to process the document.
• Better access to the proof engine features from Ltac: goal management primitives, range selectors and a typeclasses eauto engine handling multiple goals and multiple successes, by Cyprien Mangin, Matthieu Sozeau and Arnaud Spiwack.
• Tactic behavior uniformization and specification, generalization of intro-patterns by Hugo Herbelin and others.
• A brand new warning system allowing to control warnings, turn them into errors or ignore them selectively by Maxime Dénès, Guillaume Melquiond, Pierre-Marie Pédrot and others.
• Irrefutable patterns in abstractions, by Daniel de Rauglaudre.
• The ssreflect subterm selection algorithm by Georges Gonthier and Enrico Tassi, now accessible to tactic writers through the ssrmatching plugin.
• LtacProf, a profiler for Ltac by Jason Gross, Paul Steckler, Enrico Tassi and Tobias Tebbi.

More information can be found in the CHANGES file. Feedback and bug reports are extremely welcome.

Coq 8.6 initiates a time-based release cycle, with a major version being released every 10 months. The roadmap is also made public.

To date, Coq 8.6 contains more external contributions than any previous Coq version. Code reviews were systematically done before integration of new features, with an important focus given to compatibility and performance issues.

The first release candidate of Coq 8.6 is available for testing. Coq 8.6 includes:

• A new, faster state-of-the-art universe constraint checker by Jacques-Henri Jourdan.
• In CoqIDE and other asynchronous interfaces, more fine-grained asynchronous processing and error reporting by Enrico Tassi, making Coq capable of recovering from errors and continuing to process the document.
• Better access to the proof engine features from Ltac: goal management primitives, range selectors and a typeclasses eauto engine handling multiple goals and multiple successes, by Cyprien Mangin, Matthieu Sozeau and Arnaud Spiwack.
• Tactic behavior uniformization and specification, generalization of intro-patterns by Hugo Herbelin and others.
• A brand new warning system allowing to control warnings, turn them into errors or ignore them selectively by Maxime Dénès, Guillaume Melquiond, Pierre-Marie Pédrot and others.
• Irrefutable patterns in abstractions, by Daniel de Rauglaudre.
• The ssreflect subterm selection algorithm by Georges Gonthier and Enrico Tassi, now accessible to tactic writers through the ssrmatching plugin.
• LtacProf, a profiler for Ltac by Jason Gross, Paul Steckler, Enrico Tassi and Tobias Tebbi.

More information can be found in the CHANGES file. Feedback and bug reports are extremely welcome.

Coq 8.6 initiates a time-based release cycle, with a major version being released every 10 months. The roadmap is also made public.

To date, Coq 8.6 contains more external contributions than any previous Coq version. Code reviews were systematically done before integration of new features, with an important focus given to compatibility and performance issues.

The first beta release of Coq 8.6 is available for testing. Coq 8.6 includes:

• A new, faster state-of-the-art universe constraint checker by Jacques-Henri Jourdan.
• In CoqIDE and other asynchronous interfaces, more fine-grained asynchronous processing and error reporting by Enrico Tassi, making Coq capable of recovering from errors and continuing to process the document.
• Better access to the proof engine features from Ltac: goal management primitives, range selectors and a typeclasses eauto engine handling multiple goals and multiple successes, by Cyprien Mangin, Matthieu Sozeau and Arnaud Spiwack.
• Tactic behavior uniformization and specification, generalization of intro-patterns by Hugo Herbelin and others.
• A brand new warning system allowing to control warnings, turn them into errors or ignore them selectively by Maxime Dénès, Guillaume Melquiond, Pierre-Marie Pédrot and others.
• Irrefutable patterns in abstractions, by Daniel de Rauglaudre.
• The ssreflect subterm selection algorithm by Georges Gonthier and Enrico Tassi, now accessible to tactic writers through the ssrmatching plugin.
• LtacProf, a profiler for Ltac by Jason Gross, Paul Steckler, Enrico Tassi and Tobias Tebbi.

More information can be found in the CHANGES file. Feedback and bug reports are extremely welcome.

Coq 8.6 initiates a time-based release cycle, with a major version being released every 10 months. The roadmap is also made public.

To date, Coq 8.6 contains more external contributions than any previous Coq version. Code reviews were systematically done before integration of new features, with an important focus given to compatibility and performance issues.

Version 8.5pl3 of Coq is available. It fixes several bugs of version 8.5pl2, including one critical bug. More information can be found in the CHANGES file. Feedback and bug reports are extremely welcome.

Version 8.5pl2 of Coq is available. It fixes several bugs of version 8.5pl1, including one critical bug. More information can be found in the CHANGES file. Feedback and bug reports are extremely welcome.

Version 8.5pl1 of Coq is available. It fixes several bugs of version 8.5, including one critical bug. It also brings various performance improvements. More information can be found in the CHANGES file. Feedback and bug reports are extremely welcome.

The final release of Coq 8.5 is available! The 8.5 version brings several major features to Coq:

• asynchronous edition of documents under CoqIDE to keep working on a proof while Coq checks the other proofs in the background (by Enrico Tassi);
• universe polymorphism making it possible to reuse the same definitions at various universe levels (by Matthieu Sozeau);
• primitive projections improving space and time efficiency of records, and adding eta-conversion for records (by Matthieu Sozeau);
• a new tactic engine allowing dependent subgoals, fully backtracking tactics, as well as tactics which can consider multiple goals together (by Arnaud Spiwack);
• a new reduction procedure called native_compute to evaluate terms using the OCaml native compiler, for proofs with large computational steps (by Maxime Dénès).

More information about the changes from 8.4 to 8.5 can be found in the CHANGES file. Feedback and bug reports are extremely welcome. Enjoy!

The first release candidate of Coq 8.5 is available for testing. The 8.5 version brings several major features to Coq:

• asynchronous edition of documents under CoqIDE to keep working on a proof while Coq checks the other proofs in the background (by Enrico Tassi);
• universe polymorphism making it possible to reuse the same definitions at various universe levels (by Matthieu Sozeau);
• primitive projections improving space and time efficiency of records, and adding eta-conversion for records (by Matthieu Sozeau);
• a new tactic engine allowing dependent subgoals, fully backtracking tactics, as well as tactics which can consider multiple goals together (by Arnaud Spiwack);
• a new reduction procedure called native_compute to evaluate terms using the OCaml native compiler, for proofs with large computational steps (by Maxime Dénès).

More information about the changes from 8.4 to 8.5 and since the beta releases can be found in the CHANGES file. Feedback and bug reports are extremely welcome. Enjoy!

The third beta release of Coq 8.5 is available for testing. The 8.5 version brings several major features to Coq:

• asynchronous edition of documents under CoqIDE to keep working on a proof while Coq checks the other proofs in the background (by Enrico Tassi);
• universe polymorphism making it possible to reuse the same definitions at various universe levels (by Matthieu Sozeau);
• primitive projections improving space and time efficiency of records, and adding eta-conversion for records (by Matthieu Sozeau);
• a new tactic engine allowing dependent subgoals, fully backtracking tactics, as well as tactics which can consider multiple goals together (by Arnaud Spiwack);
• a new reduction procedure called native_compute to evaluate terms using the OCaml native compiler, for proofs with large computational steps (by Maxime Dénès).

More information about the changes from 8.4 to 8.5 and since the first two beta releases can be found in the CHANGES file. Feedback and bug reports are extremely welcome. Enjoy!

The second beta release of Coq 8.5 is available for testing. The 8.5 version brings several major features to Coq:

• asynchronous edition of documents under CoqIDE to keep working on a proof while Coq checks the other proofs in the background (by Enrico Tassi);
• universe polymorphism making it possible to reuse the same definitions at various universe levels (by Matthieu Sozeau);
• primitive projections improving space and time efficiency of records, and adding eta-conversion for records (by Matthieu Sozeau);
• a new tactic engine allowing dependent subgoals, fully backtracking tactics, as well as tactics which can consider multiple goals together (by Arnaud Spiwack);
• a new reduction procedure called native_compute to evaluate terms using the OCaml native compiler, for proofs with large computational steps (by Maxime Dénès).

More information about the changes from 8.4 to 8.5 and since the first beta release can be found in the CHANGES file. Feedback and bug reports are extremely welcome. Enjoy!

Version 8.4pl6 of Coq fixes several bugs of version 8.4pl5. More information to be found in the CHANGES file.

The first beta release of Coq 8.5 is available for testing. The 8.5 version brings several major features to Coq:

• asynchronous edition of documents under CoqIDE to keep working on a proof while Coq checks the other proofs in the background (by Enrico Tassi);
• universe polymorphism making it possible to reuse the same definitions at various universe levels (by Matthieu Sozeau);
• primitive projections improving space and time efficiency of records, and adding eta-conversion for records (by Matthieu Sozeau);
• a new tactic engine allowing dependent subgoals, fully backtracking tactics, as well as tactics which can consider multiple goals together (by Arnaud Spiwack);
• a new reduction procedure called native_compute to evaluate terms using the OCaml native compiler, for proofs with large computational steps (by Maxime Dénès).

More information about the changes from 8.4 to 8.5 can be found in the CHANGES file. Feedback and bug reports are extremely welcome. Enjoy!

Version 8.4pl5 of Coq fixes several bugs of version 8.4pl4 including the compatibility with OCaml 4.02. More information to be found in the CHANGES file.

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

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 recipients of the award are thanking all developers who contributed to the success of Coq, the users who illustrated how to use Coq for so many impressive projects in formal certification, programming, logic, formalization of mathematics and teaching as well as the whole surrounding scientific community in proof theory, type theory, programming languages, interactive theorem proving.

All over 30 years, Coq also benefited from the trust and support from Inria and from its partners, CNRS, ENS Lyon, University Paris-Sud, École Polytechnique, University Paris-Diderot.

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.

Look here for more on the award.

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 2011 will be held on August 26 at Nijmegen, as part of ITP 2011.

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.

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.

We are pleased to announce the final release of Coq 8.3 which includes a new tactic (nsatz, standing for Hilbert's NullStellensatz, that extends ring to systems of polynomial equations) and a few new libraries (a certification of mergesort, a new library of finite sets with computational and logical contents separated).

This version also comes with many improvements of existing features, especially regarding the tactics, the module system, extraction, the type classes, the program command, libraries, coqdoc. Here is an excerpt:

• new operator <+ for conveniently chaining application of functors
• new round of extension of the modular library of arithmetic
• support for matching terms with binders in Ltac,
• linking notations in coqdoc,
• quote tactic now working on arbitrary expressions,
• Lemma and co accept parameters that are automatically introduced,
• interactive proofs in module types,
• a beautifying coqc option for pretty-printing files

See the file CHANGES for a full log of changes.

Even if we try to preserve compatibility as much as possible with Coq 8.2, we had to arbitrate for a break of behavior in some situations. The major incompatibilities can be easily treated by using the new -compat 8.2 option or by setting/unsetting adequate options. See COMPATIBILITY for details and migration recommendations.

In addition to the "ssreflect" plugin, extension packages we are aware about include the following (but probably there are more):

• the Heq library for smooth rewriting using heterogeneous equality by C.-K. Hur;
• the aac_tactics plugin for rewriting modulo associativity and commutativity by T. Braibant and D. Pous.

Note also the following user contributions submitted since 8.2 was released:

• Projective geometry in plane and space (N. Magaud, J. Narboux, P. Schreck)
• Proofs of Quicksort's worst- and average-case complexity (Eelis)
• Tactic that helps to prove inductive lemmas by fixpoint "descente infinie" functions (M. Li)
• A tactic for deciding Kleene algebras (T. Braibant and D. Pous)

If you want to try it, go to the download page.

The Coq development team

Coq Modulo Theories (CoqMT) is an extension of the Coq proof assistant (8.2) that embeds, in its computational mechanism, validity entailment for user-defined first-order equational theories.

The alpha-release is out.

The 2nd Asian-Pacific Coq Summer School will take place from the 20th to the 27th of August 2010 at Tsinghua University, Beijing, China.

This summer school will provide an up-to-date one-week introduction by European experts to the Coq proof assistant. This course is intended to Master and PhD students, and professors and researchers interested in learning how to use this state-of-the-art tool.

The Coq Workshop 2010 will be held on July 9 at Edinburgh. The program is out.

The Coq developpers are pleased to announce the release of the beta version of Coq 8.3. This release intends to give the curious and impatient users of Coq a flavour of what Coq 8.3 will be. To see what is new in this version of Coq, please refer to the CHANGES file.

Please be aware that this release should be considered as unstable, and should not be used as a production environment.

Now that you have been warned, you can download the source files.

The Mathematical Components Team, at the Microsoft Research-Inria Joint Center released a new version of Ssreflect, an powerful extension for Coq. For more information, read the official announcement:

«
We are pleased to announce the new release of the Ssreflect
extension library for the Coq proof assistant, version
8.2/8.2pl1. This release includes:
- an update of the tactic language which complies with the new version
of Coq;
- an update of the combinatoric libraries distributed in the previous
release of ssreflect;
- a new set of libraries for abstract algebra.

The name Ssreflect stands for "small scale reflection", a style of
proof that evolved from the computer-checked proof of the Four Colour
Theorem and which leverages the higher-order nature of Coq's
underlying logic to provide effective automation for many small,
clerical proof steps. This is often accomplished by restating
("reflecting") problems in a more concrete form, hence the name. For
example, in the Ssreflect library arithmetic comparison is not an
abstract predicate, but a function computing a boolean.

Along with documentation, also available at
https://hal.inria.fr/inria-00258384 the Ssreflect distribution
comprises two parts:
- A new tactic language, which promotes more structured, concise and
robust proof scripts, and is in fact independent from the "reflection"
proof style. It is implemented as a linkable extension to the Coq
system.
- A set of Coq libraries that provide core "reflection-oriented"
theories for
+ basic combinatorics: arithmetic, lists, graphs, and finite sets.
+ abstract algebra: an algebraic hierarchy from
additive groups to closed fields, polynomials, matrix,
basic finite group theory, infrastructure for finite summations,...)

Some features of the tactic language:
- It provides tacticals for most structural steps (e.g., moving
assumptions), so that script steps mostly match logical steps.
- It provides tactics and tatical to support structured layout,
including reordering subgoals and supporting "without loss of
generality" arguments.
- It provides a powerful rewriting tactic that supports chained
rules, automatic unfolding of definitions and conditional rewriting,
as well as precise control over where and how much rewriting occurs.
- It can be used in combination with the classic Coq tactic language.

Some features of the library:
- Exploits advanced features of Coq such as coercions and canonical
projections to build generic theories (e.g., for decidable equality).
- Uses rewrite rules and dependent predicate families to state
lemmas that can be applied deeply and bidirectionally. This means
fewer structural steps and a smaller library, respectively.
- Uses boolean functions to represent sets (i.e., comprehensions),
rather than an ad hoc set algebra.

The Ssreflect 1.2 distribution is available at
http://www.msr-inria.inria.fr/projects/mathematical-components-2/
It is distributed under either one (your choice) of the CeCILL-B or CeCILL
version 2 licences (the French equivalent of the BSD and GNU GPL licenses,
respectively).

The tactic language is quite stable; we have been using it
internally for three years essentially without change. We will support
new releases of Coq in due course. We also plan to extend the core
library as our more advanced work on general and linear algebra
progresses.

Comments and bug reports are of course most welcome, and can be
directed at ssreflect(at-sign)msr-inria.inria.fr. To subscribe, either
send an email to sympa@msr-inria.inria.fr, whose title contains the
word ssreflect, or use the following web interface:
https://sympa.inria.fr/sympa/info/ssreflect

Enjoy!

The Mathematical Components Team, at the Microsoft Research-Inria
Joint Center
»

A new patch level for Coq 8.2 is now available. You can get it from the download page.

Thomas Braibant and Damien Pous are pleased to announce the first release of ATBR, a Coq library whose aim is to provide tools for working with various algebraic structures, including non-commutative idempotent semirings and Kleene algebras.

The main tactic they provide in this library is a reflexive tactic for solving (in)equations in Kleene algebras. The decision procedure goes through standard finite automata constructions, that they formalized.

For example, this tactic automatically solves goals of the form a#*(b+a#*(1+c))# == (a+b+c)# or a*b*c*a*b*c*a# <= a#*(b*c+a)#, where a, b, and c are elements of an arbitrary Kleene algebra (binary relations, regular languages, min-max expressions...), # is the (postfix) star operation, * is the infix product or concatenation operation, + is the sum or union operation, and 1 is the neutral element for *.

In order to define this tactic, they had to work with matrices, so that the ATBR library also contains a new formalisation of matrices in Coq along with a set of tools (notably, "ring"-like tactic for matrices whose dimensions are not necessarily uniform).

More details can be found from Coq user contribution web-page

In particular, a Coq file illustrating the kind of tools we provide can be found there.

The first Asian-Pacific Coq summer school will be held in China, in the Future Internet Technology Research Center (FIT) of Tsinghua University, from 24^th to 30^th, august 2009.

More information and registration on the Asian-Pacific Coq summer school web page.

The Ott tool, developed by Peter Sewell and Francesco Zappa Nardelli, has recently been extended to compile language definitions to a Coq representation in locally-nameless style with cofinite quantification, as popularised in Engineering Formal Metatheory by Aydemir, Charguéraud, Pierce, Pollack and Weirich. It deals with the single-binder case only.

Some examples (including STLC, Fsub, and the nu-calculus of Pitts and Stark) and the documentation are available from the ln-ott page and the project web-site.

This is related to the recent LNgen tool of Brian Aydemir and Stephanie Weirich.

Stephanie Weirich and Brian Aydemir are pleased to announce LNgen, a prototype tool for generating Coq code for the infrastructure associated with a locally nameless representation. This work builds upon their work with Charguéraud, Pierce, and Pollack on Engineering Formal Metatheory, where they described a locally nameless strategy for representing languages with binding.

LNgen uses a subset of the Ott specification language as its input language. Currently, it supports the definition of syntax with single binders. Compared to the recently announced locally nameless backend for Ott, LNgen does not handle the definition of relations, but it does generate a large collection of "infrastructure" lemmas and their proofs, e.g., facts about substitution.

Call for papers

The Coq workshop will bring together Coq users, developers and
contributors. The workshop will be organized from submitted papers,
invited talks and a plenary discussion on the evolution and design of
Coq. Topics for submitting a paper include:

• Language or tactics features
• Theory and implementation of the Calculus of Inductive Constructions
• Applications and experience in education and industry
• Tools, platforms built on Coq
• Plugins, libraries for Coq
• Interfacing with Coq
• Formalization tricks and Coq pearls

Authors should send their papers to Hugo.Herbelin@inria.fr. Submitted
papers should be in (postscript or) portable document format. Papers
should not exceed 12 pages in length in single-column full-page 11pt A4
style.

If there is sufficient demand, we will try to organize a time slot for
demonstrations. Similarly, we may also organize a session on the lessons
learned from teaching Coq. If you are interested, please send a brief
proposal.

Venue:

TPHOLs 2009, Munich, Germany

Important Dates:

• Papers Due: May 11, 2009
• Acceptance Notification: June 23, 2009
• Workshop: August 21, 2009

Program committee:

• Yves Bertot
• Frédéric Blanqui
• Jacek Chrzączsz
• Eduardo Giménez
• Georges Gonthier
• Hugo Herbelin (chair)
• Greg Morrisett
• David Nowak
• Benjamin Pierce

Coq 8.2 brings Haskell-style type classes, various evolutions of the arithmetic libraries, and many other various improvements and extensions regarding the module system, tactics, syntax, etc. You can download it from this page.
Enjoy!

The Coq development team

A release candidate for Coq 8.2 is now out ! You can download it from this page.

The patch level 4 release of Coq 8.1 is out. See the download page.

The beta release of Coq 8.2 is now out. For more informations, look at this page.

The Microsoft Research-Inria Joint Center is pleased to announce
the first full release of the Ssreflect extension library for the Coq
proof assistant, version 8.1.

The name Ssreflect stands for "small scale reflection", a style of
proof that evolved from the computer-checked proof of the Four Colour
Theorem and which leverages the higher-order nature of Coq's
underlying logic to provide effective automation for many small,
clerical proof steps. This is often accomplished by restating
("reflecting") problems in a more concrete form, hence the name. For
example, in the Ssreflect library arithmetic comparison is not an
abstract predicate, but a function computing a boolean.

Along with documentation, also available at
https://hal.inria.fr/inria-00258384 the Ssreflect distribution
comprises two parts:
- A new tactic language, which promotes more structured, concise and
robust proof scripts, and is in fact independent from the "reflection"
proof style. It is implemented as a linkable extension to the Coq
system.
- A set of Coq libraries that provide core "reflection-oriented"
theories for basic combinatorics (roughly: arithmetic, lists, and
finite sets).

Some features of the tactic language:
- It provides tacticals for most structural steps (e.g., moving
assumptions), so that script steps mostly match logical steps.
- It provides tactics and tactical to support structured layout,
including reordering subgoals and supporting "without loss of
generality" arguments.
- It provides a powerful rewriting tactic that supports chained
rules, automatic unfolding of definitions and conditional rewriting,
as well as precise control over where and how much rewriting occurs.
- It can be used in combination with the classic Coq tactic
language.

Some features of the library:
- Exploits advanced features of Coq such as coercions an canonical
projections to build generic theories (e.g., for decidable equality).
- Uses rewrite rules and dependent predicate families to state
lemmas that can be applied deeply and bidirectionally. This means
fewer structural steps and a smaller library, respectively.
- Uses boolean functions to represent sets (i.e., comprehensions),
rather than an ad hoc set algebra.

The Ssreflect 1.1 distribution is available at
http://www.msr-inria.inria.fr/projects/mathematical-components-2/. It is
distributed under the CeCill-B license (the French equivalent of the
BSD license).

The tactic language is quite stable; we have been using it
internally for two years essentially without change. We will support
new releases of Coq in due course. We also plan to extend the core
library as our more advanced work on general and linear algebra
progresses.

Comments and bug reports are of course most welcome, and can be
directed at ssreflect(at-sign)msr-inria.inria.fr. To subscribe, either
send an email to sympa@msr-inria.inria.fr, whose title contains the
word ssreflect, or use the following web interface:
https://sympa.inria.fr/sympa/info/ssreflect

Enjoy!

The Mathematical Components Team,
at the Microsoft Research-Inria Joint Center

Frédéric Blanqui is pleased to announce a new release of CoLoR.
You can download it and find more details on http://color.loria.fr/.
The most important new features are:

• arctic matrix interpretations [Koprowski, Waldmann]
• strongly connected components of a graph [Ducas]
• decomposition of a termination problem into sub-problems using the SCC decomposition of its dependency graph [Ducas]
• some support for classical reasoning [Blanqui]

enjoy!

Après des mois douloureux de gestation, le nouveau site de Coq est enfin en ligne. Enjoy it !