Installing the Coq proof assistant

  • Download and install the last version of Coq (from sources or with binaries):
  • Install an IDE for interacting with Coq
    • a standalone IDE distributed with Coq (easier for beginners but difficult to install on some platforms): CoqIDE
    • a Emacs mode: Proof General

Lecture 1: Motivations and Examples

Lecture 2: Coq Crash Course

Lecture 3

Lecture 4