Progress Report |
Due Date |
Midterm Check-in |
March, 17 |
Final Check-in |
April, 30 |
Reading
Exercises
- Get Coq up and running on your system
- Download Software Foundations source files
- Create your git repository for solutions and proofs
Reading
- Functional Programming in Coq: Basics.v
Topics
- Basic types, enumerations, numbers, booleans
- Functions and recursion
- Unit tests
Exercises
- Standard: All 1 and 2 star
Reading
- Proof by Induction: Induction.v
Topics
- Inductive proof tactics, structured proofs
- Local assertions
- Formal vs informal proofs
Exercises
- Standard: All 2 star
- Advanced: All 3 star
- Challenge: bin_nat_bin