Jeremy Dawson

NICTA
Research School of Information Sciences and Engineering
Australian National University
Canberra   ACT   0200
AUSTRALIA

Email:   firstname.surname at rsise.anu.edu.au, or
  firstname.surname at nicta.com.au

Phone:   +61 (0)2 6125 8606

Fax:   +61 (0)2 6125 8651

Employment

I am currently (since Feb 2003) a Postdoctoral Fellow in the Logic and Computation programme of NICTA but work and am physically located in the Automated Reasoning Group in the Computer Sciences Laboratory in the Research School of Information Sciences and Engineering at the Australian National University

My research work here (and in my previous position as a Senior Research Associate on an ARC Large Grant held by Dr Rajeev Goré) 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. The Isabelle files are here.

We have realized that this proof can be translated into the context of general term-rewriting theory, and have accordingly derived theorems on termination of term-rewriting. The Isabelle files are here.

Recently I have also mechanised some cut-elimination proofs for sequent calculi. I've been doing other things as well, see the publication list below.

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.

Previous employment

I have previously worked (among others) in CSIRO Division of Mathematics and Statistics (doing statistical analyses and research in combinatorial mathematics, particularly matroid theory), and in the Department of Defence, doing Computer Security, where I became interested in the formal verification of software.

Studies/Thesis

In 1997 I did the Graduate Diploma in Computer Science. My honours thesis, Mechanised Proof Systems for Relation Algebras, was on automating display logic in Isabelle; my supervisor was Rajeev Goré of the Automated Reasoning Group. In 1998 and late 1999 I did some further work along these lines, see the papers below.

Here are copies of my thesis, in ps.gz, dvi.gz, and here are the source code files referred to in it.

Projects

L4.verified

EVACS

In 2001, I wrote a prototype vote-counting program for the complex proportional representation system used in electing the ACT Assembly. Recently the requirements of the system have been encoded in the language of the HOL theorem proving system and I am engaged in similarly encoding the actions of my program, with a view to formally proving that it correctly meets its requirements. Further information on this is at http://web.rsise.anu.edu.au/~rpg/EVoting

Research Interests

Publications

A list of publications is here; some online ones follow - note that copyrights to some are held by publishers, including Springer-Verlag

Conferences

Workshops

Technical reports, etc

Other

Ranked =17th in 1998 International Functional Programming Contest, see table of results

Finalist in 1999 International Functional Programming Contest, see report

Jeremy Dawson