Jeremy Dawson

formerly Computer Sciences Laboratory
now School of Computer Science
Research School of Information Sciences and Engineering
College of Engineering and Computer Science
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 a Research Fellow in the Logic and Computation Group Research School of Information Sciences and Engineering at the Australian National University

At present I am working on an ARC Discovery Project held by Alwen Tiu concerned with formalising results in 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. Further details are here. The Isabelle files are here.

In the middle of 2008 I mechanised a proof of cut-admissibility for the provability logic GLS, following a paper of Goré and Ramanayake. The Isabelle files are here.

My research work here over recent years 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 then 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.

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