Lean

Installation instructions for Lean can be found here.

The Lean community maintains a rich set of resources for learning Lean. Here are some recommended for this course:

• Theorem Proving in Lean
• Functional Programming in Lean
• The Hitchhiker's Guide to Logical Verification in Lean
• Metaprogramming in Lean 4
• Tactic cheat sheet

Rocq

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