Dependent Type Driven Program Synthesis

by Dr. Edwin Brady

Abstract

Idris is a functional programming language with first-class types, where types may be parameterised by other values. This allows us to give increasingly precise specifications for functions, and be more confident in their correctness. But, perhaps more importantly, it gives the language implementation more information up front about what a function should do. Therefore, we can use Idris as an interactive assistant, and treat programming as a conversation with the machine.

In particular, the Idris system supports program synthesis, generating (fragments of) programs from types. In this talk, I will show the current state of program synthesis in Idris, outline how it works, and discuss some possible future research directions.

Bio

Dr. Edwin Brady is a Lecturer in Computer Science at the University of St Andrews, interested in type theory, dependently typed functional programming, compilers and metaprogramming. He is currently working on a new implementation of Idris, a dependently typed functional programming language. When He is not doing that, you might find him playing Go (He is about 2 kyu), walking up a hill, watching a game of cricket, or waiting for a delayed train.

School of Computer and Cyber Sciences Augusta University