Coq proof assistant

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

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

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

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

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

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

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

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

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 ... [More] 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 [email protected], 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 » [Less]