Michael Norrish
Senior Researcher
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.
Current work in this area includes 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 HOL 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.