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 Goré 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 I have been mostly working on Isabelle theories for fixed-length words in support of NICTA's L4 MicroKernel Verification project. |
