Interactive Theorem Proving Project
CS-642 / 4 crédits
Enseignant: Pit-Claudel Clément
Langue: Anglais
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
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