I am currently a PhD student in the Department of Computer and Information Sciences at the University of Strathclyde, where I am a member of the Mathematically Structured Programming Group. Prior to that, I did a BSc in Computer Science, also at Strathclyde.
My PhD is on correct-by-construction model checking for the modal μ-calculus. My broad interests are dependently-typed functional programming languages, constructive logic, and type theory.
I like playing with loopy data types. I write a lot of Agda code.