Jeremy Dawson
Email:
firstname.surname at rsise.anu.edu.au
Phone:
+61 (0)2 6125 7778
Fax:
+61 (0)2 6125 8651
Employment (1998current)
For most of the past 13 years I have been at the
Logic and Computation Group in the
Research School of Information Sciences and Engineering
at the
Australian National University, see further details below.
My current position is on an ARC Discovery Project held by
Rajeev Goré
concerned with verifying cutadmissibility theorems, interpolation
theorems and similar metalogical results.
My earlier research work in computer science
was largely about embedding a display
calculus in Isabelle/HOL, and proving, in Isabelle, Belnap's
cutelimination theorem. In the course of work on a stronger result,
the strong normalization property of the set of proof reductions used
in cutelimination, 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 termrewriting theory, and have accordingly derived
theorems on termination of termrewriting.
The Isabelle files are here.
In late 2010 I extended and adapted some of the Isabelle proofs to prove
a version of Craig's interpolation theorem for Display Calculi,
based on work of James Brotherston and Rajeev Goré.
The Isabelle files are here.
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.
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 votecounting 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
 Formal verification
 Automated theorem proving, especially in relation to
 metalogic and cutelimination
 termination of termrewriting
 Functional programming
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
SpringerVerlag.
A more detailed CV is also here.
Journals and Refereed Conferences

Jeremy E. Dawson, James Brotherston & Rajeev Goré,
Machinechecked Interpolation Theorems for Substructural Logics
using Display Calculi
Isabelle source files

Jeremy E. Dawson, Rajeev Goré & Jesse Wu,
MachineChecked ProofTheory for Propositional Modal Logics
In: Progress Computer Science(Birkhäuser), Vol. 28, Reinhard Kahle et al.
(Eds): Advances in Proof Theory, Chapter 5
Isabelle source files
link to publisher's site

Jeremy E. Dawson, Rajeev Goré, Thomas Meumann:
MachineChecked Reasoning About
Complex Voting Schemes Using HigherOrder Logic.
In Proc. EVoting and Identity  5th International Conference, VoteID 2015,
Bern, Switzerland, September 24, 2015.

Jeremy E. Dawson, Ranald Clouston, Rajeev Goré & Alwen Tiu,
From Display Calculi to Deep Nested Sequent Calculi: Formalised for Full
Intuitionistic Linear Logic.
In Proc. TCS 2014: Theoretical Computer Science, LNCS 8705, 250264.
Isabelle source files

Ranald Clouston, Jeremy E. Dawson, Rajeev Goré & Alwen Tiu,
AnnotationFree Sequent Calculi for Full Intuitionistic Linear Logic.
In Proc. CSL 2013: European Conferences on Computer Science Logics,
Schloss Dagstuhl  LeibnizZentrum für Informatik, LIPIcs, 23:197214.
Isabelle source files

Jeremy E. Dawson & Rajeev Goré,
Generic Methods
for Formalising Sequent Calculi Applied to Provability Logic.
In Logic for Programming, Artificial Intelligence and Reasoning (LPAR 2010),
LNCS 6397, 263277.
Isabelle source files

Alwen Tiu, Rajeev Goré & Jeremy Dawson,
A Proof Theoretic Analysis of Intruder Theories.
Logical Methods in Computer Science 6 (3:12), 2010, 137.
http://arxiv.org/pdf/1005.4508
details of Isabelle proofs 
Isabelle source files

Alwen Tiu & Jeremy E. Dawson,
Automating Open Bisimulation Checking for the Spi Calculus.
In Computer Security Foundations Symposium (CSF 2010), 307321.
Isabelle source files

Jeremy E. Dawson & Alwen Tiu
Formalising Observer Theory for EnvironmentSensitive Bisimulation
In 22nd International Conference on Theorem Proving in Higher Order Logics,
Munich, August 2009 (TPHOLs 2009),
LNCS 5674, 244259.
Isabelle source files

