Scribing: 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. You must submit your scribe notes 2 days after the lecture. Whenever nobody volunteers to scribe the following lecture, we will run a simple script to randomly choose the scribes.
Note: the grey entries in the table represent a tentative schedule and are subjected to change.
Lecture | Date | Topic | Notes | Scribes |
01 |
Aug 29 | Course overview | lec01.pdf | |
Basics of Programming Language Semantics | ||||
02 | Sep 1 | The IMP Language | lec02.ps | Munson, Arbree |
03 | Sep 3 | Large Step Operational Sematics I | lec03.ps | Munson, Williams |
04 | Sep 5 | Large-Step Operational Semantics II | lec04.ps | Dmitriev, Finley |
05 | Sep 8 | Small Step Operational Semantics | lec05.ps | Dmitriev, Martin |
06 | Sep 10 | Proofs by Induction | lec06.ps | Wang, Qi |
07 | Sep 12 | Induction and Inductive Definitions | lec07.ps | Finley, Martin |
08 | Sep 15 | Denotational Semantics | lec08.ps | Shaparenko |
09 | Sep 17 | Denotational Semantics of While Loops | lec09.ps | Shaparenko |
10 | Sep 19 | Complete Partial Orders | lec10.ps | Wang, Qi |
11 | Sep 22 | The Fixed Point Theorem | lec11.ps | Hong, Tan |
12 | Sep 24 | Domain Constructions I | lec12.ps | Hong, Tan |
13 | Sep 26 | Domain Constructions II | lec13.ps | Martin |
14 | Sep 29 | Axiomatic Semantics | lec14.ps | McKeen, Moon |
15 | Oct 1 | Soundness of Hoare Logic | lec15.ps | Haridasan, Elhawary |
16 | Oct 3 | Relative Completeness of Hoare Logic | lec16.ps | Haridasan, Elhawary |
17 | Oct 6 | Kleene Algebras Invited lecturer: Dexter Kozen |
lec17.ps | Munson |
Language Features and Semantics |
||||
18 | Oct 8 | Introduction to REC | lec18.ps | Finley |
19 | Oct 10 | Call-by-Name Semantics of REC | lec19.ps | Dmitriev |
Oct13 |
Fall Break |
|||
20 | Oct 15 | The Untyped Lambda Calculus | lec20.ps | Moczydlowski, Hasan |
21 | Oct 17 | Expressiveness of Lambda Calculus | lec21.ps | Moczydlowski |
22 | Oct 20 | Fixed Point Combinators | lec22.ps | Arbree, Moczydlowski |
23 | Oct 22 | Substitution and Term Equivalence | lec23.ps | Elhawary |
24 | Oct 24 | Introduction to FUN | lec24.ps | Arbree |
Oct 27 |
Prelim Review |
|||
Oct 28 |
Preliminary Exam: 7:30-9:30PM , UP 211 |
|||
Oct 29 |
No Class (post-exam) |
|||
25 | Oct 31 | Error Handling | lec25.ps | Tan |
26 | Nov 3 | Static and Dynamic Scoping | lec26.ps | Wang |
27 | Nov 5 | Dynamic Allocation | lec27.ps | Hong |
28 | Nov 7 | Translational Semantics | lec28.ps | Haridasan |
29 | Nov 10 | CPS Semantics | lec29.ps | Guron |
30 | Nov 12 | Continuations Continued | lec30.ps | McKeen, Moon |
Static and Abstract Semantics | ||||
31 | Nov 14 | The Simply Typed Lambda Calculus | lec31.ps | Hasan, Guron |
32 | Nov 17 | Progress + Preservation =>
Soundness |
lec32.ps | Hasan |
33 |
Nov 19 | Product and Sum Types | lec33.ps | Qi |
34 | Nov 21 | Recursive Types | lec34.ps | Williams, Guron |
35 | Nov 24 | Subtyping and Coercions | lec35.ps | McKeen |
36 | Nov 26 | The Curry-Howard Isomorphism | lec36.ps | Moon |
Nov 28 |
Thanksgiving Break |
|||
37 | Dec 1 | Abstract Interpretation | lec37.ps | Williams |
38 | Dec 3 | Correctness of Abstract Interpretation | ||
39 | Dec 5 | Case Study: Shape Analysis | ||
Dec 15 | Final Exam: 12:00-2:30PM , PH 213 |