Edwin Brady

Idris implementor, Lecturer at the University of St Andrews

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.

State, Side-effects and Communication in Idris

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.

Video ←Back