Welcome to my webpage
I work at the University of St Andrews, in the United Kingdom, and I am interested in type theory, proof theory and category theory
My current and past research (2012-2015) has investigated various proof automations for the Idris language (which can also be seen as a proof assistant) and was more generally focused on techniques to improve the usability of dependent types.
I also have a strong interest in the foundations of mathematics and formaly verified mathematics and am currently exploring various things about this (2016-), on which I'm planning to focus after completion of my PhD.
I am also teaching various modules for first, second and third year, which includes lecturing a part of the third year module on Computational Complexity (CS 3052).
My research advisor is Edwin Brady.