Proof optimization for partial redundancy elimination

Partial redundancy elimination is a subtle optimization which performs common subexpression elimination and expression motion at the same time. In this paper, we use it as an example to promote and demonstrate the scalability of the technology of proof optimization. By this we mean automatic transformation of a given program's Hoare logic proof of functional correctness or resource usage into one of the optimized program, guided by a type-derivation representation of the result of the underlying dataflow analyses. A proof optimizer is a useful tool for the producer's side in a natural proof-carrying code scenario where programs are proved correct prior to optimizing compilation before transmission to the consumer. We present a type-systematic description of the underlying analyses and of the optimization for the while language, demonstrate that the optimization is semantically sound and improving in a formulation using type-indexed relations, and then show that these arguments can be transferred to automatic transformations of functional correctness/resource usage proofs in Hoare logics. For the improvement part, we instrument the standard semantics and Hoare logic so that evaluations of expressions become a resource.