Scribing: Due to the lack of scribing volunteers
for the remaining lectures, we have randomly scheduled the remaining entries
using a simple perl script. Further changes in the
schedule are possible if all of the persons involved in the change agree. After assigning each
student two lectures to scribe, there are still a few empty entries left for the
last lectures. If you want to sign up for scribing one of the last lectures, send
an email at cs611@cs.cornell.edu,
indicating your full name(s) and the date of the lecture you want to scribe. Use
the provided LaTeX scribing template to
typeset your scribed notes and then send your final document to cs611@cs.cornell.edu.
Note: the grey entries in the table represent a tentative schedule and are subjected to change.
Lecture | Date | Topic | Notes | Scribes |
01 | Aug 30 | Course overview | lec01.ps | |
02 | Sep 2 | Introduction to IMP | lec02.ps | Alexander, Goel |
Basics of Programming Language Semantics | ||||
03 | Sep 4 | Large-step operational semantics | lec03.ps | Kim, Alexander |
04 | Sep 6 | Large-step semantics (ctd.) | lec04.ps | Kim, Goel |
05 | Sep 9 | Small-step operational semantics | lec05.ps | Irawan, Kulkarni |
06 | Sep 11 | Inductive proofs | lec06.ps | Cherem, Kurland |
07 | Sep 13 | Inductive definitions | lec07.ps | Irawan, Kulkarni |
08 | Sep 16 | Denotational semantics of IMP | lec08.ps | Milanovici, Barrera |
09 | Sep 18 | Denotational semantics of While loops | lec09.ps | Spalding, Fleming |
10 | Sep 20 | Complete partial orders | lec10.ps | Machanavajjhala, Vishnumurthy |
11 | Sep 23 | Domain constructions | lec11.ps | Spalding, Fleming |
12 | Sep 25 | More domain constructions | lec12.ps | Barrera, Diaz |
13 | Sep 27 | Introduction to axiomatic semantics | lec13.ps | Zhang,Lan |
14 | Sep 30 | Soundness of Hoare Logic | lec14.ps | Zhang, Lan |
15 | Oct 2 | Relative Completeness of Hoare Logic | lec15.ps | Svitkina, Hayrapetyan |
16 | Oct 4 | Verification conditions Invited lecturer: Dexter Kozen |
lec16.ps | Shieh, Srijuntongsiri |
17 | Oct 7 | Dynamic logic, Kleene algebras with tests Invited lecturer: Dexter Kozen |
lec17.ps | Roeder, Botev |
Language Features and Semantics |
||||
18 | Oct 9 | The applicative language REC | lec18.ps |
Dziobiak, Barth |
19 | Oct 11 | Denotational semantics of REC | lec19.ps | Roeder, Botev |
Oct14 |
Fall Break |
|||
20 | Oct 16 | Introduction to Lambda Calculus | lec20.ps | Stoyanov, Svitkina |
21 | Oct 18 | Expressiveness of Lambda Calculus | lec21.ps | Stoyanov, Vishnumurthy |
22 | Oct 21 | Recursion, substitution | lec22.ps (draft) | Hackett, Machanavajjhala |
23 | Oct 23 | Eta reduction and evaluation orders | lec23.ps (draft) | Cherem, Kurland |
24 | Oct 25 | The functional language F | lec24.ps | Aboul-Hosn, Ramanarayanan |
25 | Oct 28 | Error handling using denotational semantics | lec25.ps | Aboul-Hosn, Ramanarayanan |
Oct 30 |
Prelim Review |
|||
Oct 31 |
Preliminary Exam: PH 203, 7:30-9:00PM |
|||
Nov 1 |
No Class (post-exam) |
|||
26 | Nov 4 | Static and dynamic scoping | lec26.ps | Radlinski, Calandrino |
27 | Nov 6 | References, state, imperative features | lec27.ps | Srijuntongsiri, Hackett |
28 | Nov 8 | Translations and continuations | lec28.ps | Barth, Dziobiak |
29 | Nov 11 | Continuation Passing Style | lec29.ps | Viglietta, Allavena |
30 | Nov 13 | CPS semantics: non-local control | lec30.ps | Viglietta, Fidanboylu |
Static and Abstract Semantics | ||||
31 | Nov 15 | Simply typed Lambda Calculus | lec31.ps | Walsh, Shieh |
32 | Nov 18 | Safety = progress + preservation | lec32.ps | Hayrapetyan, Schultz |
33 | Nov 20 | Product and sum types | draft.ps | Schultz, Fidanboylu |
34 | Nov 22 | Recursive types | lec34.ps | Diaz, Walsh |
35 | Nov 25 | Subtyping and coercions | draft.ps | Radlinski, Allavena |
36 | Nov 27 | Polymorphism / Lattices | draft.ps | Vishnumurthy, Machanavajjhala |
Nov 29 |
Thanksgiving Break |
|||
37 | Dec 2 | Abstract interpretation | draft.ps | Svitkina, Lan, Dziobiak, Aboul-Hosn |
38 | Dec 4 | Widening operators | draft.ps | Fidanboylu, Kulkarni, Kurland, Irawan |
39 | Dec 6 | Correctness of abstract interpretation | draft.ps | Spalding, Fleming |
Dec 20 | Final Exam: PH 203, 9:00-11:30AM |