Program Derivation by Proof Transformation

In the proofs-as-programs methodology, verified programs are developed through theorem-proving in a constructive logic. Under this approach, the theorem-proving process can be regarded as a program derivation process. The merits of this approach to programming are twofold. First, working with proofs instead of programs concentrates the developer's effort on the intellectually difficult part of the development process: understanding, solving, and explaining the solution to a mathematical problem. Second, the proof provides a formal and trustworthy basis for an explanation of the program. This thesis investigates the use of proof transformations as a way to address important concerns in program derivation that are not addressed by theorem-proving alone. One difficulty with the proofs-as-programs strategy arises from the conflict between elegance and efficiency. A simple, elegant proof may lead to an inefficient program. A more complex proof that corresponds to a more efficient program ma..