The following schedule lists the topics we will cover and approximately the number of meetings we will spend on each topic. The schedule is tentative. Most likely, some things will change during the semester, and I will revise the schedule as necessary.

The Reading column lists the assigned reading for the meeting. You should view the readings as an introduction to spark discussion in class.

The Assignment column lists the due date for each assignment.

Date Topic Reading Assignment
T 8/23 Welcome, course overview, and Caml tutorial
R 8/25 The C++0x Proposal for "Concepts"
Gregor, Jarvi, Siek, Lumsdaine, Dos Reis, and Stroustrup. Concepts: Linguistic Support for Generic Programming in C++.
Winskel, Chapter 1
 Sign-up on the course google group introduce yourself there.
T 8/30 Big-step operational semantics
Winskel, Chapter 2
R 9/1 Small-step operational semantics
Pierce, Chapter 3
Optional. Chapter 3 of G.D. Plotkin. A Structural Approach to Operational Semantics.
HW 1 due
T 9/6 Proofs by induction, video Part A, Part B, Part C.
Harper, Chapter 2
Winskel, Chapter 3
R 9/8 More on induction, video Part A, Part B.
Winskel, Chapter 4
HW 2 due
T 9/13 Axiomatic Semantics
Winskel, Chapter 6
Optional. Robert W. Floyd. Assigning Meanings to Programs.
R 9/15 Axiomatic Semantics
C.A.R. Hoare. Proof of a Program: FIND.
HW 3 due
T 9/20 Functions
Pierce, Chapter 5
Henk Barendregt. Lambda Calculi with Types. (First two chapters.)
R 9/22 Types
Pierce, Chapter 8
 HW 4 due
T 9/27 Type Safety
Pierce, Chapter 9
R 9/29 Contextual Semantics and Exceptions
Andrew K. Wright and Matthias Felleisen. A Syntactic Approach to Type Soundness.
HW 5 due
T 10/4 Abstract Machines
Chapters 6 and 7 of Felleisen and Flatt. Programming Languages and Lambda Calculi.
Optional. Peter J. Landin. The mechanical evaluation of expressions.
R 10/6 From Interpreters to Abstract Machines
Pages 726 to the end of John C. Reynolds. Definitional interpreters for higher-order programming languages.
Mads Sig Ager, Dariusz Biernacki, Olivier Danvy, Jan Midtgaard. A functional correspondence between evaluators and abstract machines.
HW 6 due
T 10/11 Continuations
Chapters 8 and 9 of Felleisen and Flatt. Programming Languages and Lambda Calculi.
Optional. Matthias Felleisen and Daniel P. Friedman. Control operators, the SECD-Machine, and the lambda-Calculus.
R 10/13 Object-oriented languages
Pierce, Chapters 15 and 16
 HW 7 due
T 10/18 Nominal Subtyping
R 10/20 Program Equivalence and Logical Relations
Harper, Chapter 50
T 10/25 Generics (aka. Parametric Polymorphism)
Pierce, Chapter 23
R 10/27 Parametricity
Philip Wadler. Theorems for free!
Harper, Chapter 51
 Project proposal due
T 11/1 Process Equivalence and Bisimulation
Harper, Chapter 52
R 11/3 Partial Evaluation William R. Cook and Ralf Lammel. Tutorial on Online Partial Evaluation.
T 11/8 Data-flow Analysis
Nielson, Nielson, and Hankin. Principles of Program Analysis, Chapter 2 (through section 2.4).
R 11/10 More data-flow
John B. Kam and Jeffrey D. Ullman Monotone data flow analysis frameworks.
HW 8 due
T 11/15 Denotational Semantics
Winskel, Chapter 5
R 11/17 Domain Theory, video lecture
Chapter 6 of David A. Schmidt, Denotational Semantics
Optional. Dana Scott and Christopher Strachey. Towards a Mathematical Semantics for Computer Languages.
Project status update due.
T 11/22 No class: Fall Break
R 11/24 No class: Fall Break
T 11/29 Abstract Interpretation
Samson Abramsky and Chris Hankin. An Introduction to Abstract Interpretation.
R 12/1 Abstract Interpretation, continued
Optional. Patrick Cousot and Radhia Cousot. Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. Symposium on Principles of Programming Languages (POPL), 1977.
T 12/6 Project presentations
R 12/8 Project presentations
W 12/14 4:30-7:00pm, ECCS 1B28 Final Exam