Automatic verification of functions with accumulating parameters

DOI10.1017/S0956796899003408zbMATH Open0940.68023OpenAlexW2169770847MaRDI QIDQ4267724FDOQ4267724

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

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

zbMATH Keywords

reasoning about functional programs

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18)

Cited In (6)

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

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)