You are here
» People » Mr Donovan CrichtonMr Donovan Crichton
Bldg N44 Technology, Room 2.02.
Griffith University, Nathan Campus, Nathan, Brisbane, QLD.
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 visiting Griffith University's Nathan Campus in Brisbane, and return on-campus to ANU four weeks a year.
This is usually:
1 week in April.
1 week in September.
2 weeks in December.
Research
For my PhD i am investigating inductive-recursive formalisation of modal type theories in Idris. In particular I am interested in Quantitative Type Theory, Observational Type Theory, and Guarded Dependent Type Theory.
More broadly, I am interested in improving the state of the art of dependent-typed pure functional programming languages and applying dependent-typed proof mechanisation techniques to support real world programming.
I have tangential interests in Functional Programming, Category Theory, Programming Language Implementation, and Non-Dependent Type Theories.
- 2023 S1: COMP1100/1130 - Head Tutor.
- 2022 S2: COMP1100 - Associate Lecturer / Co-convenor.
- 2021 S1: COMP1100/1130 - Tutor.
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.
Scholarships
- 2021: University of Edinburgh LFCS Visiting Research Internship (6 months).
- 2021: Recipient of an ASD Co-Lab Scholarship (3 years).
- 2020: Recipient of an ANU University Research Scholarship (3 years).
- OOPSLA 2024 - Served on the artefact evaluation committee.
- PLDI 2023 - Served on the artefact evaluation committee.
