- Main
Type-Directed Program Synthesis
- Knoth, Tristan
- Advisor(s): Polikarpova, Nadia
Abstract
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.
Main Content
Enter the password to open this PDF file:
-
-
-
-
-
-
-
-
-
-
-
-
-
-