Program synthesis is the process of generating a program from specifications. Our approach is using type theory and proof search. Sponsored by Professor Osera.
The Motivation: Since our synthesizer uses enumeration of possible solutions, it experiences an exponential blow up in the search space as program size increases. Implementing restrictions based on types helps reduce the search space, but the increase rate is still exponential.
The Research: Our project is expanding the automated MYTH synthesizer into a semi-automated synthesizer that allows the user to guide the synthesis process, reducing the search space with each choice. We were able to transition from automated to semi-automated this past summer, and are now working on further testing and UI development.
The Tools: emacs, OCaml, GitHub
My role: Research Assistant