Automatic Verification of Functions with Accumulating Parameters

A. Ireland, Alan Bundy

Research output: Contribution to journalArticlepeer-review

Abstract / Description of output

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
Issue number2
Publication statusPublished - 1999


Dive into the research topics of 'Automatic Verification of Functions with Accumulating Parameters'. Together they form a unique fingerprint.

Cite this