| Week | Date | Reading | Lecture 1 | Lecture 2 | Assignment |
|---|---|---|---|---|---|
| 1 | 08/29 | SF Preface+Basics (2 fst sec.) | Introduction | Functional Programming in Coq | Lec2: HW1 out (Coq) |
| 2 | 09/05 | SWA Chapter 1 + SF Basics | Labor Day | Simple Proofs & Proofs by Induction | Lec2: HW1 due |
| 3 | 09/12 | SWA Chapter 2 (2.1) + SF Proofs by induction, Lists | Operational Semantics: Natural Semantics | Data Structures | Lec1: HW2 out |
| 4 | 09/19 | SWA Chapter 2 (2.2) + SF Poly | Structural Operational Semantics | Polymorphism and Higher-Order Functions | Lec1: HW2 due |
| 5 | 09/26 | SF "Tactics: More Basic Tactics" | Semantics Functions and their Properties (in Coq) | Semantics Functions and their Properties (in Coq) | Lec2: HW3 out |
| 6 | 10/03 | SF "Logic" | Special assignment | SOS as a Function in Coq | Lec2: HW3 due |
| 7 | 10/10 | SF IndProp | Inductive Predicates | Quizz, Inductive Predicates | PA1 out |
| 8 | 10/17 | Operational Semantics in Coq | Operational Semantics in Coq | ||
| 9 | 10/24 | Midterm Exam | Operational Semantics in Coq | ||
| 10 | 10/31 | SWA Chapter 3 | Extensions to Operational Semantics | Extensions of Operational Semantics in Coq | Lec2: PA1 due, PA2 out |
| 11 | 11/07 | SWA Chapter 9.1 | Application of Operational Semantics | Application of Operational Semantics in Coq | |
| 12 | 11/14 | SWA Chapter 9.2 | Axiomatic Semantics: Partial Correctness | Application of Operational Semantics in Coq(2) | Lec2: PA2 due, PA3 out |
| 13 | 11/21 | SWA Chapter 10 (10.1) | Axiomatic Semantics: Total Correctness | Application of Operational Semantics in Coq(3) | |
| 14 | 11/28 | Quizz; Axiomatic Semantics: Applications | Axiomatic Semantics in Coq | Lec2: PA3 due, PA4 out | |
| 15 | 12/05 | Final Exam Review (1) | Final Exam Review (2) & Research in MRAP @ SICCS | Lec2: PA4 due |
See BBLearn