We are interested in understanding just how a program analysis
justifies the program transformation that is typically based upon it.
Many interesting optimizations depend on interprocedural analyses,
which collect information about program units larger than a single
procedure. Such optimizations are widespread in higher-order
languages such as Scheme or ML, and play an important role in ordinary
imperative languages as well. Despite decades of work on abstract
interpretation and related analysis frameworks, there are still very
few examples in which an analysis is actually used to prove the
correctness of an associated transformation. We seek to understand
this gap by doing a series of examples related to the compilation of
higher-order ``almost-functional'' languages like Scheme or ML. We
have studied a sequence of analysis-based transformations, including
offline partial evaluation, lightweight closure conversion, useless
variable elimination, and destructive update introduction. We also
seek to unify analysis-based transformations with the theory of
transformations based on contextual equivalence, and to extend all of
this theory to embrace programs that compute in parallel or
distributed settings.
More recently, we have been studying the foundations of program
analyses, providing new techniques for formulating and proving the
soundness of various analyses. We seek to extend this work to
context- and flow-dependent analyses, and to languages in which
procedures may be invoked implicitly via events, callbacks, or
aspects.
(Recent
Papers)