UC San Diego

Program synthesis tools promise the ability to automate programming, generating executable code from a high-level specification. This dissertation presents work intended to help bring synthesis to more realistic programming problems. First, we consider the problem of resource-guided synthesis: we design a resource analysis enabling the implementation of the first synthesizer capable of reasoning about program efficiency. This approach to resource analysis is automatic and highly expressive, subsuming a number of existing techniques as well as automating the verification of bounds that previously would have required manual proofs. Second, we present a framework for the more general problem of implementing a synthesizer for an arbitrary type system. Our framework facilitates experimentation with new search strategies or specification styles, paving the way towards more expressive and efficient synthesis tools.