Links to other websites

Welcome to my webpage



About me


I work at the University of St Andrews, in the United Kingdom, and I am essentially interested in software correctness, programming languages and type theory.


I want to make software more reliable and less prone to bugs, and that's why I love to develop new languages and formal systems that enable programmers to be more rigorous. I believe types should play a central role in software development, and more precisely that the programming activity should be driven by the types.


My current research is on the application of formal methods to real (industrial) problems, and in the design of safe programming languages and logical frameworks that will be adapted for the everyday programming.


My 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.


I am teaching various modules for first, second and third year, which includes lecturing a part of the third year module on Computational Complexity (CS 3052).


I am a reviewer of the Journal of Functional Programming.