Interactive Theorem Proving Project
Frequency
Every year
Summary
A project-focused introduction to interactive theorem proving.
Content
Sample topics:
- Intro to the interactive theorem proving (Rocq, 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, in-class quizzes, formal verification project
Learning objectives: Plan and carry out mechanized proofs
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