Equivalence checking of two functional programs using inductive theorem provers

DOI10.1016/j.ipl.2017.08.002zbMath1419.68038OpenAlexW2752201671MaRDI QIDQ2410575

M. Demba

Publication date: 18 October 2017

Published in: Information Processing Letters (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.ipl.2017.08.002

zbMATH Keywords

generalizationinductive theorem provingloop invariantprogram correctnessprogram schemas

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18)

Uses Software

• HipSpec
• IsaCoSy

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• 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
• 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
• Transforming Programs into Recursive Functions