My BSc degree is in Mathematics, where I specialized in theoretical Computer Science, and my PhD degree is in Computer Science. My PhD thesis was on automated theorem-proving (ATP), a hard and important area within logic and artificial intelligence. After my PhD I was a Lecturer in Computer Science at the University of Essex, moving from there to being a Lecturer in Computer Science at QMW (formerly QMC) in the University of London. I moved to Waikato in January 1994 and am currently a Professor in Computer Science.
Having worked on ATP for my PhD, I continued that work myself, along with
my PhD students, for some years. As time went on I came across other,
connected, topics that were interesting and important and I gradually
expanded my research into theorem-proving which required some
user-interaction and also into non-standard logics which can be used to
support programming. This led to work in the area of constructive
type-theory, which involved a single logical system for specifying and
That work has, more recently, grown into developing a whole new basis
for the formal specification language Z: the work is being done jointly
with Martin Henson from the University of Essex, U.K.
I also have research interests, and a grant funded by the New Zealand government, to do with micro-charts (rather like UML Statecharts). That work is described
You can find much more information about my work (teaching and research) on my personal home page.
You can access a selection of my papers here