Program transforlation thesis available for ftp

My PhD thesis, Correct Higher-Order Program Transformations, is now
available for anonymous ftp as:


ftp.ccs.neu.edu:/pub/people/steck/thesis.ps


Here's the abstract:


> We present a method for proving the correctness of
> compiler optimizations for higher-order programming
> languages. Programs are annotated with propositions
> derived as the solutions to dataflow constraints
> formulated as local consistency conditions for each
> parse tree node. We can prove that any such solution
> yields sound annotations, that is, the propositions are
> true. Each compiler optimization is presented as a
> source-to-source transformation. Using the annotations
> and additional constraint information, we can prove
> that the optimization is correct with respect to some
> criterion. The correctness criterion is similar for
> each transformation. The particular optimizations we
> exhibit are {\em selective and lightweight closure
> conversion} (constructing source-level closures for
> procedures, with two variations), {\em \ultrabeta} (a
> generalization of copy propagation to higher-order
> languages), and {\em selective thunkification}
> (transforming call-by-name programs into call-by-value
> equivalents).


Enjoy.


-- Paul
--

Return to the comp.compilers page.
Search the comp.compilers archives again.