Coq installation

You need to install Coq and either CoqIDE (recommended for beginners) or Proof General (recommended for emacs users).

• Installation of the Coq system:

  • Installation of Coq on Linux

  • Installation of Coq on Mac (to be completed)

  • Installation of Coq on Windows (to be completed)

• 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: subscription archive

• The Coq bug tracker

• The Coq FAQ (no longer maintained)

• The Coq IRC channel: irc://irc.freenode.net/#coq

Coq tutorials

• 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

• Other tutorials...

• Teaching Coq and teaching with Coq

Coq community

Pointers to existing projects involving Coq.

• Formal programming language research in Coq

• Formal mathematics in Coq

Coq libraries

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.

(to be completed)

Coq plugins and tools

• Plugins and tools for Coq

(section to be updated)

Coq's logic

• Axioms that can safely be added to Coq

• Papers about Coq's theoretical foundations

Coq Wiki

• Manual pages for this wiki

• Editing the current front page

• Old articles

• Old versions of the front page