Department of Computer Science and Technology

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