Lambda the Ultimate

Type-sensitive control-flow analysis, John Reppy, 2006 ML Workshop.

Higher-order typed languages, such as ML, provide strong support for data and type abstraction. While such abstraction is often viewed as costing performance, there are situations where it may provide opportunities for more aggressive program optimization. Specifically, we can exploit the fact that type abstraction guarantees representation independence, which allows the compiler to specialize data representations. This paper describes a first step in supporting such optimizations; namely a modular control-flow analysis that uses the program’s type information to compute more precise results. We present our algorithm as an extension of Serrano’s version of 0-CFA and we show that it respects types. We also discuss applications of the analysis with a specific focus on optimizing Concurrent ML programs.

Near-Concrete Program Interpretation, By Paritosh Shroff, Scott F. Smith, Christian Skalka:

We develop near-concrete program interpretation (NCI), a higher-order program analysis that achieves high precision via close, yet decidable, simulation of operational (concrete) semantics. NCI models mutable heaps with possibly recursive structure, and achieves flow-, context- and path-sensitivity in a uniform setting. The analysis also extracts a nugget that characterizes the value bindings resulting from program execution; it can be used to statically determine a wide range of non-trivial properties. The technical novelty of the system lies in a prune-rerun technique for approximating recursive functions. To illustrate the generality and usefulness of the system, we show how it can be used to statically enforce temporal program safety, information flow security, and array bounds checking properties.

Very interesting paper that brings sophisticated higher order analysis to abstract interpretation. The paper proves the algorithm is exponential for certain types of programs, akin to ML type inference, and polynomial for first order programs. They have a working implementation in OCaml.

Hi all,
i am new to functional programming paradigm. One thing that i have doubt about is lazy evaluation. I dont know how much it is useful in practical sense of programming? Is it useful, because it allows us to be less careful at the time of writing the program ( by not giving syntax errors) and then crashing suddenly during actual execution of the function .. i am not sure. Can you please explain a little on this topic.

regards
chinmay