Lecture
Lecture
- Wed, Sep 26 - Lecture 1 : Administrivia, motivation, Coq crash course
- Mon, Oct 1 - Lecture 2 : Syntax, More Coq (FRAP Chapters 1, 2)
- Wed, Oct 3 - No Lecture
- Mon, Oct 8 - Lecture 3 : Trusting Trust, ADTs (FRAP Chapter 3)
- Wed, Oct 10 - Lecture 4 : ADTs Continued (FRAP Chapter 3)
- Mon, Oct 15 - Lecture 5 : Semantics via Interpreters (FRAP Chapter 4)
- Wed, Oct 17 - Lecture 6 : Semantics via Interpreters Continued (FRAP Chapter 4)
- Mon, Oct 22 - Lecture 7 : Euler & Nelson; Invariants and Model Checking (FRAP Chapters 5,6)
- Wed, Oct 24 - Lecture 8 : Invariants and Model Checking Continued (FRAP Chapters 5,6)
- Mon, Oct 29 - Lecture 9: Operational Semantics (FRAP Chapter 7)
- Wed, Oct 31 - Lecture 10: Operational Semantics Continued (FRAP Chapter 7)
- Mon, Nov 5 - Lecture 11: Compiler Correctness (FRAP Chapter 9)
- Wed, Nov 7 - Lecture 12: Compiler Correctness Continued (FRAP Chapter 9)
- Mon, Nov 12 - No Lecture
- Wed, Nov 14 - Lecture 13: Simply Typed Lambda Calculus (FRAP Chapter 10)
- Mon, Nov 19 - Lecture 14: Simply Typed Lambda Calculus Continued (FRAP Chapter 10)
- Wed, Nov 21 - Lecture 15: Church Encodings
- Mon, Nov 25 - Lecture 16: Hoare Logic (FRAP Chapter 12)
- Wed, Nov 28 - Lecture 17: Hoare Logic Continued (FRAP Chapter 12)