Exercises

1. A Brief Presentation of Coq
2. Types and Expressions
3. Propositions and Proofs
4. Dependent Products
5. Everyday logic
6. Inductive Data Structures
7. Tactics and automation
8. Inductive Predicates
9. Functions and their specification
10. Extraction and imperative programming
11. A Case Study : binary search trees
12. The Module System
13. Infinite Objects and Proofs
14. Foundations of Inductive Types
15. General Recursion
16. Proof by reflection