Princeton University
Computer Science Department

Computer Science 441
Programming Languages

David Walker

Fall 2007

Home Page                                         Notes & Assignments

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.

notes on installing sml and emacs mode

ML-intro-1 slides

ML-intro-2 slides


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

Type Inference Slides

  Quantified Types:    Type Inference


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

Featherweight Java Slides

Stack Inspection Slides

  Typed Assembly Language Exam stuff

Typed assembly language slides

  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.