Princeton University
|
Computer Science 441
|
|
Here is an approximate schedule for COS 441. This schedule is only approximate and may be changed at any time.
| Day | Topics | Reading | Notes/Assignments |
| M Sep 19 | Intro; Deductive Systems | Pierce Chap 2 (especially 2.4) Pierce Chap 3.1-3.3 |
Lecture1; Aquinas' example proof |
| W 21 | Intuitionistic Logic | Optional: Wadler's article on Proofs and Programs | |
| M 26 | ML intro | Online resourses for SML are
here.
I particularly recommend
Robert Harper's
"Programming in Standard ML" and Peter Lee's short notes on
Using the SML/NJ
System. Check out the
ML Basis
documentation as well. Frances' notes on installing sml and emacs mode Frances' lecture notes and some related slides |
Assignment #1: Deductive Systems (Due: M Oct 3) |
| W 28 | ML intro | ||
| M Oct 3 | Untyped Lambda Calculus | Pierce Chap 5; slides | Assignment #2: ML & Proof Checking (Due: M Oct 10) |
| W 5 | MinML: Syntax and Operational Semantics | MinML OS slides | |
| M 10 | MinML: Properties of Operational Semantics | Assignment #3: Untyped Lambda Calculus (Due: M Oct 17) | |
| W 12 | MinML Typing; Curry-Howard Isomorphism | Pierce Chap 8.1, 8.2, 9.1, 9.2, 9.4 | |
| M 17 | Type Safety | Pierce Chap 8.3, 9.3 | Assignment #4: Typed Lambda Calculus (Due: W Oct 26) |
| W 19 | Product types + begin sums | Pierce Chap 11 | |
| M 24 | Sum types | Pierce Chap 11 | |
| W 26 | Recursive types | Pierce Chap 20.1, 20.2 | |
| Fall Break | |||
| M Nov 7 | Denotational Semantics | Mitchell Handout (Chap 4.4) | Take-home midterm goes online Sunday Night Nov 6 (Complete by W Midnight, Nov 9) |
| W 9 | Semantics of Pictures | ||
| M 14 | Effectful Computations: References | Pierce Chap 13 | |
| W 16 | Effectful Computations: Exceptions, Continuations & Evaluation Contexts | Pierce Chap 14; Evaluation Contexts Note | Assignment #5: Denotational Semantics(Due: M Nov 28) |
| M 21 | Quantified Types: PolyMinML/System F | Pierce Chap 23 | |
| W 23 | Quantified Types: Existential Types & Data Abstraction | Pierce Chap 24 | |
| M 28 | Quantified Types: Type Inference | Pierce Chap 22.1 - 22.5 | |
| W 30 | Quantified Types: Type Inference | Assignment #6: Effectful computations, data abstraction (Due: W Dec 7) | |
| M Dec 5 | Declarative Subtyping | Pierce Chap 15.1-15.5 | |
| W 7 | Algorithmic Subtyping | Pierce Chap 16.1-16.3 | Assignment #7:
Type Inference and Subtyping (Due
F Dec 16) You will need the code supplied here. Note: You may hand in your assignment sooner (eg: on Wednesday or even Monday!) |
| M 12 | Featherweight Java | Pierce Chap 19 | |
| W 14 | |||
| Jan 18-19 | Final Exam | you will have 24 hours to do the Final, just like the midterm | Jan 18-19 |
Midterm Exam Topics
The midterm may cover any material from class lectures, from assignments, or from chapters of the course textbook mentioned below.
Final Exam Topics
the final exam may cover any material from class lectures, from assignments, or from chapters of the course textbook mentioned either under midterm topics above or below.