Princeton University

Computer Science 441
Programming Languages
Andrew Appel

Fall 2009

General Information       Schedule       Policies

This schedule is approximate and subject to adjustment.
Be sure to recheck the schedule each Thursday to see whether Friday's class is a Lecture or Lab.
Lab sessions are at 10:00 and 11:00.

Date Monday Wednesday Friday
Sep 14-18 no class today no class today
Coq Installation Notes
Preface; Basics (Basics.v)
Introduction; functional programming (numbers, lists); basic proofs
Sep 21-25 Basics; Lists Lists (Lists.v)
Homework 0 due
Lab (Friend 009)
Homework 1 due Sunday
Sep 28 - Oct 2 Polymorphism (Poly.v) Polymorphism Lab (Friend 009)
Homework 2 due Sunday
Oct 5-7 Propositions (Props.v) Logic (Logic.v) Lecture (CS 105) or Lab (Friend 009)
Homework 3 due Sunday
Oct 12-16 ML programming language; Caml core language
ML; Binomial Queues
Caml reference
Sedgewick Algs 3e, §9.7
Lab (Friend 009)
Homework 4 due Sunday
Oct 19-23 Imperative programs (SfLib.v Imp.v) Imperative programs Lecture (CS 105)
Homework 5 due Sunday
Oct 26-29 Imperative Programs; omega tactic (Omega.v) Informal Proofs In-class midterm exam (CS 105)
Take-home midterm due
Fall Break
Nov 9-13 Program Equivalence (Equiv.v) Program Equivalence Lab (Friend 009)
Homework 6 due Sunday
Nov 16-20 Hoare Logic (Hoare.v) Hoare Logic Lecture (CS 105)
Homework 7 due Sunday
Nov 23-25 Small-step operational semantics (Smallstep.v) Small-step O.S. (holiday)
Nov 30 - Dec 4 Lambda-calculus (Stlc.v)
Homework 8 due
Lambda-calculus Lecture (CS 105)
Homework 9 due Sunday
Dec 7-11 More lambda-calculus (MoreStlc.v) t.b.a. Lab (Friend 009)
Homework 10 due Sunday
Dec 14-18 Compiler Correctness (Compiler.v) Coq tips; (Induction.v)
The Big Picture
Lab, upon request
Jan 8 Homework 11 due
Jan 13-16 Final Exam: Part 1, Part 2