CMSC 22400/32400: Programming Proofs (Winter 2022)


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.

Office Hours

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:


This class will follow a modified version of volume one of Software FoundationsLogical 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. 

Proofs as Programs
Basic Coq, Propositional and Predicate Logic, Dependent Types, Induction as Recursion
Data Structures
Proofs about Numbers, Lists, Trees, Maps, and other standard structures
Reasoning About Programs
Embedded Programs, Program Semantics, Evaluation, and Equivalence
Lightweight and heavyweight approaches to automation proofs
Type Theory
The simply-typed lambda calculus, type soundness
Hoare Logic
Logics for proving program correctness


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!