A framework for program development based on schematic proof
- 30 December 2002
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
Abstract
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. The proposal is illustrated with a worked example developed in L.C. Paulson's (1990) 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 the approach. Author(s) Basin, D. Max-Planck-Inst. fur Inf., Saarbrucken, Germany Bundy, A. ; Kraan, I. ; Matthews, S.Keywords
This publication has 12 references indexed in Scilit:
- Specifying theorem provers in a higher-order logic programming languagePublished by Springer Nature ,2005
- On computational open-endedness in Martin-Lof's type theoryPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Logic Program Synthesis via Proof PlanningPublished by Springer Nature ,1993
- Tutorial notes: Reasoning about logic programsLecture Notes in Computer Science, 1992
- Logic programming in the LF logical frameworkPublished by Cambridge University Press (CUP) ,1991
- Tactical theorem proving in program verificationPublished by Springer Nature ,1990
- The OYSTER-CLAM systemPublished by Springer Nature ,1990
- The calculus of constructionsInformation and Computation, 1988
- Making prolog more expressiveThe Journal of Logic Programming, 1984
- A Transformation System for Developing Recursive ProgramsJournal of the ACM, 1977