Table of Contents

Some years ago, when the Programming Languages research group at Oregon State University was discussing what to read, the Static Program Analysis lecture notes came up. The group didn’t end up reading the lecture notes, but I did. As I was going through them, I noticed that they were quite rigorous: the first several chapters cover a little bit of lattice theory, and the subsequent analyses – and the descriptions thereof – are quite precise. When I went to implement the algorithms in the textbook, I realized that just writing them down would not be enough. After all, the textbook also proves several properties of the lattice-based analyses, which would be lost in translation if I were to just write C++ or Haskell.

At the same time, I noticed that lots of recent papers in programming language theory were formalizing their results in Agda. Having played with dependent types before, I was excited to try it out. Thus began my journey to formalize (the first few chapters of) Static Program Analysis in Agda.

In all, I built a framework for static analyses, based on a tool called motone functions. This framework can be used to implement and reason about many different analyses (currently only a certain class called forward analyses, but that’s not hard limitation). Recently, I’ve proven the correctness of the algorithms my framework produces. Having reached this milestone, I’d like to pause and talk about what I’ve done.

In subsequent posts in this series, will describe what I have so far. It’s not perfect, and some work is yet to be done; however, getting to this point was no joke, and I think it’s worth discussing. In all, I’d like to cover the following major topics, spending a couple of posts on each:

Here are the posts that I’ve written so far for this series: