Abstract
We demonstrate a method for describing data-flow analyses based program optimizations as compositional type systems with a transformation component. Analysis results are presented in terms of types ascribed to expressions and statements, certifiable by type derivations, and the transformation component carries out the optimizations that the type derivations license. We describe dead code elimination and common subexpression elimination. In the case of common subexpression elimination we circumvent non-compositionality with a combined type system for a combination of two analyses. The motivation of this work lies in certified code applications, where an optimization of a program must be supported by a checkable justification. As an example application we highlight "proof optimization", i.e., mechanical transformation of a program's functional correctness proof together with the program, based on the analysis type derivation.
| Original language | English |
|---|---|
| Pages (from-to) | 131-154 |
| Number of pages | 24 |
| Journal | Journal of Logic and Algebraic Programming |
| Volume | 77 |
| Issue number | 1-2 |
| DOIs | |
| Publication status | Published - Sept 2008 |
Bibliographical note
Funding Information:We are grateful to Peter Thiemann, Bernd Fischer and David Sands for discussions and to the two anonymous referees of this paper for their very helpful remarks and suggestions. This work was supported by the Estonian Science Foundation Grant Nos. 5567 and 6940 and the EU FP6 IST integrated project MOBIUS.
Other keywords
- Certification
- Data-flow analyses
- Optimizations
- Proof optimization
- Type systems