[Colloq] Thesis defense: Igor Siveroni, Friday 12/14, 10am.

[Mitchell Wand]

THESIS DEFENSE

10:00am
Friday, December 14, 2001
149 Cullinane Hall
Northeastern University
(building 9 on the map at http://www.neu.edu/maps/maps.html)

IGOR SIVERONI

Correctness of Analysis-based Program Transformations of Functional
Programming Languages. 

Abstract:

Program transformations are an important part of optimizing compilers.
A program transformation takes advantage of information about
different aspects of a program's behavior i.e. program properties, to
improve the performance of the program. An analysis-based program
transformation gets this information from a program analysis: the
process of determining aspects of a program's behavior without
actually running it. We are interested in the relation between these
three elements: analysis, program property and the transformation it
allegedly justifies.

This presentation is concerned with the correctness of analysis-based
program transformations of functional programming languages, that is,
the process of proving that a transformation preserves the meaning of
the original program.  We claim that the core of this process relies
on the specification of the program property that justifies the
transformation in terms of the semantics of the language. We achieve
this by defining program properties as validation systems based on
execution traces of programs which can then be used to derive program
analyses using the well-known techniques of abstract interpretation.
We then divide the correctness proof into two parts: (1) The
transformation is first validated against the property specification
while (2) the analysis is proved to satisfy the same
specification. Program properties link both parts.


We show the correctness of two program transformations. The first
transformation identifies code expressions that do not contribute to
the final value of the program and replaces them with less
computationally-expensive expressions e.g. constants. The second
transformation removes such useless code, a process that also involves
the removal of useless variables.  In both cases we specify the
properties of the information used by the transformations and use
these specifications to derive program analyses. We show that the
results of the analyses satisfy the specifications and that the
transformation is meaning-preserving. We use big-step semantics, where
execution traces are defined as proof (derivation) trees, and present
the correctness proofs as tree (bi)simulation results.

Advisor: Mitchell Wand
Committee: Will Clinger, Jens Palsberg, Raj Rajaraman, David Lorenz