Coq is 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 a Coq wiki.
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 Proof General (to be completed)
Installation of plugins (to be completed)
Tips on Makefiles for Coq (to be completed)
Coq official resources
The Coq FAQ (no longer maintained)
The Coq IRC channel: irc://irc.freenode.net/#coq
Software Foundations, by Benjamin C. Pierce et al
Certified Programming with Dependent Types, by Adam Chlipala
CoqArt' (book), by Yves Bertot and Pierre Castéran
Pointers to existing projects involving Coq.
A non-exhaustive list of Coq libraries that are being used by other people than the developers.
SSReflect: 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)