Using the HOL Prove Assistant for proving the Correctness of term Rewriting Rules reducing Terms of Sequential Behavior
No abstract available.
Related papers
- Verifying Term Graph Optimizations using Isabelle/HOL CPP 2023
- Verifying and improving Halide's term rewriting system with program synthesis OOPSLA 2020
- IsaRare: Automatic Verification of SMT Rewrites in Isabelle/HOL TACAS 2024
- A Formalization of the Development Closedness Criterion for Left-Linear Term Rewrite Systems CPP 2023
- Formal Models of Distributed Memory Management ICFP 1997
- Termination of rewriting in the Calculus of Constructions JFP 2003
- PfComp: A Verified Compiler for Packet Filtering Leveraging Binary Decision Diagrams CPP 2024
- A Correctness Proof for Combinator Reduction with Cycles TOPLAS 1990