This course will focus on Programming Proofs, in two senses. In the first sense, we will learn how to write a mathematical proof inside a proof assistant, a tool for writing proofs that are mechanically checked by a computer. These proofs resemble, and fundamentally are, programs, hence we will be programming our proofs. In the second sense, we will learn how to write proofs about programs, from proving that they avoid a certain class of errors to precisely characterizing their behavior. Our tool of choice will be the Coq proof assistant, though the lessons in this course will easily carry over to other proof assistants like Isabelle, Agda, and Lean.
Professor Rand: F 2:00-3:30, JCL 313.
Benjamin Caldwell (TA): MW 1:30-3:00, JCL 205.
Before coming to class, students should install the following software:
The Coq proof assistant
An IDE: Proof General (emacs) or VsCoq (visual studio code), depending on your preference. If you use Proof General, I recommend adding Company-Coq. The CoqIDE that comes with Coq will also work but it has historically been clunkier.
This class will follow a modified version of volume one of Software Foundations: Logical Foundations along with a bit of volume two, Programming Languages Foundations. We will cover mathematical logic in Coq, data structures and proofs about such structures, programming languages and type systems, and proof automation. We will also spend time on the Curry-Howard (or Programs as Proofs) Isomorphism, which underlies the Coq proof assistant. Most classes will consist of live coding which in context will often mean live proof. Materials will be provided both before and after class, so students can follow along in class and review afterward. (The review material will also contain exercises.) This format should translate easily to an online learning environment for the first two weeks of class.
We will cover the first three topics below and 1-3 of the remaining topics, time permitting.
Half of a student's grade will come from homework drawn from the Software Foundations books as we cover it. Exercises labeled advanced will only be required of students enrolled in the graduate section. The remainder of the grade will come from a midterm (25%) and a final project (25%).
| Date | Topic | Class Material | After Class | Notes |
| Jan 11 | Introduction to the Coq Proof Assistant | Basics.v | Basics.v | Due Jan 18. |
| Jan 13 | Induction | Induction.v | Induction.v | Due Jan 20. |
| Jan 18 | Data Structures | Lists.v | Lists.v | Due Jan 25. |
| Jan 20 | Polymorphism | Poly.v | Poly.v | Due Jan 27. |
| Jan 25 | Tactics | Tactics.v | Tactics.v | Due Feb 1. |
| Jan 27 | Logic | Logic.v | Logic.v | Due Feb 8 (extended). |
| Feb 01 | Inductive Propositions | IndProp.v | IndProp.v | Due Feb 8. |
| Feb 03 | Proofs and Programs | ProofObjects.v | ProofObjects.v | Due Feb 10. |
| Feb 08 | Induction Principles | IndPrinciples.v | IndPrinciples.v | Due Feb 15. |
| Feb 10 | Maps | Maps.v | Maps.v | Due Feb 17. |
| Feb 15 | Midterm | midterm_2022.v | midterm_2022_sol.v | |
| Feb 17 | The Imp Language | Imp.v | Imp.v | Due Feb 24. |
| Extra | Automation | Auto.v | Some automation for those interested. (No homework.) | |
| Feb 22 | Program Equivalence | Equiv.v | Equiv.v | Due Mar 3. |
| Feb 24 | Hoare Logic | Hoare.v | Hoare.v | Due Mar 8. |
| Mar 01 | Project Proposal Due | |||
| Mar 01 | More Hoare Logic | Hoare2.v | Hoare2.v | Due Mar 8. |
| Mar 03 | Small Step Semantics | Smallstep.v | Smallstep.v | Due Mar 10. |
| Mar 08 | Types | Types.v | Types.v | Due Mar 15. |
| Mar 10 | Typed Lambda Calculus | Stlc.v | Stlc.v | No homework. |
| Mar 15 | Final Projects Due | Good luck! |