invited talk: The next 700 synthesis calculi
July 24th 09:00-10:00 in auditorium 2
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.Selected
A Higher-Order Interpretation of Deductive Tableau.
Journal of Symbolic Computation, 2001.
Program Development Schemata as Derived Rules.
Journal of Symbolic Computation, 2000.
Modeling a Hardware Synthesis Methodology in Isabelle.
Formal Methods in Systems Design, 1999.
Logical Framework Based Program Development.
ACM Computing Surveys, 1998.
Formalization of the Development Process.
Algebraic Foundations of System Specification, 1988.
Middle-Out Reasoning for Logic Program Synthesis.
Journal of Automated Reasoning, 1996.