Princeton University

Computer Science 510
Programming Languages
Andrew Appel

Spring 2023

General Information       Schedule       Policies

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

Lab sessions (optional) are listed on the main page.

Date Monday,    Wednesday Thu/Fri Homework
Jan 30 - Feb 3 Introduction; functional programming (numbers, lists); basic proofs: Coq Installation Notes; Preface; Basics; Induction; Lists ( Basics.v, Induction.v, Lists.v ) Lab Homework 1
Feb 6-10 Sequent Calculus, Polymorphism, More basic tactics (Poly.v, Tactics.v) Lab Homework 2
Feb 13-17 Logic in Coq, Inductively defined propositions, Curry-Howard correspondence (Logic.v, IndProp.v, ProofObjects.v) Lab Homework 3
Feb 20-24 ML programming language; Caml core language, Caml reference; Installing Ocaml;,; Denotational Semantics; Binomial Queues, Maps Lab Homework 4
Feb 27 - Mar 3 Proving correctness of functional programs, permutations, selection sort, insertion sort (VFA.v, Perm.v, Selection.v, Sort.v)
Maps, Search Trees, Abstract Data Types (Maps.v SearchTree.v, ADT.v)
Lab Homework 5
Mar 6-10 SOS, Imperative programs, Automation ( Imp.v, Auto.v); Search trees, Red-Black trees, (SearchTree.v, Redblack.v), Bentley-Sedgewick Trees Take-home midterm due
Spring Break: No class March 13-17
Mar 20-24 Program Equivalence (Equiv.v), Hoare Logic (Hoare.v) Lab Homework 6
Mar 27-31 Hoare Logic (Hoare2.v), Small-step operational semantics (Smallstep.v), Type systems (lecture notes; Types.v) Lab Homework 7
Apr 3-7 Simply typed lambda calculus; Type Soundness; subtyping (lecture notes, Stlc.v, StlcProp.v, Sub.v) Lab Homework 8
Apr 10-14 SAT, SMT (reading: Boolean Satisfiability Solvers); Dafny (selection sort) Lab Homework 9
Apr 17-21 Separation Logic (read Chapters 2 and 3 of PLCC); Verifiable C, vc.tgz Lab
Apr 24-28 Verifying C programs (Verifiable C), vc.tgz Lab
May 1 Reading period
May 9 Homework 10 due (if you're not doing Homework 11) Homework 10
May 12 Homework 11 due (if you didn't do Homework 10) Homework 11