Projects / Coq


The Coq tool is a proof assistant which is able to handle calculus assertions, to check proofs of these assertions mechanically, and to extract a certified program from the constructive proof of its formal specification.

Operating Systems

Recent releases

  •  11 Aug 2009 12:04

    Release Notes: Various bugs were fixed.

    •  18 Feb 2009 08:19

      Release Notes: This release 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.

      •  25 Aug 2006 10:27

        Release Notes: The search depth argument of auto can be parameterised in the Ltac language. The constr_may_eval entry was added for tactic extensions. A couple of lemmas of ZArith were renamed. This concerns names containing O (the letter), which is replaced by 0 (the number).

        •  09 May 2005 05:23

          Release Notes: GPL-incompatible QPL files for CoqIde are now under the GPL. Pretty-printing of coercions to Funclass were fixed and improved.

          •  21 Apr 2004 18:03

            Release Notes: This is a new major evolution of the Coq system. It features a more extensible logical system due to the removal of the impredicativity of the sort Set, a completely new syntax, an automatic translator from the old to the new syntax, a new notion of "interpretation scopes", a revised and simplified standard library, a new automation tactic for first-order statements, and a new integrated GTK-based user interface.


            Project Spotlight


            A Fluent OpenStack client API for Java.


            Project Spotlight

            TurnKey TWiki Appliance

            A TWiki appliance that is easy to use and lightweight.