Lecture Notes

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.