Tjark Weber. Master's thesis, University of Wyoming, Laramie, WY, August 2002.
This thesis presents a formalization of program transformations and their general categorical framework in Nuprl. It gives formal definitions of catamorphisms and anamorphisms and formal, constructive proofs for when an arrow is a catamorphism or anamorphism. Necessary and sufficient conditions for when a function is a catamorphism are proved constructively, and a program transformation is extracted from the proofs. An instance of Bird's fusion theorem for binary trees is verified in Nuprl, and applied to the Quicksort algorithm to formally prove the algorithm correct.
The theory files were developed with Nuprl Version 4.2. The Nuprl system can be downloaded from http://www.nuprl.org/.
@mastersthesis{weber02program,
author = {Tjark Weber},
title = {Program Transformations in {Nuprl}},
school = {University of Wyoming},
address = {Laramie, WY},
month = aug,
year = {2002}
}