Associate Professor
School of Computing, Australian National University
Adjunct Professor, S3D, Carnegie Mellon University
Senior Visiting Fellow, Trustworthy Systems, UNSW Sydney
I design programming languages and verification techniques that make software safe, secure, and verifiably trustworthy — across cyber security, trustworthy devices & systems, quantum computing, and software engineering.
My work spans cyber security, trustworthy systems, quantum computing, programming languages, and software engineering
Fiducia is part of a broader toolkit for developing trustworthy embedded systems, providing information flow and liveness guarantees for critical deployments. Built on the Trustworthy Systems seL4 microkernel as a foundation for verified security properties.
fiducia-lang.github.ioA secure general-purpose programming language using object capabilities and effects, developed with Jonathan Aldrich at CMU. Influenced CUE and Scala (see Impact).
wyvernlang.github.ioCapability-based security, authority-safe module systems, and preventing command injection and other attacks through language design. Building secure-by-construction software to defend against real-world cyber threats.
Secure by ConstructionTrustworthy systems security for embedded and space platforms, including consulting for Skykraft and other industry partners. Exploring secure Edge AI deployment on platforms such as NVIDIA Jetson Orin.
Industry ConsultingVerification of quantum programs, including embedding quantum program verification into Dafny and symbolic execution of quantum circuits. Our ESOP 2026 Distinguished Paper validates quantum state preparation programs.
Distinguished Paper AwardPioneered Generic Ownership, showing how type polymorphism provides ownership support. This approach was adopted by the Rust programming language as "lifetime parameters".
Influenced RustProving pre- and post-conditions of reactive systems, correct-by-construction programming approaches, and formal methods for ensuring software correctness.
Formal MethodsEmpirical studies of software development practices, developer tools and productivity, API usability, and evidence-based approaches to improving software quality and developer experience.
Empirical SECurrent postdocs and PhD students. Solid border indicates primary supervisor.
View all current & past students
I am always looking for motivated graduate students to work on programming language design, type systems, software verification, and related areas.
How to Apply ANU PhD ScholarshipsAward-winning and high-impact work across two decades of research
Alex completed his PhD (submitted 2006, conferred 2007) on Generic Ownership, showing how type polymorphism can be used to provide ownership type support in any language. This approach has since been widely adopted by the Rust Programming Language as "lifetime parameters". He went on to demonstrate deep connections between ownership and immutability with the help of the Royal Society of New Zealand Marsden Fund (2008 - 2011), with a book chapter on Immutability outlining the core outcomes of this work.
After a full-year sabbatical at Carnegie Mellon University working with Professor Jonathan Aldrich, Alex created the Wyvern Programming Language - a novel general-purpose language designed from the ground up with security and usability as its primary goals. This produced numerous publications including work on type-specific languages and decidable typing for type members.
Since joining the Australian National University in 2022, Alex's 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 quantum state preparation recognised by an ESOP 2026 Distinguished Paper Award. He is a Permanent Member of IFIP Working Group 2.4, a Senior Visiting Fellow with the Trustworthy Systems group at UNSW Sydney, and leads the School of Computing's GenAI teaching deployment under the ANU–Anthropic partnership.
Alex's ownership type system research directly influenced how the Rust programming language implements its ownership and lifetime system - one of Rust's defining features for memory safety. The well-known "The Performance of Open Source Applications" book cites his research that revolutionised performance evaluations in Talos and similar systems.
The CUE configuration language, used widely within Alibaba's cloud, based its module system on Wyvern's design. Scala drew on our Wyvern research for its path-dependent types and type member mechanisms, and more recently adopted the capabilities-and-effects combination that Wyvern pioneered — see Scala's capture calculus, whose ideas originate in our paper Capabilities: Effects for Free (ICFEM 2018).
Grants and industry funding supporting our research
| Period | Grant | Amount |
|---|---|---|
| 2026 - 2027 | Anthropic Claude API Credits for Teaching at SOCO (shared with Dr Ben Swift) | $500,000 (in-kind) |
| 2026 | ANU CSS Tier 2 Learning & Teaching Grant: “Badges as a Complementary Performance Indicator” (shared with B. Pereira Nunes, A. Chen, B. Swift, B. Bergin, C. Martin, D. Guo, D. Campbell, A. Martin, P. Höfner, R. Shome, F. Muehlboeck, S. Okai-Ugbaje) | $5,000 |
| 2025 - 2026 | Skykraft Industry Research Grant (multiple rounds) | $50,000 |
| 2024 | DVCRI University Strategic Fund towards Centre of Excellence on Trustworthy Systems | $36,000 |
| 2022 | ANU Startup Package Funding | $500,000 |
| 2021 - 2023 | SHEADI Faculty Strategic Initiative PhD Scholarship | $100,000 |
| 2020 - 2021 | Robonomics Network Research Grant | $72,000 |
| 2019 | Kyoto University Visiting Professor Scholarship | $20,000 |
| 2017 - 2018 | Oracle Corporation Research Grant | $70,000 |
| 2013 | Carnegie Mellon University Visiting Researcher Funding (DARPA Lablet) | $25,000 |
| 2012 | Mozilla Foundation Research Grant | $15,000 |
| 2009 - 2011 | Royal Society of NZ Marsden Fast Start Grant | $300,000 |
| 2009 | RSNZ ISAT Grant | $5,420 |
| 2007 - 2016 | VUW University Research Fund (multiple rounds) | $47,000 |
Active leadership roles in the programming languages community
Chair, 2024 - 2026
Member at Large 2024 - 2027, Treasurer since 2025
General Chair, Auckland, NZ
Research Committee Co-Chair
Programme Committee Chair
Permanent Member (invitation-only)
