Interests
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.
Research
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.
Biography
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.