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.

Formal verification of software is a largely underrepresented discipline in practice. While it is not the most accessible topic, efforts are made to bridge the gap between theory and practice. One tool conceived for this exact purpose is agda2hs, a tool intended to allow developers to create their programs correct-by-design. A program written a proof assistant language Agda, along with the proof of its correctness, can be translated to the readable Haskell equivalent, retaining only the functionally relevant aspects and leaving the proof related aspects of the code behind. This paper describes research done into the current abilities of agda2hs on the use case of verifying properties of free monads, a higher order type with potential for use in implementation of domain specific languages and purely functional and modular handling of effects. In order to represent an aspect of the type in a general way I used containers, a uniform way of representing types that store data. This led me to a limitation of agda2hs: while the tool in its current state can only handle direct translations from a common subset of the two languages, in order to translate my definition of the data type I needed a more fine grained control of the translation process which the tool could not provide.