| Mon 3/31/25 |
Course overview and basics of Coq |
Course overview; Preface; Basics |
| Wed 4/2/25 |
Induction and datastructures |
Induction; Lists |
| Fri 4/4/25 |
continued |
|
| Mon 4/7/25 |
continued |
|
| Wed 4/9/25 |
No class; Prof. Arden out of town |
video links coming soon |
| Fri 4/11/25 |
No class; Prof. Arden out of town |
video links coming soon |
| Mon 4/14/25 |
Polymorphism, functions as data |
Poly |
| Wed 4/16/25 |
continued |
|
| Fri 4/18/25 |
More Tactics |
Tactics |
| Mon 4/21/25 |
Logic in Coq |
Logic |
| Wed 4/23/25 |
continued |
|
| Fri 4/25/25 |
continued |
|
| Mon 4/28/25 |
Inductively defined propositions |
IndProd; ProofObjects |
| Wed 4/30/25 |
continued |
|
| Fri 5/2/25 |
Total and partial maps; IMP |
Maps; Imp; ImpParser; ImpCEvalFun |
| Mon 5/5/25 |
IMP: modeling an imperative language |
|
| Wed 5/7/25 |
Program equivalence |
Equiv |
| Fri 5/9/25 |
Hoare Logic |
Hoare; Hoare2 |
| Mon 5/12/25 |
|
|
| Wed 5/14/25 |
|
|
| Fri 5/16/25 |
|
|
| Mon 5/19/25 |
|
|
| Wed 5/21/25 |
|
|
| Fri 5/23/25 |
|
|
| Wed 5/28/25 |
|
|
| Fri 5/30/25 |
|
|
| Mon 6/2/25 |
|
|
| Wed 6/4/25 |
|
|
| Fri 6/6/25 |
|
|
| |
|
|
| |
|
|
| |
|
|
| |
|
|
| |
|
|
| |
|
|
| |
|
|