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