Department
Princeton University

Computer Science 510
Programming Languages
Andrew Appel

Spring 2017

General Information       Schedule       Policies

This schedule is subject to change, especially for dates more than 1 week in the future.

Lab sessions are Friday 10am-noon, place to be determined, attendance optional, and you can arrive late or leave early. Lectures are at 11:00 and I would appreciate it if you arrive on time.

Date Monday,    Wednesday Friday Homework
Feb 6-10 Introduction; functional programming (numbers, lists); basic proofs: Coq Installation Notes; Preface; Basics; Induction; Lists ( Basics.v, Induction.v, Lists.v ) Lab Homework 1
Feb 13-17 Sequent Calculus, Polymorphism, More basic tactics (Poly.v, Tactics.v) Lab Homework 2
Feb 20-24 Logic in Coq, Inductively defined propositions, Curry-Howard correspondence, Maps (Logic.v, IndProp.v, ProofObjects.v, Maps.v) Lab Homework 3
Feb 27-Mar 3 ML programming language
interp.ml; Caml core language, Caml reference
Sedgewick Algs 3e, §9.7
Lab Homework 4
Mar 6-10 Proving correctness of functional programs, permutations, selection sort, insertion sort (VFA.v, Perm.v, Selection.v, Sort.v) Lab Homework 5
Mar 13-17 Imperative programs ( Imp.v); Search trees (SearchTree.v) Take-home midterm due
Spring Break
Mar 27-31 Program Equivalence (Equiv.v), Hoare Logic (Hoare.v) Lab Homework 6
Apr 3-7 Hoare Logic (Hoare2.v), Small-step operational semantics (Smallstep.v) Lab Homework 7
Apr 10-14 Tactic automation (Auto.v), red-black trees (Redblack.v); Type systems (lecture notes; Types.v) Lab Homework 8
Apr 17-21 Satisfiability (reading: Boolean Satisfiability Solvers) Lab Homework 9
Apr 24-30 Lambda Calculus (STLC.pdf, Stlc.v, StlcProp.v, MoreStlc.v, Typechecking.v); Birth of CS Lab Project proposal
May 1-5 extraction; abstract data types
(Extraction.v, ADT.v); Separation Logic (read Chapters 2 and 3 of PLCC).
May 8 reading period -- no class -- last homework due Homework 10 or Project Checkpoint due
May 16 Due date for final project (if not Stlc.v)