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.



@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"}