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

Problem statement

Program synthesis is a set of techniques for automatically generating programs that satisfy a given high-level specification. However, an important question is where these specifications come from. Often, these specifications come in the form of either test cases or boolean propositions that the final program should satisfy. But a different answer to this question comes from the world of dependently typed programming languages such as Agda and Idris: the specification of the program should be encoded in its type. This brings us to the main question for this thesis: can a program specification in the form of a dependent type signature be used to guide program synthesis to construct a program that satisfies this specification?

Project description

The goal of this project is to explore how techniques from the field of program synthesis could be applied to the task of constructing programs in a dependently typed programming language. Since this is an explorative thesis, we expect a large initial part of the thesis will be dedicated to a survey of existing techniques from both fields. Once you have identified the most promising approaches, the next step in this thesis will be to implement a prototype tool that applies program synthesis to a dependently typed language.

Further reading

• Talk by Edwin Brady: Dependent Type Driven Program Synthesis

Contacts for the project

• Jesper Cockx (TU Delft)