Michael Norrish

Associate Professor, Computing Foundations Lead, and BAC Convenor


My interests lie in the intersection between interactive theorem-proving, real-world computer systems (particularly in the domain of programming languages), and mechanised mathematics.

  • Interactive theorem-proving: ITP systems are also known as proof assistants, and that’s what they hope to do: help humans prove important theorems. My interests here cover both implementing such systems and using them in various application areas.

  • Programming Language Semantics: programming languages underpin computer systems: they are fundamentally how people tell computers what to do, and (perhaps) how to do it. These languages necessarily have semantics just as do human languages. To my mind, the task of figuring out exactly what programming languages mean is both fascinating and important: the human needs to know what a program is supposed to do if they are to express themselves at all using the programming language; the computer needs to know what the human means by a particular piece of program text in order to correctly turn it into a behaviour.

  • Mechanised Mathematics: this is the task of using an ITP to prove theorems drawn from mathematics. This is not just fun in its own right, but can also be critically important if the theorem underpins some piece of computer code.


My current research centres around:

  • The HOL4 system; I am this ITP’s primary developer; and
  • The CakeML project, a verified compiler for a functional programming language rather similar to SML (and OCaml).

My Google Scholar page gives a good picture of what I have done to date in my research career.


I received my PhD (C Formalised in HOL) in 1999 from the University of Cambridge, and was an undergraduate at Victoria University of Wellington.

Getting in Touch

My ANU e-mail address is your best bet. Raising issues on the github pages associated with my research projects will also work. I am also trying out Mastodon, where I am @michaeln@mastodon.sdf.org.

You are on Aboriginal land.

The Australian National University acknowledges, celebrates and pays our respects to the Ngunnawal and Ngambri people of the Canberra region and to all First Nations Australians on whose traditional lands we meet and work, and whose cultures are among the oldest continuing cultures in human history.

bars search times arrow-up