Clone this wiki locally
Coq is a proof assistant based on the calculus of constructions. It is used to formalize proofs in a variety of fields, including mathematics and programming languages. Cocorico is the Coq wiki.
Note: this wiki has been converted in October 2017 from an earlier wiki based on MoinMoin. Some help on this Wiki. More about this migration. In case of need, this earlier wiki is still here for the moment, in read-only mode.
You need to install Coq and either CoqIDE (recommended for beginners) or Proof General (recommended for emacs users).
- Installation of the Coq system:
- Configuration of CoqIDE
- Configuration of Proof General (to be completed)
- Installation of plugins (to be completed)
- Tips on Makefiles for Coq (to be completed)
Coq official resources
- The Coq Reference Manual
- The Coq Standard Library
- The Coq-Club mailing list
- The Coq bug tracker
- The Coq gitter (web chat)
- The Coq FAQ (no longer maintained)
- The Coq IRC channel:
- Volume 1: Logical Foundations (by Benjamin C. Pierce et al.)
- Volume 2: Programming Language Foundations (by Benjamin C. Pierce et al.)
- Volume 3: Verified Functional Algorithms (by Andrew Appel)
- Certified Programming with Dependent Types, by Adam Chlipala
- CoqArt' (book), by Yves Bertot and Pierre Castéran
- Other tutorials...
- Teaching Coq and teaching with Coq
- The Contributing Guide
- Coq Working Groups
- The next Coq Working Group
- Ideas for the Google Summer of Code 2016
- Procedures related to continuous integration
- Wishes for Coq (and a specific page of wishes for unification)
- Wishes for Graphical User Interfaces (and a specific page for CoqIDE wishes)
- A development tutorial
- Development frequently asked questions
- List of maintainers
- Road maps
- Archive of discussions
Pointers to existing projects involving Coq.
A non-exhaustive list of Coq libraries that are being used by other people than the developers.
- Mathematical Components: formalization of mathematical theories, focusing in particular on group theory.
- Flocq: formalization of floating-point computations.
- TLC: a non-constructive library for Coq: an alternative to Coq's standard library.
- Coq ExtLib: A collection of theories and plugins that may be useful in other Coq developments.
(to be completed)
Coq plugins and tools
(section to be updated)