
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
