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
Dans les plans d'études
- Forme de l'examen: Multiple (session libre)
- Matière examinée: Interactive Theorem Proving Project
- Cours: 2 Heure(s)
- Projet: 70 Heure(s)
- TP: 40 Heure(s)
- Type: optionnel