CS 1951X: Formal Proof and Verification / Fall 2021

Looking for the Fall 2022 site? Click here!

Course Description

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.

Syllabus: syllabus.pdf

Time and Location: MW 3:00-4:20pm, CIT 165

Course content

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.

• Basics
  • 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
• Mathematics
  • 11. Logical Foundations
  • 12. Basic Mathematical Structures
  • 13. Rational and Real Numbers
• Meta-Reasoning
  • 6. Monads
  • 7. Metaprogramming
  • 9. Hoare Logic

Previous Offerings

• Fall 2021 (Vrije Universiteit Amsterdam, in progress)
• Fall 2020 (Vrije Universiteit Amsterdam)

Instructors

Robert Y. Lewis

Teaching Assistants

Gareth Mansfield

Anirudh Narsipur

Walter Zhang