Program Synthesis with Dependent Types

Lead Research Organisation: University of Oxford
Department Name: Computer Science

Abstract

Dependently typed languages offer a powerful and elegant way of ensuring strong program correctness properties at compile time, but with current languages it tends to be inconvenient to actually take advantage of this. Even some of the datatypes in Idris's standard library lack proofs of basic correctness properties, for example.
A large part of the difficulty lies in the amount the programmer needs to write in order for a function to match a type sufficiently expressive to describe its intended behaviour, rather than just detailed enough to work. It requires the type containing a detailed specification, the main implementation of the program, and the proof of correctness. The proof would in many cases be quite simple and similar to the reasons the programmer believes the program is correct in the first place, but finding all the relevant lemmas and formatting it in the correct way can be tedious. This difficulty could be reduced by having the compiler produce the proof instead.
Given the unity between programs and proofs in dependent type systems, any sufficiently general method of synthesising proofs would also be capable of synthesising other sorts of functions from their types. The expressiveness of the type system means that any function with the correct type would automatically also have the correct behaviour.
There are many existing approaches to program synthesis in general. Some approaches synthesize a function from a set of input-output examples, restricting the solution to give the correct answer only in those cases, and thus can't prove the correctness of their outputs in general. In the case of synthesising programs from their dependent type signatures, complete semi-algorithms already exist (although a complete algorithm, correctly identifying all those cases where a type is uninhabited, would of course be impossible), but are of limited usefulness due to their very slow running times. There are also many approaches which deal only with restricted classes of problems (e.g. using liquid types, where there is a separate solver for the constraints on functions), are unable to use some sorts of proof (e.g. being unable to generate inductive hypotheses not directly related to the goal), or rely heavily on specific forms of common hypotheses. I don't yet know whether I will end up also solving only some restricted case, but I intend to avoid it if possible.
I hope that the development of languages with useful formal verification built in will help to reduce the incidence of certain types of bug. I will be considering other ways of improving the usability of dependently typed languages other than program synthesis as well, but this seems like one potentially promising direction.
This project falls within the EPSRC's "Programming languages & compilers" and "Verification and correctness" research areas.

Publications

10 25 50

Studentship Projects

Project Reference Relationship Related To Start End Student Name
EP/N509711/1 01/10/2016 30/09/2021
2219011 Studentship EP/N509711/1 01/10/2019 31/03/2023 Andrew Kenyon-Roberts
EP/R513295/1 01/10/2018 30/09/2023
2219011 Studentship EP/R513295/1 01/10/2019 31/03/2023 Andrew Kenyon-Roberts