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.13.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; CurryHoward 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)  Takehome 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.115.5  
W 7  Algorithmic Subtyping  Pierce Chap 16.116.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 1819  Final Exam  you will have 24 hours to do the Final, just like the midterm  Jan 1819 
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.