Exact Flow Analysis

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, then 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.

• Type: Conference
• Year: 1997
• Where: SAS
• Authors: Christian Mossin
• Keywords: Analysis, Formal Methods, SAS 1997, Simply Typed Lambda Calculus, Type-based flow Analysis