Lecture: Verifiction with the Coq Proof Assistant
After completing the module, students will be able to
- understand the basic concepts of formal proofs, verification, and interactive theorem proving, and the role of proof assistants like Coq in this process.
- use the Coq language to express formal models and their properties.
- construct formal proofs, including reasoning about inductive and recursive definitions and usage of tactics and automation to simplify proofs.
- verify the correctness of computer programs using Coq by reasoning about program semantics.