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