Calendar & Readings

SES # TOPICS READINGS KEY DATES
Unit 1: Intro to Functional Programming & Operational Semantics
1 Introduction to Functional Programming and Types

Some interesting reading about the genesis of functional programming:

Backus, John. "Can Programming be Liberated from the Von Neumann Style? A Functional Style and its Algebra of Programs." Magazine Communications of the ACM 8, no. 21 (1978): 613–41.

Hudak, Hughes, Peyton Jones, et al. This resource may not render correctly in a screen reader."A History of Haskell: Being Lazy With Class." (PDF) 2007.

 Problem Set 1 Out
2 Lambda Calculus

Suggested Reading:

Buy at MIT Press Buy at Amazon Pierce, Benjamin C. Chapter 5 in Types and Programming Languages. MIT Press, 2002. ISBN: 9780262162098. [Preview with Google Books]

  
3 Big-Step vs. Small-Step Semantics and the λLet Calculus    
4 Coq Crash Course (Examples in Operational Semantics)   Problem Set 1 due
Unit 2: Type Theory
5 Introduction to Simple Types

Buy at MIT Press Buy at Amazon Cardelli's, Luca. "Type Systems." In Types and Programming Languages. MIT Press, 2002. ISBN: 9780262162098.

 Problem Set 2 Out
6 Hindley-Milner Type Inference and Polymorphic Types    
7 Algebraic Data Types & Their Ingredients: Product, Sum, and Recursive Types    
8 Type Classes and Subtyping    
Unit 3: Types for Imperative Programs
9 Monads  

Problem Set 2 due

Problem Set 3 Out
10 Typing of Imperative Programs    
11 Verification of Complex Properties with Types: From Information Flow to Race Detection

Myers, A. C. "JFlow: Practical Mostly-static Information Flow Control." Principles of Programming Languages (1999): 228–41.

Flanagan, C., and S. N. Freund. "Type-based Race Detection for Java." ACM SIGPLAN Notices 35, no. 5 (2000): 219–32.

  
Unit 4: Axiomatic Semantics
12 Intro to Axiomatic Semantics

Floyd, Robert. This resource may not render correctly in a screen reader."Assigning Meanings to Programs." (PDF)

 Problem Set 4 Out
13 Verification Condition Generation Hoare. "An Axiomatic Basis for Computer Programming." Communications of the ACM 12, no. 10 (1969): 576–80. Problem Set 3 due
14 Total Correctness and Termination    
15 Separation Logic    
16 Axiomatic Semantics for Concurrency: Rely-Guarantee & Concurrent Separation Logic    
Unit 5: Abstract Interpretation
17 Dataflow Analysis, Lattices, Fixed Points Kildall, Gary. "A Unified Approach to Global Program Optimization." Principles of Programming Languages (1973): 194–206.

Problem Set 4 due

Problem Set 5 Out
18 Abstract Interpretation, Galois Connections Cousot, P., and R. Cousot. "Abstract Interpretation: A Unified Lattice Model for Static analysis of Programs by Construction or Approximation of Fixpoints." Principles of Programming Languages (1977): 238–52.  
19 Abstract Interpretation, Galois Connections (cont.)    
20 The Heap: Inferring Loop Invariants About Data Structure Shape

Sagiv, Reps, et al. "Solving Shape-Analysis Problems in Languages with Destructive Updating." Principles of Programming Languages 20, no. 1 (1993): 1–50.

  
Unit 6: Model Checking
21 Intro to Models and Properties    
22 Temporal Logic   Problem Set 5 due
23 Explicit State Model Checking   Problem Set 6 Out
24 Symbolic Model Checking    
25 Software Model Checking with Abstraction Refinement

Henzinger, T. A., R. Jhala, et al. "Lazy Abstraction." Principles of Programming Languages ACM 37, no. 1 (2002): 58–70.

Ball, T., R. Majumdar, et al. "Automatic Predicate Abstraction of C Programs." ACM SIGPLAN Notices 36, no. 5 (2001): 203–13.

  
26 From Model Checking to Synthesis   Problem Set 6 due