Bio
My research sits at the intersection of programming languages, cybersecurity, formal verification, and quantum computing, with a shared goal of making software safe, secure, and verifiably trustworthy, from embedded microcontrollers to quantum circuits.
Impact: Over the past two decades, my work has found its way into widely used languages and tools. My PhD work on Generic Ownership (submitted 2006, conferred 2007) showed how type polymorphism can provide ownership type support in any language, and directly influenced how the Rust programming language implements lifetime parameters, one of Rust’s defining safety features. With the support of Royal Society of New Zealand Marsden Funding (2008 - 2011), I went on to show deep connections between ownership and immutability, summarised in a book chapter on Immutability. Following a sabbatical year at Carnegie Mellon University, I co-created the Wyvern programming language with Professor Jonathan Aldrich, focusing on object capabilities and secure module systems. Its design informed the module system of the CUE configuration language, now widely used within Alibaba’s cloud infrastructure, as well as Scala 3’s path-dependent types and capture checking.
Since joining the ANU in 2022, my research has centred on trustworthy systems. I am developing Fiducia, a language for secure and trustworthy embedded systems built on the seL4 microkernel, providing information-flow and liveness guarantees for safety-critical deployments. My group’s Rust work continues: view types for partial borrows, formalised in Aeneas, and the verification of concurrent and lock-free data structures with Iris and Verus. In quantum computing, we produced 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 lead a research group of half a dozen research students and postdocs at the ANU. In the programming languages community, I serve as Chair of the SPLASH Steering Committee and as Member at Large and Treasurer of the ACM SIGPLAN Executive Committee. I am a Permanent Member of IFIP Working Group 2.4 and 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, Cybersecurity, Formal 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.