Our current goal is to develop a generic framwork for constraint-based program analysis.
High-level programming languages improve programmer productivity, but their compilers
require complex program analyses to make programs run efficiently. Recently a number
of program analyses have been suggested which use constraint solving techniques to infer
interesting program properties.
A recent trend is to present (and implement) program analysis as non-standard type inference, by marrying a type language with notation for decorating type expressions, the decorations expressing the program properties of interest. The direction that much of this research is currently taking is to extend the underlying type language beyond what the programming language requires, for example to include intersection types or subtyping.
Our view is that, while it is both convenient and elegant to express program analysis as constrained-type inference, the language for expressing program properties should not necessarily be coupled closely with the type system. From the point of view of the analysis designer and implementor, it seems more attractive to utilise expressive constraint languages that come with well-developed solvers and well-understood theories, making only the reasonable assumption that programs presented to the analyser are well-typed and explicitly typed, for example by an earlier type inference phase in a compiler.
We have designed and implemented a binding-time and strictness analysis for Haskell and incorporated both analyses into the GHC compiler. Most recently, we have also incorporated a exception analysis.
Last modified: Fri Aug 23 11:36:09 GMT-8 2002