Research interests:

Formal verification; Automated theorem proving, especially in relation to metalogic and cut-elimination, termination of term-rewriting; Functional programming.

Duties:

My research work previously at NICTA (and, prior to that, in my position as a Senior Research Associate on an ARC Large Grant held by Dr Rajeev Gore at the ANU) has largely been embedding a display calculus in Isabelle/HOL, and proving, in Isabelle, Belnap's cut-elimination theorem. In the course of work on a stronger result, the strong normalization property of the set of proof reductions used in cut-elimination, we discovered that the published proof of this omits a case, requiring a largely new proof, which we have now completed. We have realised that this proof can be translated into the context of general term-rewriting theory, and have accordingly derived theorems on termination of term-rewriting. Recently I have also mechanised some cut-elimination proofs for sequent calculi. I've been doing other things as well, see the publication list on my homepage. In the last couple of years with NICTA I was mostly working on Isabelle theories for fixed-length words in support of NICTA's L4 MicroKernel Verification project. Since returning to RSISE I first worked on machine-checked proof theory, doing a proof in Isabelle of the cut-elimination result for provability logic. Now I am working with Alwen Tiu on machine-checked proofs for the spi-calculus. Most recently I have formalised bitrace consistency, and proved results making it clear that consistency of an observer theory is decidable. I have also proved results which show, in combination with other published work, that consistency of a bitrace is decidable.

Research opportunities with Dr Jeremy DAWSON

• Verified Vote Counting
• Analysing Voting Schemes Using Logic