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


A framework for program development based on schematic proof

Basin, David A. and Bundy, Alan and Kraan, Ina and Matthews, Seán

MPI-I-93-231. August 1993, 12 pages. | Status: available - back from printing | Next --> Entry | Previous <-- Entry

Abstract in LaTeX format:
Often, calculi for manipulating and reasoning about
programs can be recast as calculi for synthesizing programs. The
difference involves often only a slight shift of perspective:
admitting metavariables into proofs. We propose that such
calculi should be implemented in logical frameworks that support this
kind of proof construction and that such an implementation
can unify program verification and synthesis. Our proposal is
illustrated with a worked example developed in Paulson's Isabelle
system. We also give examples of existent calculi that are closely
related to the methodology we are proposing and others that can be
profitably recast using our approach.
Categories / Keywords: program synthesis, program verification, program transformation, logical frameworks, deductive synthesis, higher-order unification
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-93-231.pdfMPI-I-93-231.pdfMPI-I-93-231.dvi - MPI-I-93-231.dvi
62 KBytes; 114 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 = {Basin, David A. and Bundy, Alan and Kraan, Ina and Matthews, Se{\'a}n},
  TITLE = {A framework for program development based on schematic proof},
  TYPE = {Research Report},
  INSTITUTION = {Max-Planck-Institut f{\"u}r Informatik},
  ADDRESS = {Im Stadtwald, D-66123 Saarbr{\"u}cken, Germany},
  NUMBER = {MPI-I-93-231},
  MONTH = {August},
  YEAR = {1993},
  ISSN = {0946-011X},