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:
<![CDATA[
@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"}
]]></plaintext></p></div></div>