Programming by example and proving by example using higher-order unification

Abstract

We propose a new approach to programming by example, in which a program is synthesized from examples by higher-order unification in a type theory with a recursion operator. The approach, when applied to the problem of proof generalization, makes it possible to synthesize a general proof from a concrete example proof and establish a method of proving by example. Cases in which a program and a proof are simultaneously synthesized are also considered. In order to represent proofs as terms and generalize proof terms by higher-order unification, we extend Logical Framework to a system with product and equality.