News

Coq 8.5 beta 2 is out!

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!

Coq 8.4pl6 is out

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

Coq 8.5 beta 1 is out!

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!

Coq 8.4pl5 is out

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.

Coq is hiring a specialized engineer for 2 years

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

Coq 8.4pl4 is out

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.

Coq received ACM Software System 2013 award

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.

Coq source repository migrated to git

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 :-)

Coq received ACM SIGPLAN Programming Languages Software 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.

Look here for more on the award.

Coq 8.4 is out!

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.

Release candidate of Coq 8.4 is out

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

Beta-release of Coq 8.4

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

Coq 8.3pl3 is out

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.

Coq Workshop 2011

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

3rd Asian-Pacific Summer School on Formal Methods

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.

Coq 8.3pl2 is out

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.

Coq 8.3 is out !

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

Alpha-release of Coq Modulo Theories

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.

2nd Asian-Pacific Coq Summer School

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.

Coq Workshop 2010

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

Coq 8.3 beta version

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.

Announcing Ssreflect version 1.2

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
»

Coq 8.2pl1 is out !

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

A tactic for deciding Kleene algebras

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.

First Asian-Pacific Coq Summer School

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

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

A locally-nameless backend for Ott

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.

Announcing LNgen

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.

The Coq workshop 2009

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 has arrived

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

Coq 8.2 release candidate

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

Bug-fix release for Coq 8.1

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

Release of Coq 8.2 (beta)

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

Announcing Ssreflect 1.1

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

New CoLoR release

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!

Le nouveau site est en ligne !

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