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
- an update of the combinatoric libraries distributed in the previous
release of ssreflect;
- a new set of libraries for abstract algebra.
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.
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
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.
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.
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.
The Coq development team