Programming Research Group Technical Monograph PRG-104

Stephen Wilson

MSc thesis Nov 1992, 97 pages, ISBN 0-902928-81-3

This report describes the development of an interactive equational reasoning assistant, ERA, for an Orwell type notation (Orwell is a functional programming language which is very similar to Miranda; Miranda is a trademark of Research Software Ltd). It is designed to support both proof and program sythesis, using either the inductive or purely calculational styles. Aspects of the tool include pretty printed output, proof schemas, induction hypothesis generation, multiple current proofs, rewriting modulo associativity, and the ability to save proofs mid-stream.