The following schedule lists the topics we will cover and approximately the number of meetings we will spend on each topic. The schedule is tentative. Most likely, some things will change during the semester, and I will revise the schedule as necessary.
The Reading column lists the assigned reading for the meeting. You should view the readings as an introduction to spark discussion in class.
The Assignment column lists the due date for each assignment.
| Date | Topic | Reading | Assignment | ||
|---|---|---|---|---|---|
| 1 | Tue | 1/16 | Welcome and course overview. Inductive definitions. Get signed-up on Moodle. Post a note on Piazza to introduce yourself. |
||
| Thu | 1/18 | Judgments and rules meeting02 |
Harper Ch. 1-2 | ||
| 2 | Tue | 1/23 | Judgments and rules meeting03 |
||
| Thu | 1/25 | Judgments and rules meeting04 |
Harper Ch. 3 | HW0 due Fri | |
| 3 | Tue | 1/30 | Statics and dynamics meeting05 |
Harper Ch. 4-5 | |
| Thu | 2/1 | Statics and dynamics meeting06 |
|||
| 4 | Tue | 2/6 | Type safety meeting07 |
Harper Ch. 6-7 | |
| Thu | 2/8 | Type safety meeting08 |
HW1 due Fri | ||
| 5 | Tue | 2/13 | Imperative computation meeting09 |
Winskel Ch. 2; Harper Ch. 34 | |
| Thu | 2/15 | Language implementation in OCaml meeting10 |
OCaml | ||
| 6 | Tue | 2/20 | Functions and System T meeting11 |
Harper Ch. 8-9 | |
| Thu | 2/22 | Finite data types meeting12 |
Harper Ch. 10-11 | HW2 due Fri | |
| 7 | Tue | 2/27 | Denotational semantics meeting13 |
Winskel Ch. 5 | |
| Thu | 3/1 | Denotational semantics meeting14 |
Recommended: Winskel Ch. 8 (read for the general concepts, not the details). Supplemental: Schmidt. Denotational Semantics. Classic: Scott and Strachey. Towards a Mathematical Semantics for Computer Languages. Supplemental: For an alternative presentation of partial orders, least upper bounds, monotonic and continuous functions, and least fixed points, take a look at this report. (up to and including Section 2.4) |
||
| 8 | Tue | 3/6 | Recursive types (System FPC) meeting15 |
Harper Ch. 19-20 | |
| Thu | 3/8 | Parametric polymorphism (System F) meeting16 |
Harper Ch. 16 | HW3 due Fri | |
| 9 | Tue | 3/13 | Catch-up questions meeting17 |
Winskel Ch. 6 Recommended: C.A.R. Hoare. An Axiomatic Basis for Computer Programming. CACM 12(10), October 1969. Recommended: Robert W. Floyd. Assigning Meanings to Programs. |
|
| Thu | 3/15 | Catch-up questions meeting18 |
Winskel Ch. 7 | ||
| 10 | Tue | 3/20 | Axiomatic semantics meeting19 |
Harper Ch. 28 | |
| Thu | 3/22 | Control flow: Exceptions and continuations meeting20 |
Harper Ch. 29-30 | Proposal due Fri | |
| 11 | Tue | 3/27 | No class: spring break | ||
| Thu | 3/29 | No class: spring break | |||
| 12 | Tue | 4/3 | Control flow: Exceptions and continuations | ||
| Thu | 4/5 | Control flow: Exceptions and continuations | HW4 due Fri | ||
| 13 | Tue | 4/10 | Continuations, VC, AI (Abstract Interpretation) | ||
| Thu | 4/12 | Continuations, VC, AI | Status Update due Fri | ||
| 14 | Tue | 4/17 | Review | ||
| Thu | 4/19 | Review | |||
| 15 | Tue | 4/24 | Final exam review | ||
| Thu | 4/26 | Final exam: evening (time 7:30-10pm) | |||
| 16 | Tue | 5/1 | Final project presentations | ||
| Thu | 5/3 | Final project presentations | Presentation Peer Eval due Fri | ||
| 17 | Tue | 5/8 | Finals week | Paper due Sun, Paper Peer Eval Extra Credit due Mon |