Canberra Research Laboratory
My interests are in the following (overlapping) areas:
- Formal methods
The use of mathematics and logic to help in the specification and development of computer hardware and software.
- Interactive theorem-proving
Computer systems that help people prove theorems. These work in a dialogue-like process where the person posits the proof of some theorem, and the computer checks that the proof is valid. While the proof is being developed, the computer can also display intermediate proof-states to help the user know what’s still to be done.
- Formal semantics
Giving formal descriptions to computer languages and systems. My PhD gave such a description for the widely-used language C. More recently, as part of the NICTA project Validating Network Semantics, I worked on a formal description of the TCP/IP protocols (and the associated Sockets API for controlling them) with colleagues at the University of Cambridge.
I am also very interested in the mechanisation of languages with binders. Developing effective techniques for reasoning about syntax that is “quotiented up to α-equivalence” is a fascinating area. Collaborators in this area include René Vestergaard and Christian Urban. See also the POPLmark Challenge.
If you’re a student interested in working in these areas, you might like to consider some of my student project ideas.
Most of my research publications are available online.
Canberra Research Lab., NICTA
PO Box 8001,
Canberra, ACT 2601