Edwin Brady

Creator of the Idris programming language

Edwin is Lecturer in Computer Science at the University of St Andrews in Scotland, interested in type-driven development, domain-specific languages and reasoning about effectful programs. When he's not doing that, he might be playing Go, watching cricket, or wandering around Scotland's hills.

Secrets of type-driven program synthesis

Idris is a functional programming language with first-class types, where types may be parameterised by other values. This gives the language implementation a lot of information up front about what a function should do, which means we can use Idris is our interactive assistant, where we write programs by conversation with the machine.  As part of this, we are actively developing program synthesis tools, which generate fragments of programs from types. This can appear like magic! However, the key ideas are surprisingly simple. In this talk, I will demonstrate the current state of program synthesis and Idris, and try to demystify how it works, as well as discuss some related work and possible future research directions.

Slides
←Back