Type-Directed Synthesis of Products

Abstract

Software synthesis - the process of generating complete, general-purpose programs from specifications - has become a hot research topic in the past few years. For decades the problem was thought to be insurmountable: the search space of possible programs is far too massive to efficiently traverse. Advances in efficient constraint solving have overcome this barrier, enabling a new generation of effective synthesis systems. Most existing systems compile synthesis tasks down to low-level SMT instances, sacrificing high-level semantic information while solving only first-order problems (i.e., filling integer holes). Recent work takes an alternative approach, using the Curry-Howard isomorphism and techniques from automated theorem proving to construct higher-order programs with algebraic datatypes. My thesis involved extending this type-directed synthesis engine to handle product types, which required significant modifications to both the underlying theory and the tool itself. Product types streamline other language features, eliminating variable-arity constructors among other workarounds employed in the original synthesis system. A form of logical conjunction, products are invertible, making it possible to equip the synthesis system with an efficient theorem-proving technique called focusing that eliminates many of the nondeterministic choices inherent in proof search. These theoretical enhancements informed a new version of the type-directed synthesis prototype implementation, which remained performance-competitive with the original synthesizer. A significant advantage of the type-directed synthesis framework is its extensibility; this thesis is a roadmap for future such efforts to increase the expressive power of the system.