Interests
My main interests are in Gentzen systems for various logics, particularly modal logics and temporal logics. Currently I am working on the intricacies of Display Logic and how to obtain Gentzen systems for hybrid logics like intuitionistic modal logic. With Jeremy Dawson, I am working on formalising proofs of weak and strong normalisation for various calculi in the logical framework Isabelle. With Vaughan Coulthard, Jen Davoren and Thomas Moor I am working on inventing bi-modal tense logics with applications in hybrid systems. I am also interested in software engineering and security aspects of Java applications, particularly for JavaCards.
Research
Electronic Voting and Vote-Counting, Proof Methods for Non-classical Logics, Term Rewriting, Interactive Theorem Proving, Automated Reasoning, Logic
Biography
I obtained my PhD from the Computer Laboratory of the University of Cambridge in 1992. Before that I completed my BSc (hons) and MSc at the Unviversity of Melbourne.