Flow analysis of typed higher-order programs. Rev. version.

*(English)*Zbl 0891.68025
Copenhagen: Univ. of Copenhagen, xii, 243 p. (1997).

Summary: This thesis concerns flow analysis of typed higher-order programs. Flow analysis attempts at compile time to predict the creation, flow and use of values. We present a suite of analyses based on type systems: they work by adding extra information to the standard types of the analysed program. The analyses are proven to be sound under any evaluation order.

The first two analyses, simple and sub-type based flow analysis, are known from the literature. We present a new modular formulation, allowing subexpressions to be analysed independently from their context without loss of precision.

Modularity makes it possible to extend the analyses with polymorphism which allows named functions to be used differently in different contexts. This leads to improved precision. We show that ML- and fix-polymorphic flow analysis is computable in polynomial time.

Finally, we present a flow analysis based on intersection types. We show a completeness result for this analysis: the analysis is precise up to not knowing which branch of a conditional is taken and not discarding any computation.

The sub-type based analysis can be given a very natural presentation using graphs. The graph formulation leads to an improvement over existing algorithms: single flow queries can be answered in linear time and full flow analysis can be performed in quadratic time (under assumption that the size of standard types is bounded).

We argue that the presented analyses are not restricted to a specific standard type system, but are applicable to any functional programming language; even dynamically typed languages.

The first two analyses, simple and sub-type based flow analysis, are known from the literature. We present a new modular formulation, allowing subexpressions to be analysed independently from their context without loss of precision.

Modularity makes it possible to extend the analyses with polymorphism which allows named functions to be used differently in different contexts. This leads to improved precision. We show that ML- and fix-polymorphic flow analysis is computable in polynomial time.

Finally, we present a flow analysis based on intersection types. We show a completeness result for this analysis: the analysis is precise up to not knowing which branch of a conditional is taken and not discarding any computation.

The sub-type based analysis can be given a very natural presentation using graphs. The graph formulation leads to an improvement over existing algorithms: single flow queries can be answered in linear time and full flow analysis can be performed in quadratic time (under assumption that the size of standard types is bounded).

We argue that the presented analyses are not restricted to a specific standard type system, but are applicable to any functional programming language; even dynamically typed languages.