#### Automating Squiggol

#### Ursula Martin, Tobias Nipkow

The Squiggol style of progam development is shown to be readily automated
using LP, an equational reasoning theorem prover. Higher-order functions
are handled by currying and the introduction of an application operator. We
present an automated verification of Bird's development of the maximum
segment sum algorithm, and a similar treatment of a proof of the binomial
theorem.
dvi

BibTeX:

@inproceedings{Martin-Nipkow-Squiggol,
author="Ursula Martin and Tobias Nipkow",
title="Automating {Squiggol}",
booktitle="Programming Concepts and Methods",
editor="M. Broy and C.B. Jones",
year=1990,publisher="North-Holland",pages="233--247"}