Max-Planck-Institut für Informatik
max planck institut
mpii logo Minerva of the Max Planck Society


Recursive program optimization through inductive synthesis proof transformation

Madden, Peter

MPI-I-94-240. September 1994, 44 pages. | Status: available - back from printing | Next --> Entry | Previous <-- Entry

Abstract in LaTeX format:
The research described in this paper involved developing
transformation techniques which increase the efficiency of the
original program, the {\em source}, by transforming its synthesis
proof into one, the {\em target}, which yields a computationally more
efficient algorithm. We describe a working proof transformation
system which, by exploiting the duality between mathematical
induction and recursion, employs the novel strategy of optimizing
recursive programs by transforming inductive proofs. We compare and
contrast this approach with the more traditional approaches to
program transformation, and highlight the benefits of proof
transformation with regards to search, correctness, automatability
and generality.
To appear in the Journal of Automated Reasoning
References to related material:

To download this research report, please select the type of document that fits best your needs.Attachement Size(s):
MPI-I-94-240.pdfMPI-I-94-240.pdf41603 KBytes
Please note: If you don't have a viewer for PostScript on your platform, try to install GhostScript and GhostView
URL to this document:
Hide details for BibTeXBibTeX
  AUTHOR = {Madden, Peter},
  TITLE = {Recursive program optimization through inductive synthesis proof transformation},
  TYPE = {Research Report},
  INSTITUTION = {Max-Planck-Institut f{\"u}r Informatik},
  ADDRESS = {Im Stadtwald, D-66123 Saarbr{\"u}cken, Germany},
  NUMBER = {MPI-I-94-240},
  MONTH = {September},
  YEAR = {1994},
  ISSN = {0946-011X},
  NOTE = {To appear in the Journal of Automated Reasoning},