Michael Norrish

Principal Researcher
Canberra Research Laboratory

A photo of me

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.

Recent work in this area has included collaboration with Gerwin Klein and others in the formal methods and ERTOS areas, looking at the verification of the L4 µ-kernel.

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.

I am a developer of the HOL4 theorem-proving system, maintaining and enhancing this system with Konrad Slind, Mike Gordon and others.

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. 

Contact Information

Postal address:

Michael Norrish
Canberra Research Lab., NICTA
PO Box 8001,
Canberra, ACT 2601


My public e-mail key