Proof optimization for partial redundancy elimination

DOI10.1016/j.jlap.2009.05.002zbMath1187.68167OpenAlexW1989185026MaRDI QIDQ843219

Tarmo Uustalu, Ando Saabas

Publication date: 29 September 2009

Published in: The Journal of Logic and Algebraic Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.jlap.2009.05.002

zbMATH Keywords

type systemsproof-carrying codepartial redundancy eliminationprogram proof transformationsoundness and improvement of dataflow analyses and optimizations

Mathematics Subject Classification ID

Theory of software (68N99)

Related Items (1)

Relational bytecode correlations

Cites Work

• Unnamed Item
• Unnamed Item
• A compositional natural semantics and Hoare logic for low-level languages
• Program and proof optimizations with type systems
• Partial redundancy elimination: A simple, pragmatic, and provably correct algorithm.
• A program logic for resources
• Simple relational correctness proofs for static analyses and program transformations
• Proof-Producing Program Analysis
• Certificate Translation for Optimizing Compilers
• A solution to a problem with Morel and Renvoise's “Global optimization by suppression of partial redundancies”
• Global optimization by suppression of partial redundancies
• Automated soundness proofs for dataflow analyses and transformations via local rules
• An axiomatic basis for computer programming
• Programming Languages and Systems

This page was built for publication: Proof optimization for partial redundancy elimination