| Summary: | This thesis establishes formal equational properties of multi-stage
calculi and related proof techniques that support analyses of staged
programs. A key promise of staging is to make programs efficient
without destroying clarity, thereby reducing the likelihood of bugs.
However, few publications rigorously verify that their staged
programs indeed behave as intended. In fact, little is known about
how staged programs can be verified, or what correctness issues
staging introduces. To solve this problem, I show a reduction of
the correctness of a staged program to that of an unstaged program.
This reduction not only clarifies the effects of staging on program
behavior but also eases verification, as unstaged programs are more
susceptible to existing reasoning techniques. I also demonstrate
that important single-stage reasoning techniques apply to staged
programs. These techniques are useful for establishing side
conditions for the reduction and for discovering or validating
further reasoning principles. === NSF grant CCF-0747431
|
|---|
