Dr Jeremy Dawson

College of Engineering & Computer Science
T: 6125 7778

Areas of expertise

  • Mathematical Logic, Set Theory, Lattices And Universal Algebra 010107
  • Computational Logic And Formal Languages 080203
  • Combinatorics And Discrete Mathematics (Excl. Physical Combinatorics) 010104
  • Artificial Intelligence And Image Processing 0801
  • Computation Theory And Mathematics 0802
  • Computer Software 0803


Research interests:
Formal verification; Automated theorem proving, especially in relation to metalogic and cut-elimination, termination of term-rewriting; Functional programming.
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.


Return to top

Updated:  08 May 2021 / Responsible Officer:  Director (Research Services Division) / Page Contact:  Researchers