CS 1951X: Formal Proof and Verification / Fall 2021
Proof assistants are tools that are used to check the correctness of programs. Unlike tools like model checkers and SAT solvers, proof assistants are highly interactive. Machine-checked formal proofs lead to trustworthy programs and fully specified reliable mathematics.
This course introduces students to the theory and use of proof assistants, using the system Lean. We will use Lean to verify properties of functional programs and theorems from pure mathematics. We will learn the theory of deductive reasoning and the logic that these tools are based on.
Time and Location: MW 3:00-4:20pm, CIT 165
Rob is new to Brown, and this course has never been taught here before. We plan to cover the entire Hitchhiker’s Guide to Logical Verification. However, this text is tuned to a different course and a different schedule, and we want to leave room for improvisiation!
For this reason we are not scheduling specific lectures far in advance. Instead, we’ll work through the chapters Hitchhiker’s Guide in this order. The Lectures page will keep a record of what we’ve done so far and what’s coming in the next few classes.
- 1. Definitions
- 2. Backward Proofs
- 3. Forward Proofs
- Functional-Logic Programming
- 4. Functional Programming
- 5. Inductive Predicates
- Program Semantics
- 8. Operational Semantics
- 10. Denotational Semantics
- 11. Logical Foundations
- 12. Basic Mathematical Structures
- 13. Rational and Real Numbers
- 6. Monads
- 7. Metaprogramming
- 9. Hoare Logic