Program Synthesis with Dependent Types

Luka Janjić

This thesis investigates the potential of basing a program synthesis system on a dependent type theory. This is an attractive research direction because it allows a very flexible range of specification to be expressed within the same framework. We implement a prototype of a search algorithm driven by unsolved constraints typically generated during dependent type checking. We encode a range of synthesis problems from literature in our system, showcasing how it can be used for expressing the specification and synthesizing programs that manipulate data. We empirically establish the effect of constraint-directed aspect of our approach on performance, based on the encoded problems.

---

Previous: Jaro Reinders | Higher Order Patterns for Rewrite Rules
Next: | Towards Modular Language Semantics of WebDSL: A Case Study of Using Algebraic Effects in Haskell for Language Specification