Jeremy Dawson

formerly Computer Sciences Laboratory
Research School of Information Sciences and Engineering
now Research School of Computer Science
College of Engineering and Computer Science
Australian National University
Canberra   ACT   0200
AUSTRALIA

Email:   firstname-surname at gmx.com

Retirement

In retirement I've been doing more of a variety of things, including

Employment (1998-2021)

For this period of 24 years I was at the Logic and Computation Group in the Research School of Information Sciences and Engineering at the Australian National University, subsequently in the Research School of Computer Science, part of the College of Engineering and Computer Science, see further details below.

I have held positions under various funding sources including ARC Discovery Projects held by Rajeev Goré concerned with verifying cut-admissibility theorems, interpolation theorems and similar meta-logical results.

My earlier research work in computer science was largely about 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.

Topics I have worked on more recently have included

Studies/Thesis (1997)

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.

Earlier employment (up to 1996)

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. At one point I studied law and worked in the office administering the Commonwealth Superannuation Scheme, in the Review and Reconsideration area, handling appeals against the office's decisions.

Projects

L4.verified

For about three years I was actively involved in NICTA's L4.verified project, which used Isabelle to formally verify an operating system microkernel. In that project I was primarily responsible for the library concerning machine words of definite finite lengths and the hardware operations on them, obtaining relevant lemmas and automated proof precedures. See the AVOCS'07 paper listed below.

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://users.cecs.anu.edu.au/~rpg/EVoting

Research Interests

Software

I've written some publicly available and, I hope, useful, software, see here; currently this includes code to create .fig graphics files, as can be produced interactively and displayed by the xfig program.

Publications

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

Journals and Refereed 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, jeremy at rsise anu edu au (with dots)