**Teaching assistants**: Arjya Das (arjyadas), Rupashree
Rangaiyengar (rupashreeh).

- Aug. 3: Introduction.
- Aug. 8, 10: Lattice theory. Lecture notes.
- Aug. 17, 22: Introduction to abstract interpretation. Lecture notes.
- Aug. 24, 29: Correctness of abstract interpretation. Associated lecture notes.
- Sep. 5, 7: Kildall's algorithm. Associated lecture notes.
- Sep. 12, 14, 19: Call strings approach to inter-procedural analysis.
- Sep. 21, 26: Functional approach to inter-procedural analysis.
- Sep. 28, Oct. 10, 12: Pointer analysis. Part 1 (pptx), Part 2 (pptx). Part 1 (pdf), Part 2 (pdf).
- Oct. 17, 19, 21: PDGs and Intraprocedural slicing
- Oct. 26, Oct. 31, Nov. 2: Hoare logic
- Nov. 7, 9: Simply Typed Lambda Calculus
- Nov. 14, 16: Polymorphic type system

We will assume that students have exposure to programming, the fundamental concepts of programming languages, and the basics of mathematical logic and discrete structures. However, no prior knowledge of program analysis is assumed.

- Notes on domains and fix-points prepared by Prof. Thomas Reps.
- Alfred Tarski, A lattice-theoretic fixpoint theorem and its applications, Pacific J. Mathematics, 5, pages 285--309, 1955.
- Gary A. Kildall,
A unified approach to global program
optimization.
In
*POPL '73: Proceedings of the 1st annual ACM SIGACT-SIGPLAN symposium on Principles of programming languages*, pages 194--206, New York, NY, USA, 1973. ACM Press. - Patrick Cousot and Radhia Cousot,
Abstract interpretation: a unified lattice model for static analysis
of programs by construction or approximation of fixpoints, In
*POPL '77: Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages*, pages 238--252, New York, NY, USA, 1977. ACM Press. - Anders MÃ¸ller and Michael I. Schwartzbach's book on dataflow analysis.
- Micha Sharir and Amir Pnueli: Two approaches to interprocedural data-flow analysis, in Program Flow Analysis, Ed. Muchnik and Jones (1981). A scan of this paper.
- Tom Reps, Susan Horwitz, Mooly Sagiv, Precise interprocedural dataflow analysis via graph reachability. (This is the IDFS paper.)
- Lectures slides from Cornell University on Hoare logic.
- Paper titled "ESP: Path-sensitive program verification in polynomial time" by Manuvir Das et al.
- The paper "The semantics of slicing" by Thomas Reps and Wuu Yang.
- S. Horwitz, T. Reps, and D. Binkley. Interprocedural slicing using dependence graphs.
- Jeanne Ferrante, Karl J Ottenstein, and Joe D Warren, The program dependence graph and its use in optimization.
- Karl J Ottenstein and Linda M Ottenstein, The program dependence graph in a software development environment.
- Notes on lambda calculus prepared by Prof. Thomas Reps.
- Slides on lambda calculus: Rewrite-based term languages.
- Benjamin C. Pierce, "Types and Programming Languages". Relevant chapters: Chapters 1-4 (preliminaries), 5 and 6 (basics of lambda calculus), and 8-9 (simple type systems, including simply typed lambda calculus).
- Reading material on simple type inference: Simple type systems. Slides 1-16 are about a very simple type system (which we did not cover in class), whereas slides 17-27 are about simply typed lambda calculus.
- L. Damas and R. Milner, Principal type-schemes for
functional programs. In
*POPL '82*, pages 207--212. This is our primary reference for polymorphic type inference.There are two typographic errors in this paper:

- In Algorithm W, page 5, in item (ii), the first "let" should be
W(A,e
_{1}) = (S_{1}, τ_{1}). - In item (iv) the first "let" should be
W(A,e
_{1}) = (S_{1}, τ_{1}).

- In Algorithm W, page 5, in item (ii), the first "let" should be
W(A,e
- Peter Hancock, Polymorphic type checking, and a type checker, Chapters 8 and 9 in Simon Peyton-Jones, "The Implementation of Functional Programming Languages", Prentice-Hall, New York. This is a secondary reference for polymorphic type inference. It gives more intuition and examples than the Damas-Milner paper. Covers unification (in Chap. 9).
- Nielson, Nielson, and Hankin, "Principles of Program Analysis", Springer-Verlag. This is also a secondary reference for polymorphic type inference. The relevant sections are 5, 5.1, 5.1.1, 5.3, and 5.3.1. They cover unification quite clearly. You can read sections 5.1.2, 5.2, 5.3.2, 5.3.3, and 5.3.4 for extra information.