Coq

Coq is a proof assistant based on the Calculus of Inductive Constructions.

Coq is notable for being based on tactics. Instead of writing a term in type theory itself, the user uses a tactic, which builds a term in stages. The behaviour of tactics may range from simple term-building steps (i.e. intro to introduce a \lambda-abstraction) to fully automated proof construction (e.g. decision procedures such as lia or tauto).

Universes

Coq supports three kinds of universes:

• Prop, an impredicative universe of propositions
• Set, a predicative universe of small types
• various levels of Type, a predicative universe of large types

Historically, Set used to also be impredicative. This was changed in version 8.0 due to the incompatibility of impredicativity with various axioms of mainstream mathematics and classical logic. This is explained in detail in a GitHub wiki post by Pierre-Marie Pédrot.

Books

There are at least two introductory books based on Coq:

• Sofware Foundations
• Certified Programming with Dependent Types

References

• The Wikipedia page on Coq has quite a bit of historical information.