Bio
My research area is programming languages and software verification. I work on the mathematical principles that define the behaviour of the essential tools that software engineers use to craft all the fantastic technology surrounding us today. My contributions to type systems around ownership, immutability, and capabilities redefined the security guarantees that modern software engineering can provide.
Impact: My work over the first decade of my career involved the concepts of ownership and immutability, and how to provide usable language support for both with the help of type parameters. My approach has now been widely adopted by the Rust programming language as “lifetime parameters”. In the second decade, I worked on the design and production of a usable and secure programming language called Wyvern that utilises object capabilities and effects. A popular configuration language called CUE is used widely within Alibaba’s cloud and service configuration. CUE based its module system design on the Wyvern modules. Wyvern’s ideas on object capabilities and effects have also influenced the Scala programming language’s work on capture checking and effects.
My PhD (submitted 2006, conferred 2007) on Generic Ownership showed how type polymorphism can be used to provide ownership type support in any language. I went on to show deep connections between ownership and immutability with the help of the Royal Society of New Zealand Marsden Funding in 2008 - 2011 with a book chapter on Immutability outlining all the core outcomes of this novel approach.
After a full-year sabbatical at what was then the Institute for Software Research at Carnegie Mellon University, working with Professor Jonathan Aldrich, I have created a novel general-purpose Wyvern Programming Language designed from the ground up with security and usability as its primary goals. Many students and publications came out of that project over the following decade, including novel ideas for type-specific languages and decidable typing for type members - some of which are reflected in the modern generation of the industrial Scala Programming Language.
Since joining the ANU in 2022, my research has centred on trustworthy systems and quantum program verification: the Fiducia language for verified embedded systems building on the seL4 microkernel, and the first embedding of quantum program verification into Dafny (OOPSLA 2025), with follow-on work on validating quantum state preparation recognised by an ESOP 2026 Distinguished Paper Award.
I am a Permanent Member of IFIP Working Group 2.4, a Senior Visiting Fellow with the Trustworthy Systems group at UNSW Sydney, and I lead the School of Computing’s GenAI teaching deployment under the ANU Anthropic partnership.
Degrees
BSc(Hons), PhD, Victoria University of Wellington, New Zealand
Research Interests
Programming Language Design, Software Verification, Trustworthy Systems, Quantum Computing
More Information
Please click here to see the list of my publications, current and former students, as well as my teaching and administrative commitments.