Introduction to Computational Logic

• We follow the MPCTT book (draft, may be updated)
• Coq files accompanying the chapters of the book (at github, may be updated)
• Videos including lectures
• We use the Coq Proof assistant: 
  • Coq Homepage
  • Reference Manual
  • Standard Library
  • Commands
  • Tactics
• Related online books
  • An online book on software foundations starting with an introduction to Coq (by Benjamin Pierce and others)
  • A book on certified programming with dependent types using Coq (by Adam Chlipala)
  • Computational type theory, a survey by Robert L. Constable in Scholarpedia
  • The HoTT book, online book on (homotopy) type theory

Installing the Coq proof assistant

Make sure you have the Coq proof assistant working before the first lecture.

• There are several ways to install Coq (Version 8.13). Make sure to enable/install the "equations" package. 
  • Linux/macOS/Windows: Install the Coq Platform.
  • Linux/macOS: Install Coq via the the OCaml package manager opam. See also Coq-on-Linux.
  • Windows: Download the Windows installer from the release page.
• There are three user interfaces for Coq: CoqIDE, Proof General, and VSCode. You can choose which one you want to use.
  • CoqIDE: You can download and install CoqIDE along with the rest of Coq via opam and it is included in the Windows installer. Documentation about CoqIDE can be found here.
  • Proof General: Proof General is an emacs mode that supports many theorem provers, including Coq. Using Proof General, Company Coq is an extension allowing you to look up lemmas and the Coq Documentation. Both Proof General and Company Coq can be installed via the emacs package archive melpa.
  • VSCode: You can interact with Coq using VSCode using the VSCoq plugin.