CS 499: Mechanized Reasoning about Programs

General Information




Week Date Reading Lecture 1 Lecture 2 Assignment
1 08/29SF Preface+Basics (2 fst sec.) Introduction Functional Programming in Coq Lec2: HW1 out (Coq)
2 09/05SWA Chapter 1 + SF Basics Labor Day Simple Proofs & Proofs by Induction Lec2: HW1 due
3 09/12SWA Chapter 2 (2.1) + SF Proofs by induction, Lists Operational Semantics: Natural Semantics Data Structures Lec1: HW2 out
4 09/19SWA Chapter 2 (2.2) + SF Poly Structural Operational Semantics Polymorphism and Higher-Order Functions Lec1: HW2 due
5 09/26SF "Tactics: More Basic Tactics" Semantics Functions and their Properties (in Coq)Semantics Functions and their Properties (in Coq) Lec2: HW3 out
6 10/03SF "Logic" Special assignment SOS as a Function in Coq Lec2: HW3 due
7 10/10SF 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/31SWA Chapter 3 Extensions to Operational Semantics Extensions of Operational Semantics in Coq Lec2: PA1 due, PA2 out
11 11/07SWA Chapter 9.1 Application of Operational Semantics Application of Operational Semantics in Coq
12 11/14SWA Chapter 9.2 Axiomatic Semantics: Partial Correctness Application of Operational Semantics in Coq(2) Lec2: PA2 due, PA3 out
13 11/21SWA 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