Program Synthesis With Types

Program synthesis, the automatic generation of programs from specification, promises to fundamentally change the way that we build software. By using synthesis tools, we can greatly speed up the time it takes to build complex software artifacts as well as construct programs that are automatically correct by virtue of the synthesis process. Studied since the 70s, researchers have applied techniques from many different sub-fields of computer science to solve the program synthesis problem in a variety of domains and contexts. However, one domain that has been less explored than others is the domain of typed, functional programs. This is unfortunate because programs in richly-typed languages like OCaml and Haskell are known for ``writing themselves'' once the programmer gets the types correct. In light of this observation, can we use type theory to build more expressive and efficient type-directed synthesis systems for this domain of programs? This dissertation answers this question in the affirmative by building novel type-theoretic foundations for program synthesis. By using type theory as the basis of study for program synthesis, we are able to build core synthesis calculi for typed, functional programs, analyze the calculi's meta-theoretic properties, and extend these calculi to handle increasingly richer types and language features. In addition to these foundations, we also present an implementation of these synthesis systems, Myth, that demonstrates the effectiveness of program synthesis with types on real-world code.

Author dc:creator

• Osera, Peter-Michael Santos

Advisor dc:contributor.advisor

• Steve Zdancewic

Statement dc:rights

• Peter-Michael Santos Osera

Language dc:language

en

Repository record dc:identifier.uri

https://repository.upenn.edu/handle/20.500.14332/28788

OAI identifier oai:identifier

oai:repository.upenn.edu:20.500.14332/28788