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
|
|