Automatic verification of functions with accumulating parameters

Andrew Ireland, Alan Bundy

Research output: Contribution to journalArticle

13 Citations (Scopus)

Abstract

Proof by mathematical induction plays a crucial role in reasoning about functional programs. A generalization step often holds the key to discovering an inductive proof. We present a generalization technique which is particularly applicable when reasoning about functional programs involving accumulating parameters. We provide empirical evidence for the success of our technique and show how it is contributing to the ongoing development of a parallelizing compiler for Standard ML.

Original languageEnglish
Pages (from-to)225-245
Number of pages21
JournalJournal of Functional Programming
Volume9
Issue number2
Publication statusPublished - Mar 1999

Cite this