Interactive theorem proving
Summary
A hands-on introduction to interactive theorem proving, computer-checked mathematics, compiler verification, proofs as programs, dependent types, and proof automation. Come learn how to write computer-checked proofs and certified bug-free code!
Content
- Intro to the Coq proof assistant (logic, higher-order functions, tactics)
- Functional programming (inductive types and fixpoints)
- Structural induction (data structures and verified algorithms)
- Interpreter-based program semantics (intro to compiler verification)
- Inductive relations (predicates, rule induction)
- Automation and tactics I (bottom-up reasoning and logic programming)
- Operational program semantics (small-and big-step semantics)
- Program logics (hoare triples)
- Automation and tactics II (top-down reasoning)
- Type systems (Simply-typed lambda calculus)
- Dependent types and equality proofs
- Automation and tactics III (proofs by reflection)
- Real-world theorem proving (various topics)
Learning Prerequisites
Recommended courses
This course assumes no knowledge of programming language theory. The following courses may be useful, but are not required:
- CS-320 Computer language processing (to introduce the concept of interpreter)
- CS-425 Foundations of software (to introduce type systems and the lambda calculus)
- CS-550 Formal verification (for a different perspective on theorem proving)
Important concepts to start the course
- Functional programming
Learning Outcomes
- Implement purely-functional algorithms in the Gallina language
- Translate informal requirements about software into precise mathematical properties
- Plan and carry out mechanized proofs in Coq (e.g. maths, algorithms, compilers, type systems)
- Automate repetitive proof tasks by crafting simple custom decision procedures
Teaching methods
- Lectures
- Live-coding sessions
Expected student activities
- Lectures
- Programming and verification assignments
- Project (proposal, check-in, presentation, report)
Assessment methods
- Take-home programming and verification assignments: 40% of the final grade (3 or 4 labs)
- Formal verification project: 60% of the final grade (~10 weeks, in teams of 1 to 4 students)
Supervision
| Office hours | Yes |
| Assistants | No |
| Forum | Yes |
In the programs
- Semester: Spring
- Exam form: During the semester (summer session)
- Subject examined: Interactive theorem proving
- Courses: 2 Hour(s) per week x 14 weeks
- Exercises: 1 Hour(s) per week x 14 weeks
- Lab: 2 Hour(s) per week x 14 weeks
- Type: optional
- Semester: Spring
- Exam form: During the semester (summer session)
- Subject examined: Interactive theorem proving
- Courses: 2 Hour(s) per week x 14 weeks
- Exercises: 1 Hour(s) per week x 14 weeks
- Lab: 2 Hour(s) per week x 14 weeks
- Type: optional
- Semester: Spring
- Exam form: During the semester (summer session)
- Subject examined: Interactive theorem proving
- Courses: 2 Hour(s) per week x 14 weeks
- Exercises: 1 Hour(s) per week x 14 weeks
- Lab: 2 Hour(s) per week x 14 weeks
- Type: optional
- Semester: Spring
- Exam form: During the semester (summer session)
- Subject examined: Interactive theorem proving
- Courses: 2 Hour(s) per week x 14 weeks
- Exercises: 1 Hour(s) per week x 14 weeks
- Lab: 2 Hour(s) per week x 14 weeks
- Type: optional
- Semester: Spring
- Exam form: During the semester (summer session)
- Subject examined: Interactive theorem proving
- Courses: 2 Hour(s) per week x 14 weeks
- Exercises: 1 Hour(s) per week x 14 weeks
- Lab: 2 Hour(s) per week x 14 weeks
- Type: optional
- Semester: Spring
- Exam form: During the semester (summer session)
- Subject examined: Interactive theorem proving
- Courses: 2 Hour(s) per week x 14 weeks
- Exercises: 1 Hour(s) per week x 14 weeks
- Lab: 2 Hour(s) per week x 14 weeks
- Type: optional
- Semester: Spring
- Exam form: During the semester (summer session)
- Subject examined: Interactive theorem proving
- Courses: 2 Hour(s) per week x 14 weeks
- Exercises: 1 Hour(s) per week x 14 weeks
- Lab: 2 Hour(s) per week x 14 weeks
- Type: optional
- Semester: Spring
- Exam form: During the semester (summer session)
- Subject examined: Interactive theorem proving
- Courses: 2 Hour(s) per week x 14 weeks
- Exercises: 1 Hour(s) per week x 14 weeks
- Lab: 2 Hour(s) per week x 14 weeks
- Type: optional
- Semester: Spring
- Exam form: During the semester (summer session)
- Subject examined: Interactive theorem proving
- Courses: 2 Hour(s) per week x 14 weeks
- Exercises: 1 Hour(s) per week x 14 weeks
- Lab: 2 Hour(s) per week x 14 weeks
- Type: optional