Proof optimization for partial redundancy elimination
From MaRDI portal
Publication:843219
DOI10.1016/J.JLAP.2009.05.002zbMATH Open1187.68167OpenAlexW1989185026MaRDI QIDQ843219FDOQ843219
Authors: Ando Saabas, Tarmo Uustalu 
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
Recommendations
- Optimizing proof search in model elimination
- Partial redundancy elimination: A simple, pragmatic, and provably correct algorithm.
- scientific article; zbMATH DE number 1189109
- An efficient and flexible approach to resolution proof reduction
- scientific article; zbMATH DE number 1538015
- Improved single pass algorithms for resolution proof reduction
- Loop Elimination, a Sound Optimisation Technique for PTTP Related Theorem Proving
- Reductions for non-clausal theorem proving
- Reducing redundancy in cut-elimination by resolution
- scientific article; zbMATH DE number 4182873
type systemsproof-carrying codepartial redundancy eliminationprogram proof transformationsoundness and improvement of dataflow analyses and optimizations
Cites Work
- Title not available (Why is that?)
- An axiomatic basis for computer programming
- A compositional natural semantics and Hoare logic for low-level languages
- Simple relational correctness proofs for static analyses and program transformations
- Automated soundness proofs for dataflow analyses and transformations via local rules
- A program logic for resources
- Program and proof optimizations with type systems
- Title not available (Why is that?)
- Partial redundancy elimination: A simple, pragmatic, and provably correct algorithm.
- 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
- Automatic construction of Hoare proofs from abstract interpretation results.
Cited In (13)
- \(\mathrm{PART}_{\mathrm{PW}}\): from partial analysis results to a proof witness
- Relational bytecode correlations
- Redundancy elimination for LF
- Partial redundancy elimination: A simple, pragmatic, and provably correct algorithm.
- Program and proof optimizations with type systems
- Head linear reduction and pure proof net extraction
- Simple relational correctness proofs for static analyses and program transformations
- Title not available (Why is that?)
- Constructive decision via redundancy-free proof-search
- Automatic Parallelization and Optimization of Programs by Proof Rewriting
- Redundancy elimination with a lexicographic solved form
- Compiler Construction
- Loop Elimination, a Sound Optimisation Technique for PTTP Related Theorem Proving
This page was built for publication: Proof optimization for partial redundancy elimination
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q843219)
