Abstract

Over the last decade I have worked with colleagues on different projects to develop, implement, and automate the use of calculi for program synthesis and transformation. These projects had different motivations and goals and differed too in the kinds of programs synthesized (e.g., functional programs, logic programs, and even circuit descriptions). However, despite their differences they were all based on three simple ideas. First, calculi can be formally derived in a rich enough logic (e.g., higher-order logic). Second, higher-order resolution is the central mechanism used to synthesize programs during proofs of their correctness. And third, synthesis proofs have a predictable form and can be partially or completely automated. In this talk I explain these ideas and illustrate the general methodology employed.

About David Basin

1. A Higher-Order Interpretation of Deductive Tableau.
   Journal of Symbolic Computation, 2001.
2. Program Development Schemata as Derived Rules.
   Journal of Symbolic Computation, 2000.
3. Modeling a Hardware Synthesis Methodology in Isabelle.
   Formal Methods in Systems Design, 1999.
4. Logical Framework Based Program Development.
   ACM Computing Surveys, 1998.
5. Formalization of the Development Process.
   Algebraic Foundations of System Specification, 1988.
6. Middle-Out Reasoning for Logic Program Synthesis.
   Journal of Automated Reasoning, 1996.