About

I am a Reader in Computer Science at the University of St Andrews, interested in making state of the art programming language techniques accessible to sofware developers and practitioners. This involves type theory, dependently typed functional programming, compilers and metaprogramming. I am currently working on a new implementation of Idris, a dependently typed functional programming language.

When I’m not doing that, you might find me playing Go (I’m about 2 kyu), walking up a hill, watching a game of cricket, or waiting for a delayed train. I’m afraid I also perpetrated the Whitespace programming language.

You can find out how to contact me, or see my publications. Sometimes I give conference talks.

I might also write some posts occasionally, but probably not very often.