| Lecture | Date | Topic | Reading |
| 1 | Aug 30 | Introduction to semantics [txt | pdf] | |
| 2 | Sep 1 | Small-step operational semantics [txt | pdf] | |
| 3 | Sep 3 | Inductive proofs, intro to large-step semantics [txt | pdf] | H 1.1-1.5 W 3.1,3.2 |
| 4 | Sep 6 | IMP, a simple imperative language [txt | pdf] | W 2.1 |
| 5 | Sep 8 | Large-step operational model of IMP [txt | pdf] | W 2.2-2.5 |
| 6 | Sep 10 | Command equivalences [txt | pdf] | W 3.4 |
| 7 | Sep 13 | Execution errors and non-termination | |
| 8 | Sep 15 | Intro to denotational semantics [txt] | M 4.3.3 W 5.2 |
| 9 | Sep 17 | Fixed-point semantics of while loops | |
| 10 | Sep 20 | Intro to axiomatic semantics [txt] | W 6.1-6.3 |
| 11 | Sep 22 | Hoare logic and program correctness proofs [txt] | S 3.6 W 6.4,6.6 |
| 12 | Sep 24 | Weakest pre-conditions [txt] | |
| 13 | Sep 27 | Verification conditions and applications | |
| 14 | Sep 29 | Program analysis using abstract interpretation [txt] | |
| 15 | Oct 1 | Analysis of control-flow constructs [txt] | |
| 16 | Oct 4 | Correctness of program analyses | |
| 17 | Oct 6 | Verifying temporal safety properties of programs | |
| 18 | Oct 8 | Intro to lambda calculus | S 14.1,14.2 M 4.2 |
| 19 | Oct 11 | Lambda calculus encodings | |
| 20 | Oct 13 | Evaluation order: call-by-name and call-by-value | |
| 21 | Oct 15 | Laziness and call-by-need | |
| Oct 20 | Preliminary examination | ||
| 24 | Oct 25 | Types in lambda calculus | S 14.5 |
| 25 | Oct 27 | Product and sum types [txt] | H 19.1-19.2 |
| 26 | Nov 1 | Type checking | M 6.2 |
| 27 | Nov 3 | Type inference | M 6.3 |
| 28 | Nov 5 | Parametric polymorphism [txt] | S 14.6 H 20 M 6.4 |
| 29 | Nov 8 | Records and subtyping [txt] | H 26.2 |
| 30 | Nov 10 | Pointers and references | H 14 |
| 31 | Nov 12 | Call-by-reference and call-by-value-result | S 5.2 |
| 32 | Nov 15 | Scopes and storage management | S 5.3-5.7 M 7 |
| 33 | Nov 17 | Control-flow and exceptions [txt] | H 11.1,13 M 8.1-8.2 |
| 34 | Nov 19 | Exceptions and continuations [txt] | H 12 M 8.3 |
| 35 | Nov 22 | Continuations (ctd) | |
| 36 | Nov 24 | Object-oriented programming concepts | S 7 M 10 H 27 |
| 36 | Nov 29 | Modules and data abstraction [txt] | S 6.1-6.4 M 9 |
| 37 | Dec 1 | Intro to logic programming | |
| 38 | Dec 3 | Concurrent programming |
Books abbreviations: S - Sethi, M = Mitchell, W - Winskel, H - Harper.