The next 700 synthesis calculi

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 the talk I explain these ideas and illustrate the general methodology employed.