It is recommended that you use opam to install the Rocq prover. This course will use version 20.0 of the Rocq prover.

There are IDEs of varying levels of sophistication that you can use for your Rocq development:

• Proof General in Emacs
• VSCoq in Visual Studio Code
• Coqtail in Vim
• CoqIDE

Texts:

• Coq'Art: The Calculus of Inductive Constructions
• Software Foundations
• Certified Programming with Dependent Types
• Formal Reasoning About Programs