| Tue 1/6/26 |
Course overview and basics of Coq |
Course overview; Preface; Basics |
| Thu 1/8/26 |
Induction and datastructures |
Induction |
| Tue 1/13/26 |
continued |
Lists |
| Thu 1/15/26 |
continued |
|
| Tue 1/20/26 |
|
|
| Thu 1/22/26 |
|
|
| Tue 1/27/26 |
Polymorphism, functions as data |
Poly |
| Thu 1/29/26 |
continued |
|
| Tue 2/3/26 |
More Tactics |
Tactics |
| Thu 2/5/26 |
Logic in Coq |
Logic |
| Tue 2/10/26 |
continued |
|
| Thu 2/12/26 |
continued |
|
| Tue 2/17/26 |
Inductively defined propositions |
IndProd; ProofObjects |
| Thu 2/19/26 |
continued |
|
| Tue 2/24/26 |
Total and partial maps; IMP |
Maps; Imp; ImpParser; ImpCEvalFun |
| Thu 2/26/26 |
IMP: modeling an imperative language |
|
| Tue 3/3/26 |
Program equivalence |
Equiv |
| Thu 3/5/26 |
Hoare Logic |
Hoare; Hoare2 |
| Tue 3/10/26 |
|
|
| Thu 3/12/26 |
|
|
| |
|
|
| |
|
|
| |
|
|
| |
|
|
| |
|
|
| |
|
|
| |
|
|
| |
|
|
| |
|
|
| |
|
|
| |
|
|
| |
|
|
| |
|
|
| |
|
|
| |
|
|
| |
|
|