Program development by proof transformation
Ulrich Berger and Helmut Schwichtenberg

Abstract
The paper compares two methods of extracting programs from classical proof: A "direct" method based on an analysis of normal natural deduction proofs, and a method based on Gödel's negative transalation and Friedman's A-translation. Furthermore, Goad's pruning of proofs is applied to simplify proofs and their extracted programs.

Bib entry

@InProceedings{BergerSchwichtenberg95d,
  author = 	 "Ulrich Berger and Helmut Schwichtenberg",
  title = 	 "Program Development by Proof Transformation ",
  editor =	 "H. Schwichtenberg",
  volume =	 "139",
  series =	 "Series F: Computer and Systems Sciences",
  pages =	 "1--45",
  booktitle =	 "Proof and Computation",
  year =	 "1995",
  organization = "NATO Advanced Study Institute, International
		  Summer School held in Marktoberdorf, Germany, 
                  July 20 -- August 1, 1993",
  publisher =	 "Springer-Verlag"}

Draft copy