Jeremy Dawson
Email:
firstnamesurname at gmx.com
Retirement
In retirement I've been doing more of a variety of things, including
 some category theory proofs in Coq
 reverting to my earlier interest in the law, including being rather outspoken
about legal issues and cases that attract my interest, see further
here
Employment (19982021)
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 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.
Topics I have worked on more recently have included
 proving in Isabelle a version of Craig's interpolation theorem
for Display Calculi,
based on work of James Brotherston and Rajeev Goré.
The Isabelle files are here

formalising in Isabelle some aspects of a claimed (and later
contradicted) proof of decidability of ticket entailment.
The Isabelle files are here
 formalising in Isabelle results of Nachum Dershowitz about
wellfounded unions of wellfounded relations.
The Isabelle files are here
(see
tripartite.{thy,ML}
)

formalising in Isabelle results on proof systems for
Full Intuitionistic Linear Logic, based on work with
Alwen Tiu, Ranald Clouston and Rajeev Goré.
The Isabelle files are here
 formalising in HOL4 a dual tableaux calculus of Melvin Fitting
for intuitionistic logic.
The HOL4 files are here

proving in Coq cut admissibility for Dyckhoff's LJT system for
intuitionistic propositional logic (designed to easily show
decidability), and an attempted simpler variation

formalising in Coq the syntactic (ie, by transforming a derivation tree)
proof of cut admissibility for linear logic
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 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://users.cecs.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 Dawson, Nachum Dershowitz, Rajeev Goré,
WellFounded Unions,
In: Automated Reasoning (IJCAR 2018), Oxford, LNCS/LNAI 10900, 117133.
Isabelle source files
(see
tripartite.{thy,ML}
)

Jeremy E. Dawson & Rajeev Goré,
Machinechecked Metatheory of DualTableaux for Intuitionistic Logic,
in Ewa OrÅ‚owska on Relational Methods in Logic and Computer Science,
pp 253282,
Springer series Outstanding Contributions to Logic, 17, 2018
HOL4 source files

Jeremy E. Dawson & Rajeev Goré,
Issues in MachineChecking the Decidability of Implicational Ticket
Entailment.
In: Automated Reasoning with Analytic Tableaux and Related Methods 2017
(Tableaux 2017), LNAI 10501, 347363.
Isabelle source files

Jeremy E. Dawson, James Brotherston & Rajeev Goré,
Machinechecked Interpolation Theorems for Substructural Logics
using Display Calculi
In: International Joint Conference on Automated Reasoning,
Coimbra, Portugal, 2016 (IJCAR 2016), LNCS 9706, 452468.
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)