Automatic verification of functions with accumulating parameters

DOI10.1017/S0956796899003408MaRDI QIDQ4267724zbMATH OpenOpenAlexFDO

Authors Andrew Ireland, Alan Bundy

Publication date 19 July 2000

Published in Journal of Functional Programming (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1017/s0956796899003408

zbMATH Keywords

reasoning about functional programs

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18)

Recommendations

• Deaccumulation techniques for improving provability
• Advances in Computing Science – ASIAN 2003. Progamming Languages and Distributed Computation Programming Languages and Distributed Computation
• scientific article; zbMATH DE number 1082080
• Induction proofs with partial functions

Cited in

(6)

• Equivalence checking of two functional programs using inductive theorem provers
• Discovering applications of higher order functions through proof planning
• Automatic generation of generalization lemmas for proving properties of tail-recursive definitions
• Advances in Computing Science – ASIAN 2003. Progamming Languages and Distributed Computation Programming Languages and Distributed Computation
• An integrated approach to high integrity software verification
• Deaccumulation techniques for improving provability

This page was built for publication: Automatic verification of functions with accumulating parameters

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4267724)