Edinburgh Research Explorer

Automatic Verification of Functions with Accumulating Parameters

Research output: Contribution to journalArticle

Related Edinburgh Organisations

Open Access permissions

Open

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

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.

Download statistics

No data available

ID: 402319