Following is the list of topics that we intend to cover in the course. The emphasis of the course is on effective use of verification tools. We hope that at the end of the course, students will be able to do research in this area.
- Overview of Interactive Theorem Proving
- Proof Assistant Coq
- Input language - arithmetic, lists, inductive types, recursion, etc.
- Manual proofs
- Using tactics
- Proving properties of programs
- Yves Bertot and Pierre Casteran. Interactive Theorem Proving and Program Development, Coq’Art: The Calculus of Inductive Constructions