Research
Research Interests Formal verification; Automated theorem proving, especially in relation to metalogic and cut-elimination, termination of term-rewriting; Functional programming.
Research Description My current research is directed towards proving the interpolation property for Propositional Dynamic Logic, or establishing that it does not hold. To this end, I have formalised the proof of interpolation for the display calculus for classical propositional logic, and tried (unsuccessfully) to extend this particular proof method to tense logic.
Research Outline Establishing useful properties of various logical systems (sets of logical rules which can be used effectively in proofs)
Biography
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.