You are here
» People » Mr Donovan CrichtonMr Donovan Crichton
Background
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.
Current Status
I am currently the head tutor for COMP1100/COMP1130 and am otherwise engaged with a variety of teaching-related tasks within the school.
I am working on inductive-recursive formalisations of modal type theories in Idris.
Student Projects
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
- Using Idris as a language workbench for modelling and formalising interesting lambda calculii, with Dr Ranald Clouston.
PhD Topic
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.
