The Coq Proof Assistant

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 !