  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.
