Lecture Material and Assignments

Lecture Material

Introduction and Data Flow Analysis

• Lecture 1 - Introduction
• Lectures 2-3 - OCaml
• Lecture 4-5 - Data Flow Analysis
  • Kildall, A unified approach to global program optimization (optional)
• Lecture 6 - Static Single Assignment Form
  • Cytron, Ferrante, Rosen, Wegman, and Zadeck, Efficiently Computing Static Single Assignment Form and the Control Dependence Graph (required)

Coq and PL Theory

This material was developed by Benjamin C. Pierce.

• Lecture 7 - Coq basics, Basics.v
• Lecture 8 - Lists, Lists.v
• Lectures 9 - Polymorphism and higher-order functions, Poly.v
• Lecture 10 - More on induction, Ind.v
• Lecture 11 - Logic and relations, Logic.v
• Lectures 12-13 - Operational semantics, Semantics.v

Lambda Calculus, Types, Axiomatic Semantics

• Lecture 14 - Lambda calculus
• Lecture 15-17 - Type systems
• Lectures 18-19 - (Saurabh Srivastava) Axiomatic semantics
• Lectures 20-21 - Type qualifiers
• Lecture 22 - Abstract interpretation

Applications and Other

• Lecture 23 - How to give a research talk, How to write a research paper
• Lecture 24 - Data race detection for C
• Lecture 25 - (Mike Furr) Type Checking Foreign Function Interfaces
• Lecture 26 - Path Projection
• Lecture 27 (May 6) - Project presentations
  Piotr and Peter - Verifying Programs with Lists
  Ray - Improving the Cinquecento Interpreter
  Seth - Using Types to Improve Performance in Diamondback Ruby
  Ron - DynJQual: Dynamic Type Checking in Java
• Lecture 28 (May 11) - Project presentations
  Zhongqian and Daehwan - Proving translation faithfulness and type soundness of PRuby using Coq
  Alex and John - Ruby Polish: Static Bug Detection in Ruby Programs
  Hossam and Hassan - Automatic Code Refactoring
  Mark and Tandeep - DNote: Generating Type Annotations for Ruby programs using DRuby

Assignments

• Project 1 - Programming in OCaml, boolean formulae
• Project 2 - Data flow analysis
• Homework 1, due March 2 - complete the exercises marked CMSC 631 in Basics.v and Lists.v.
• Homework 2, due March 9 - complete the exercises marked CMSC 631 in Poly.v.
• Homework 3, due March 23 - complete the exercises marked CMSC 631 in Ind.v and Logic.v.
• Homework 4, due March 30 - complete the exercises marked CMSC 631 in Semantics.v.
• Homework 5, due April 8 - Lambda calculus and type systems (here is the latex source for the file, in case it's helpful in writing up your solutions) Sample solution (partial), sample solution to problem 4
• Project 3 - Type inference