Edwin Brady is a Lecturer in Computer Science at the University of St Andrews in Scotland, UK. His research interests there include programming language design, in particular type systems and domain specific languages. Since 2008, he has been designing and implementing the Idris programming language, a general purpose functional programming language with dependent types, which he uses to implement verified domain specific languages. When he’s not doing that, he’s likely to be playing a game of Go, wrestling with the crossword, or stuck on a train somewhere in Britain.
Dependent types allow us to express a program's behaviour precisely in its type, meaning that type checking is equivalent to formally and mechanically checking a program's correctness. Introductory examples typically involve length preserving operations on lists, or ordering invariants on sorting.
Realistically, though, programming is not so simple: programs interact with users, communicate over networks, manipulate state, deal with erroneous input, and so on. In this talk I will show how advanced type systems allow us to express such interactions precisely, and how they support verification of stateful systems as a result. As an example, I will show how to implement and verify communication protocols in the Idris programming language.