Proofs and reliable programming using Coq 2020
This is a course in 7 modules of 3 hours each, with the following tentative plan Programming with simple types and recursive data-types Logical formulas and the proposition-as-type correspondence in practice Tactic-based theorem proving Reasoning by induction on programs Advanced proof-by-induction guidelines More data-types (binary trees, binary numbers) Dependent types…
