Program Synthesis for Dependently Typed Programs
Master Project of Luka Janjić

Abstract

This thesis investigates the potential of basing a program synthesis system on a de- pendent 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 im- plement a prototype of a search algorithm driven by unsolved constraints typically generated during dependent type checking. We encode a range of synthesis prob- lems 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.

Thesis

https://repository.tudelft.nl/record/uuid:1cdf7a62-d667-4376-a09b-e46c8bff508c