Course Syllabus

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

Textbooks

• Yves Bertot and Pierre Casteran. Interactive Theorem Proving and Program Development, Coq’Art: The Calculus of Inductive Constructions

Others

• (e-book) Yves Bertot. Coq in a Hurry
• Benjamin C. Pierce et al. Software Foundations