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

Lecture: MW 9:30–10:50 AM, CIT 241

Office Hours: M 11-12 AM, CIT 203

Course Content

We plan to cover most of the Hitchhiker’s Guide to Logical Verification. We'll cover chapters roughly according to the schedule below, but topics may shift slightly as the semester progresses.

• Basics
  • 1. Types and Terms
  • 2. Programs and Theorems
  • 3. Backward Proofs
  • 4. Forward Proofs
• Functional-Logic Programming
  • 5. Functional Programming
  • 6. Inductive Predicates
• Program Semantics
  • 9. Operational Semantics
• Mathematics
  • 12. Logical Foundations
  • 13. Basic Mathematical Structures
  • 14. Rational and Real Numbers
• Meta-Reasoning
  • 7. Monads
  • 8. Metaprogramming

Assignments

Homework

Homework will be submitted via Gradescope. Please ensure that you have familiarized yourself with the grading and collaboration policies in the syllabus.

Labs

Labs are optional, TA-guided sessions that provide an opportunity to practice and reinforce the content covered in lecture.

Lectures

You can view lecture demo files and view lecture recordings here. We will aim to update this table shortly after each lecture. All lecture recordings can also be found on Panopto.

Calendar

Resources

CSCI 1715 Links

• Syllabus
• Setup Instructions
• Course GitHub Repository
• Ed Discussion
• Anonymous Feedback Form
• Extension Request Form
• The Hitchhiker's Guide to Logical Verification, the course textbook
• Final Project Information

Lean Documentation & Search Tools

• Lean Language Reference
• Mathlib4 API documentation
• LeanSearch, a search tool for Mathlib4
• An index of Lean tactics

Lean Manuals

• The Hitchhiker's Guide to Logical Verification, the course textbook
• The Lean Language Manual
• Functional Programmming in Lean, a text focusing on Lean as a programming language instead of a theorem prover
• Metaprogramming in Lean 4, a reference to programming-for-proving
• Theorem Proving in Lean 4, a comprehensive introduction to the system
• Concrete Semantics: With Isabelle/HOL, a textbook that covers similar material in a different proof assistant

Community Resources

• The leanprover-community website
• The Lean Zulip Chat is a very active and very helpful discussion site. Search the history here, or post questions in the “New Members” stream. (Note: please don’t ask course-specific questions here. When in doubt, talk to the course staff first. This is a great resource if you want to learn beyond our course!)

Staff

To email the course staff, click here. To email just the HTA and Rob, click here. To email Rob directly, click here. You are also encouraged to post (and answer!) questions on Ed Discussion.

Robert Y. Lewis

Professor

Call me Rob! I'm half computer scientist, half mathematician, and fully excited to go through some of my favorite material with you all this semester. Pronouns: he/him/his

Chloe Qiao

HTA

Hi! I'm a junior concentrating in computer science. When I'm not in the CIT, I enjoy rock-climbing, DDR, and building puzzlehunt sites. Pronouns: she/her/hers