We present a type-based flow analysis for simply typed lambda calculus with booleans, data-structures and recursion. The analysis is exact in the following sense: if the analysis predicts a redex, there exists a reduction sequence (using standard reduction plus context propagation rules) such that this redex will be reduced. The precision is accomplished using intersection typing.

It follows that the analysis is non-elementary recursive – more surprisingly, the analysis is decidable. We argue that the specification of such an analysis provides a good starting point for developing new flow analyses and an important benchmark against which other flow analyses can be compared. Furthermore, we believe that the techniques employed for stating and proving exactness are of independent interest: they provide methods for reasoning about the precision of program analyses.

A preliminary version of this paper has previously been published (Mossin 1997b). The present paper extends, elaborates and corrects this previously published abstract.