Lecture | Date | Topic | Reading |
1 | Jan 22 | Introduction to semantics [txt] | |
2 | Jan 24 | Operational semantics [txt] | |
3 | Jan 26 | Inductive definitions [txt] | W 3.1,3.2 |
4 | Jan 29 | IMP: a simple imperative language [txt] (Lecturer: Siggi Cherem) | W 2.1 |
5 | Jan 31 | Large-step operational semantics [txt] (Lecturer: Siggi Cherem) | W 2.2-2.5 |
6 | Feb 1 | Runtime errors and non-termination | |
7 | Feb 5 | Intro to denotational semantics [txt] (Lecturer: Siggi Cherem) | M 4.3.3 W 5.2 |
8 | Feb 7 | Fixed-point semantics of loops | |
9 | Feb 9 | Partial and total correctness [txt] | W 6.1-6.3 |
10 | Feb 12 | Hoare logic [txt] | W 6.4,6.5 |
11 | Feb 14 | Program correctness proofs [txt] | W 6.6 |
12 | Feb 16 | Weakest preconditions, verification conditions | W 7.2,7.4 |
13 | Feb 19 | Program specifications in Eiffel and JML [eiffel, jml] | |
14 | Feb 21 | Static program verification using ESCJava [escjava, example] | |
15 | Feb 23 | Program analysis via abstract interpretation [txt] | |
16 | Feb 26 | Analysis of control constructs [txt] | |
17 | Feb 28 | Verifying temporal safety properties | |
18 | Mar 2 | Intro to the lambda calculus (Lecturer: Siggi Cherem) | M 4.2 |
19 | Mar 5 | Call-by-name, call-by-value, lazy evaluation | |
20 | Mar 7 | ML0: a simple functional language | |
21 | Mar 9 | Evaluation order, lazy evaluation | |
Mar 12 | Preliminary Examination | ||
22 | Mar 14 | Types in the lambda calculus | |
23 | Mar 16 | Type checking | M 6.2 |
Spring Break | |||
24 | Mar 26 | Product and sum types [txt] | H 19.1-19.2 |
25 | Mar 28 | Type inference | M 6.3 |
26 | Mar 30 | Parametric polymorphism [txt] | H 20 M 6.4 |
27 | Apr 2 | Subtyping records and functions [txt] | H 26.2 |
28 | Apr 4 | Pointers and references | H 14 |
29 | Apr 6 | Call-by-reference, copy-in-copy-out parameters | |
30 | Apr 9 | Scoping, activation records, function closures | M 7 |
31 | Apr 11 | Unstructured control-flow and exceptions [txt] | H 11.1,13 M 8.1-8.2 |
32 | Apr 13 | Exceptions, continuations [txt] | H 12 M 8.3 |
33 | Apr 16 | Continuation-passing style | |
34 | Apr 18 | Object-oriented programming | M 10 H 27 |
35 | Apr 20 | Dynamic method lookup | M 10.2 |
36 | Apr 23 | Logic programming: Prolog | M 15 |
37 | Apr 25 | Unification, backtracking | M 15 |
38 | Apr 27 | More Prolog concepts | M 15 |
39 | Apr 30 | Concurrent programming concepts | |
40 | May 2 | Shared memory vs. message passing | |
41 | May 4 | Modules and data abstraction [txt] (Lecturer: Andrew Myers) |
Books abbreviations: M = Mitchell, W - Winskel, H - Harper.