I studied Information Technology with a focus on classical AI at Griffh University in Brisbane as an undergraduate, and wrote my honours thesis on the applications of dependent types to genetic programming. I then moved to Canberra to begin my PhD studies in the field of dependent type theory supervised by Dr Dirk Pattinson and Dr Ranald Clouston. I am a functional programmer by background and a passionate developer in (and very occasionally of) the Idris language.
I am away on a 5 month academic visit to the Laboratory for Foundations of Computer Science at the University of Edinburgh. I'll be returning on campus on the 16th of July but am contactable by email.
I am willing to help arrange (and in some cases be the primary point of contact for) student projects for undergraduate students in computing in the following areas. If you find any of these interesting, please do get in touch.
- Building a Discord bot that offers semantic highlighting for provided Idris code.
- Exploring practical uses of Linear Types to real world programs.
- Implementing a programming language based on Observational Type Theory
My research currently centres around a syntactical and semantic combination, and eventual implementation, of three extensions to Martin-Löf Type Theory: Quantitative Type Theory, Observational Type Theory, and Guarded Dependent Type Theory.
Broad Research Interests
I am broadly interested in expanding the performance, usability, and expressivity of functional programming languages that support dependent types. I'm also interested in the use of dependent types for formal verification of software and the formalisation of type theory.
This then necessitates my research interest in the following sub-fields of computing: Functional Programming, Type Theory, Programming Languages , Category Theory, Intuitionistic Logic, and Deductive Verification.