Technical reports
Automating Squiggol
Ursula Martin, Tobias Nipkow
September 1989, 16 pages
DOI: 10.48456/tr-179
Abstract
The Squiggol style of program 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 version of Bird’s development of the maximum segment sum algorithm, and a similar treatment of a proof of the binomial theorem.
Full text
PDF (1.0 MB)
BibTeX record
@TechReport{UCAM-CL-TR-179, author = {Martin, Ursula and Nipkow, Tobias}, title = {{Automating Squiggol}}, year = 1989, month = sep, url = {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-179.pdf}, institution = {University of Cambridge, Computer Laboratory}, doi = {10.48456/tr-179}, number = {UCAM-CL-TR-179} }