Schedule
This is a list of topics (primarily textbook chapters) that will be covered in this course. Most bullet points below represent a single class, although some chapters are longer or the topics more complex and so might require two classes (as marked). While we will try to keep the pace listed, we will adjust as needed. Once topics have been covered, this fact will be documented by adding the date of in-class discussion in red next to the topic. This follows the "blue arrow path" through the Roadmap from the textbook.
- Class overview, big picture / motivation [Completed Aug 23]
- Quick tour of Coq [Completed Aug 25]
- Certified Software (access from UNCG computers or with an ACM account) [Completed Aug 25]
- Preface [Completed Aug 30]
- Basics [Completed Sept 1]
- Induction: Proof by Induction [Completed Sept 6]
- Lists: Working with Structured Data [Completed Sept 15]
- Poly: Polymorphism and Higher-Order Functions [Completed Sept 22]
- Tactics: More Basic Tactics [Completed Sept 29]
- Logic: Logic in Coq [Completed Oct 13]
- IndProp: Inductively Defined Propositions [Completed Nov 3]
- Maps: Total and Partial Maps [Independent study]
- Imp: Simple Imperative Programs [Completed Nov 15]
- Equiv: Program Equivalence [Completed Nov 22]
- Hoare: Hoare Logic, Part I [To be completed Dec 1]