3 Schedule
Class |
| Files |
| Notes |
Jan 31, Feb 5 |
|
| An Introduction to the Coq proof assistant | |
Feb 7 |
|
| Common Coq Datatypes and Recursion | |
Feb 12 |
|
| Recursive and Inductive Proofs | |
Feb 14 |
|
| Reasoning about lists and other datatypes | |
Feb 19 |
|
| Polymorphism | |
Feb 21 |
|
| Useful Coq tactics | |
Feb 26 |
|
| More Logic, Proofs in Programs | |
Feb 28 |
|
| Inductive Propositions and Reflection | |
Mar 5 |
|
| Embedding Programs in Coq | |
Mar 7 |
|
| More Imp, Automation | |
Mar 12,14 |
|
| Program Equivalence | |
Mar 26 |
| Midterm [pdf] |
| |
Mar 28, Apr 2 |
|
| Hoare Logic | |
April 2 |
| Project Proposals Due |
| Submit via ELMS |
April 4 |
|
| Hoare Logic in Practice | |
April 9 |
|
| Small step program semantics | |
April 11 |
|
| Types, Progress and Preservation | |
April 16 |
|
| Simply Typed Lambda Calculus | |
April 18 |
|
| STLC continued | |
April 23 |
|
| Real and Complex arithmetic | |
April 25 |
|
| Matrices, Relations and Morphisms | |
April 30 |
|
| Quantum Computing | |
May 2 |
|
| A Small Quantum IMP | |
May 7 |
|
| QuickChick 1: Typeclasses | |
May 9 |
|
| QuickChick 2: Random Testing | |
May 14 |
|
| Student Presentations | |
May 14 |
|
| Recap and Resources |
Before every class, the Coq (.v) and HTML versions of the lecture materials will be available above. Students are encouraged to follow along inside, ideally within ProofGeneral. After every class, the files will be updated with additional exposition and exercises. Those are due before class on the following Tuesday; please submit via ELMS.