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" 
C.A.R. Hoare. Hints
on Programming Language Design.
Gregor, Jarvi, Siek, Lumsdaine, Dos Reis, and Stroustrup.
Concepts: Linguistic Support for Generic Programming in C++.
Winskel, Chapter 1

Signup on the course google group introduce yourself there.  
T  8/30  Bigstep operational semantics 
Winskel, Chapter 2


R  9/1  Smallstep 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
C.A.R. Hoare. An
Axiomatic Basis for Computer Programming.
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
To page 725 of
John
C. Reynolds. Definitional
interpreters for higherorder programming
languages.


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 higherorder 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 SECDMachine, and the lambdaCalculus.


R  10/13  Objectoriented languages 
Pierce, Chapters 15 and 16
Cardelli and Wegner. On
Understanding Types, Data Abstraction, and Polymorphism.

HW 7 due  
T  10/18  Nominal Subtyping 
Igarashi, Pierce, and
Wadler. Featherweight Java: A
Minimal Core Calculus for Java and GJ.


R  10/20  Program Equivalence and Logical Relations 
Harper, Chapter 50


T  10/25  Generics (aka. Parametric Polymorphism) 
Pierce, Chapter 23
John C. Reynolds. Towards a theory of type structure.


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  Dataflow Analysis 
Nielson, Nielson, and Hankin. Principles of Program Analysis, Chapter 2
(through section 2.4).


R  11/10  More dataflow 
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:307:00pm, ECCS 1B28  Final Exam 