Program synthesis with dependent types

Master thesis (2024)

Authors

L. Janjić Electrical Engineering, Mathematics and Computer Science

Contributors

J.G.H. Cockx Programming Languages - EEMCS (mentor)
S. Dumančić Algorithmics - EEMCS (graduation committee member)
Faculty
Electrical Engineering, Mathematics and Computer Science
More Info
expand_more

Published Date

21-08-2024

Language

English

Reuse Rights

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.

Faculty

Electrical Engineering, Mathematics and Computer Science

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.

Files

MSc_Thesis.pdf
(pdf | 0.307 Mb)