| layout | title | permalink |
|---|---|---|
page |
Schedule |
/schedule/ |
| Week | Dates | Topics | Reading |
|---|---|---|---|
| 1 | 08/23 - 8/27 | Introduction, Coq Basics, Functional Programming, Induction & Inductive Data Structures | Intro Slides |
| 2 | 8/30 - 9/3 | Polymorphism, Higher-Order Functions, Coq Tactics | |
| 3 | 9/8 & 9/10 | Logic in Coq, Inductive Propositions | |
| 4 | 9/13 - 9/17 | Inductive Propositions (Contd.), Curry-Howard Correspondence, Maps | |
| 5 | 9/20 - 9/24 | Modeling an Imperative Language (Imp), Operational Semantics | |
| 6 | 9/27 - 10/1 | Basic Proof Automation, Reasoning about Imp using Hoare Logic | |
| 7 | 10/4 - 10/8 | Type Systems, Simply Typed Lambda Calculus (STLC) | |
| 8 | 10/11 - 10/15 | STLC (Contd.) | |
| 9 | 10/18 - 10/22 | Properties of STLC, Extensions to STLC | |
| 10 | 10/25 - 10/29 | Extensions to STLC (Contd.), Sub-Typing | |
| 11 | 11/1 - 11/5 | More Proof Automation, Functional Program Verification | |
| 12 | 11/8 - 11/12 | Functional Program Verification (Contd.) | |
| 13 | 11/15 - 11/19 | Research Topics |