Jeremy E. Dawson & Rajeev Goré,
Termination of Abstract Reduction Systems
International Journal of Foundations of Computer Science 20 (2009), 5782.
(contains material from CATS 2007 and CSL 2004 papers).

Jeremy E. Dawson,
Isabelle Theories for Machine Words
In Seventh International Workshop
on Automated Verification
of Critical Systems (AVOCS'07),
Oxford, September 2007,
Electronic Notes in Theoretical Computer Science,
250 (2009), pp. 5570, Elsevier.

Jeremy E. Dawson,
Compound Monads in Specification Languages
In Proceedings of
Programming Languages meets Program Verification (PLPV) 2007,
Freiburg, October 2007, ACM, 2007, 310.
Isabelle source files (monads)
(modelling computations)

Jeremy E. Dawson,
Formalising Generalised Substitutions
In 20th International Conference on Theorem Proving in Higher Order Logics,
Kaiserslautern, September 2007 (TPHOLs 2007),
LNCS 4732, 5469.
Isabelle source files

Jeremy E. Dawson & Rajeev Goré,
Termination of Abstract Reduction Systems
Computing: The Australasian Theory Symposium, 2007 (CATS 2007),
Conferences in Research and Practice in Information Technology (CRPIT), Vol.
65, 3543
Isabelle source files

Jeremy E. Dawson & Rajeev Goré,
A General Theorem on Termination of Rewriting
Computer Science Logic (CSL'04), LNCS 3210, 100114.
Isabelle source files
more Isabelle source files

Jeremy E. Dawson,
Formalising General Correctness
Computing: The Australasian Theory Symposium, 2004,
Electronic Notes in Theoretical Computer Science 91, 4665, Elsevier.
Isabelle source files
 Jeremy E. Dawson & Rajeev Goré,
A New Machinechecked Proof of Strong Normalisation for Display Logic,
Computing: The Australasian Theory Symposium, 2003, Electronic Notes in
Theoretical Computer Science 78, 1635, Elsevier.
Isabelle source files

Jeremy E. Dawson & Rajeev Goré,
Machinechecking the Timed Interval Calculus,
15th Australian Joint Conference on Artificial Intelligence (AI'02),
LNCS 2557, 95106,
Isabelle source files

Jeremy E. Dawson & Rajeev Goré,
Formalised Cut Admissibility for Display Logic
15th International Conference on Theorem Proving in Higher Order Logics
(TPHOLs 2002), LNCS 2410, 131147.
Isabelle source files

Jeremy E. Dawson & Rajeev Goré,
Embedding Display Calculi into Logical Frameworks :
Comparing Twelf and Isabelle,
Computing: The Australasian Theory Symposium, 2001,
Electronic Notes in Theoretical Computer Science, Elsevier, volume 42.

Jeremy E. Dawson & Rajeev Goré,
A Mechanisation of Classical Modal Tense Logics Using Isabelle,
Proceedings of the 11th Australian Joint Conference on Artificial Intelligence,
LNCS 1502 (1998), 107118.
Isabelle source files

Jeremy E. Dawson & Rajeev Goré,
A Mechanised Proof System for Relation Algebra using Display Logic,
Proceedings of the 6th European Workshop on Logics in Artificial Intelligence,
LNCS 1489 (1998), 264278.
Isabelle source files
Workshops

Jeremy E. Dawson,
Formalising General Correctness,
In Theorem Proving in Higher Order Logics, NASA/CP2002211736, 3647.
Isabelle source files

Jeremy E. Dawson & Matt Fairtlough,
Automatic Constraint Calculation using Lax Logic,
In Theorem Proving in Higher Order Logics, NASA/CP2002211736, 4859.

Jeremy E. Dawson,
Simulating TermRewriting in LPF and in Display Logic,
Theorem Proving in Higher Order Logics: Emerging Trends
(supplementary proceedings of TPHOLs'98), TRCS9808,
Australian National University, 4762.
(later version),
Isabelle source files for
LPF 
Display Logic
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)