Princeton University
Computer Science Department

Computer Science 441
Programming Languages

David Walker

Fall 2005

Home Page                                         Notes & Assignments

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

MinML Typing slides

M 17 Type Safety Pierce Chap 8.3, 9.3

MinML Safety slides

Assignment #4:  Typed Lambda Calculus (Due: W Oct 26)
W 19 Product types + begin sums Pierce Chap 11

Sums & Products slides

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

Existential Slides

M 28 Quantified Types:    Type Inference Pierce Chap 22.1 - 22.5

Type Inference Slides

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

FJ Slides

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.