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.