Equivalence checking of two functional programs using inductive theorem provers
From MaRDI portal
Recommendations
- Inference rules for proving the equivalence of recursive procedures
- Inference rules for proving the equivalence of recursive procedures
- Towards modularly comparing programs using automated theorem provers
- Inferring the equivalence of functional programs that mutate data
- Program equivalence by circular reasoning
Cites work
- scientific article; zbMATH DE number 1615264 (Why is no real title available?)
- scientific article; zbMATH DE number 3702108 (Why is no real title available?)
- scientific article; zbMATH DE number 1889386 (Why is no real title available?)
- Automatic generation of generalization lemmas for proving properties of tail-recursive definitions
- Automatic verification of functions with accumulating parameters
- Automating Inductive Proofs Using Theory Exploration
- Conjecture synthesis for inductive theories
- Mechanizing structural induction. II: Strategies
- Proof-pattern recognition and lemma discovery in ACL2
- Recursive functions of symbolic expressions and their computation by machine, Part I
- Transforming programs into recursive functions
Cited in
(7)- Inferring the equivalence of functional programs that mutate data
- Towards modularly comparing programs using automated theorem provers
- Equivalence of two formal semantics for functional logic programs
- Effective use of SMT solvers for program equivalence checking through invariant-sketching and query-decomposition
- Program equivalence checking by two-tape automata
- An algorithm deciding functional equivalence in a new class of program schemes
- Equivalence Checking of Non-deterministic Operations
This page was built for publication: Equivalence checking of two functional programs using inductive theorem provers
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2410575)
