Interactive Theorem Proving Project
CS-642 / 4 credits
Teacher: Pit-Claudel Clément
Language: English
Remark: Doctoral-level alternative to CS-428 Interactive Theorem Proving
Frequency
Every year
Summary
A project-focused introduction to interactive theorem proving.
Content
- Intro to the Rocq 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)
Note
Assessments:
Take-home assignments: 40% of final grade Formal verification project: 60% of the final grade
By the end of the course, the student must be able to:
Plan and carry out mechanized proofs in Rocq
Learning Prerequisites
Recommended courses
CS320, CS550
In the programs
- Exam form: Multiple (session free)
- Subject examined: Interactive Theorem Proving Project
- Courses: 2 Hour(s)
- Project: 70 Hour(s)
- TP: 40 Hour(s)
- Type: optional