Program synthesis with dependent types
L. Janjić (TU Delft - Electrical Engineering, Mathematics and Computer Science)
Jesper Cockx (TU Delft - Programming Languages)
More Info
expand_more
Other than for strictly personal use, it is not permitted to download, forward or distribute the text or part of it, without the consent of the author(s) and/or copyright holder(s), unless the work is under an open content license such as Creative Commons.
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.