Coq proof assistant

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.

The Coq Workshop 201! 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 ... [More] 2010), and to show them the state of art applications of proof assistants and theorem provers in formal methods. [Less]

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 ... [More] 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 [Less]

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 ... [More] 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 [Less]

We are pleased to announce the final release of Coq 8.3 which includes a new tactic ("nsatz", standing for Hilbert's NullStellensatz, that solves systems of polynomial equations in Z or R) and a few new libraries (a certification of mergesort, a new ... [More] 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: read more [Less]

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.

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.

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.