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. At any given time, notes more than a week in advance will not likely be relevant.
| Week | Topics | Reading | Notes/Assignments |
| 1 | Intro; Deductive Systems | Pierce Chap 2 (especially 2.4) Pierce Chap 3.1-3.3 |
Lecture1;
example proof Assignment #1: Deductive Systems (Due: Mon Sept. 24) |
| Intuitionistic Logic | Optional: Wadler's article on Proofs and Programs | ||
| 2 | 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. | Assignment #2: Intuitionistic Logic (Due: Mon Oct. 1) |
| ML intro; Introduce Untyped Lambda Calculus |
|||
| 3 | Untyped Lambda Calculus | Pierce Chap 5; slides | Assignment #3: Untyped Lambda Calculus (Extended!: Wed Oct. 17) |
| Untyped Translations | Class notes on translation theorem from booleans to lambda terms | ||
| 4 | Typed Lambda Calculus: Properties of Operational Semantics | ||
| Curry-Howard Isomorphism | Pierce Chap 8.1, 8.2, 9.1, 9.2, 9.4
|
||
| 5 | Type Safety | Pierce Chap 8.3, 9.3 Class notes on substitution lemma and preservation Class notes on progress |
Assignment #4: Typed Lambda Calculus (Due: Oct 22) |
| Data structures Exam Review |
Pierce Chap 11 Class notes on how to prove things |
||
| 6 | More data structures | Pierce Chap 11 Class notes on pairs, sums and lists |
|
| Recursive types | Pierce Chap 20.1, 20.2 | ||
| Week 6 | 5-hour Take-home Midterm between Oct 19-26 | all topics weeks 1-5 | |
| Fall Break | |||
| 7 | Exam recap | ||
| Recursive data structures Evaluation Contexts |
Pierce Chap 20.1, 20.2 Class notes on evaluation contexts |
||
| 8 | Exceptions | Class
notes on evaluation contexts and exceptions Pierce Chap 14 |
Assignment #5 Data structures and recursive types (Due Nov 19) |
| References | Pierce Chap 13 | ||
| 9 | Quantified Types: Universal Polymorphism | Pierce Chap 23 | Assignment #6 References (Due Dec 3rd) |
| Quantified Types: Existential Polymorphism | Pierce Chap 24 Class notes on existential types |
||
| 10 | Quantified Types: Type Inference | Pierce Chap 22.1 - 22.5 | |
| Quantified Types: Type
Inference Subtyping |
Type Inference II Slides Class notes on subtyping Pierce Chap 15.1-15.5 on Subtyping |
||
| 11 | More Subtyping | Class notes on subtyping (Monday,
Wednesday) Pierce Chap 15.1-15.5 on Subtyping |
Assignment #7 Type inference. You'll also need this code. (Due Dec 18th) |
| 12 | Featherweight Java Java Stack Inspection |
Pierce Chap 19 | |
| Typed Assembly Language | Exam stuff | ||
| 24-hour Take-home Final Exam | covering all topics; you will have 24 hours to do the Final |
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.