Edwin Brady
Creator of the Idris programming language; Lecturer
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.
Past Activities
Code Mesh V
17.10 - 18.10
Panel discussion: Types for All: From weak to strong, from static to dynamic
When working from home, everyone looked at what books were on display on the shelves in the background. Type systems seemed to be very much in vogue, often put there to be seen. In order to not loose momentum, we are planning a panel on Type Systems at Code Mesh! It will be lead by Felienne Hermans of Leiden University.
The idea is to discuss the panelists' approach to type systems, the rationale behind their design decisions, and how they have benefited the programming languages they have created. Questions will include, but not be limited to: when do we want type, when are types in the way, and what can we do about that? How extensible should a type system be? Attendees, through the Q&A section of the app, will be able to ask their own questions. With cameras on, don't forget to put your books on display.
Code Mesh V
17.30 - 18.10
Dependent Type Driven Program Synthesis in Idris
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.
Code Mesh LDN 2018
15.25 - 16.10
Idris 2: Type-driven development of Idris
We've had lots of fun over the last couple of years investigating the possibilities and limitations of type-driven development in Idris.
As we write larger programs, though, we're finding the implementation of Idris is showing the strain - such is the nature of "research quality software." Edwin recently decided the time was right to start again and implement Idris 2 in Idris.
In this talk, Edwin will give an introduction to type-driven development (in Idris 2) and report on progress so far, showing off the most interesting features which the new design enables (notably, linear types and better type inference).