Module Topics Reading
1 Introduction, Coq Basics, Functional Programming, Induction & Inductive Data Structures Intro Slides (PDF)
Lec 2 Zoom Recording
Lec2 Reading
Lec3 Zoom Recording
Lec3 Reading
Lec4 Zoom Recording
Lec4 Reading
Lec5 Zoom Recording
Lec5 Reading
Lec6 Recording (from archive)
2 Polymorphism, Higher-Order Functions, Maps, Coq Tactics Lec7 Zoom Recording
Lec8 Zoom Recording
Lec7 & Lec8 Reading
Lec 9 Recording (from archive)
Lec 9 Reading
Lec 10 Zoom Recording
Lec 10 Reading
3 Logic in Coq, Inductive Propositions, Curry-Howard Correspondence Course Project Proposals
Lec 11 Zoom Recording
Lec 11 Reading
Lec 12 Zoom Recording
Lec 12 Reading
Lec 13 Zoom Recording
Lec 13 Reading
4 Modeling an Imperative Language (Imp), Operational Semantics Lec 14 Zoom Recoding
Lec 15 Zoom Recording
Lec 16 Zoom Recording
Lec 14-16 Reading
5 Reasoning about Imp using Hoare Logic Lec 17 Zoom Recording
Lec 18 Zoom Recording
Lec 19 Zoom Recording
Lec 17-19 Reading
6 Type Systems, Simply Typed Lambda Calculus (STLC)
7 Properties of STLC, Extensions to STLC
8 Proof Automation, Functional Program Verification
9 Research Topics