CMSC 631, Spring 2009

Program Analysis and Understanding

Lecture Material and Assignments

Lecture Material

Introduction and Data Flow Analysis

Coq and PL Theory

This material was developed by Benjamin C. Pierce.

Lambda Calculus, Types, Axiomatic Semantics

Applications and Other

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

Valid HTML 4.01!

Web Accessibility