Mr Donovan Crichton

PhD Candidate
BIT (Hons, Class 1)
Hanna Neumann Blg (145), 2.13 / 2.27E

Some (possibly) interesting things about me:

  • I am a passionate developer of and in the Idris functional programming language.
  • Vim is my editor of choice.
  • Ubuntu is my operating system of choice (although I will generally embrace any linux OS).
  • I've lived in a few places around NSW and QLD over the years, but Brisbane is the place I've lived the longest.
  • I had a middlingly successful career in accounting and finance before leaving for full time study of a Diploma at TAFE at 29 years old. It's never too late!
  • I put code that I care about here.
  • I put pieces of paper that other people may care about here.


My general research areas of interest are: Functional Programming, Type Theory, Dependent Types, Interactive Theorem Proving, and Functional Programming Languages.
I'm keenly interested in extending the capabilities of my favourite programming language / proof assistant (Idris) in ways that alleviate some of the pain associated with dependently typed programming.
For now, this means I'm looking at extending Idris with type theories that facillitate smoother proofs over coinductive types.

Updated:  10 August 2021/Responsible Officer:  Head of School/Page Contact:  CECS Webmaster