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.13.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  
CurryHoward 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  5hour Takehome Midterm between Oct 1926  all topics weeks 15  
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.115.5 on Subtyping 

11  More Subtyping  Class notes on subtyping (Monday,
Wednesday) Pierce Chap 15.115.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  
24hour Takehome 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.