Jeremy Edward DAWSON
Curriculum Vitae
Born 29 June 1952, Sydney, N.S.W., Australia.
Married, with 2 children.
Australian citizenship.
Address : 36 Bateman St, Kambah, ACT 2902, Australia.
(phone 0262312102)
Email : jeremy@rsise.anu.edu.au

 Ph.D.
 in Pure Mathematics (combinatorial mathematics),
University of Sheffield, Jan 1976  Jun 1978 (parttime from Oct 1977).
My thesis was in combinatorial mathematics (matroid theory).
 M.Sc.
 in Pure Mathematics, University of Sydney,
Jan  Nov 1975.
 B.Sc.
 (primarily Mathematics and Statistics),
with 1st class Honours (shared University medal)
in Pure Mathematics, University of Sydney, Mar 1970  Nov 1973.
 Grad. Dip. Sci.
 in Computer Science,
with Distinction (shared Computer Science prize),
Australian National University, Feb  Nov 1997.
(Note  the ANU Graduate Diploma is roughly equivalent to an Honours year,
result gained was equivalent to firstclass Honours).
My project involved automating the Display Logic proof
system for abstract relation algebras in Isabelle, and
related theoretical work.
 Diploma in Law
 Barristers' Admission Board of
N.S.W., May 1984  Sep 1988 (parttime).
 part of M.Eng.Sc
 in Operations Research,
University of N.S.W., Feb  Nov 1974 (parttime, subjects taken
amounted to 33% of whole degree).
 part of M.Sc
 in Applied Statistics,
Australian National University, Feb  Jun 1980 (parttime, subjects taken
amounted to 37% of whole degree).

 February 2012  current:
 Research Fellow, Automated Reasoning Group,
Research School of Information Sciences and
Engineering, Australian National University.
I worked on a ARC Grant held by Rajeev Goré,
working on interpolation for display calculi,
developing and implementing proofs in this area
in the Isabelle theorem prover.
 July 2010  December 2011 :
 Casual/sessional lecturer/tutor, Australian National University.

In second semester 2011 I did 70% of the teaching of a semesterlong
second year undergraduate course, ``Formal Methods in Software Engineering'',
COMP2600, in the Department of Computer Science, ANU.
I also conducted tutorials in mathematics (MATH1014, first year)
and in the Computer Science course "Algorithms" (COMP3600, third year).

In first semester 2011 I conducted tutorials in mathematics
(MATH1013, first year) and logic (COMP2620, second year),
and practical classes in programming (COMP1100, first year).

In second semester 2010 I did 50% of the teaching of a semesterlong
second year undergraduate course, ``Formal Methods in Software Engineering'',
COMP2600, in the Department of Computer Science, ANU.
 November 2010  December 2010 :
 In a temporary position with the Automated Reasoning Group
I worked on adapting my previous mechanised proofs about Display Logic to
prove results concerning Interpolation in Display Logic.
 September 2008  August 2010 :
 Research Fellow, Automated Reasoning Group,
Research School of Information Sciences and
Engineering, Australian National University.
I worked on a ARC Grant held by Alwen Tiu,
'Proof theoretical methods for reasoning about process equivalence'.
In this position I worked on bisimulation in the Spicalculus,
developing and implementing proofs in this area
in the Isabelle theorem prover.
During this period I also used a recent development of the HOL theorem prover
to prove category theoretic results about compound monads.
 May  August 2008 :
 Fellow, Automated Reasoning Group,
Research School of Information Sciences and
Engineering, Australian National University.
I studied cutelimination for sequent systems, and implemented proofs of these
in the Isabelle theorem prover.
 Feb 2003  April 2008 :
 Researcher, Logic and Computation programme, NICTA
(National ICT Australia Ltd).
I continued research in the areas described below, and also
 I worked on proofs of termination of rewrite systems, writing research
papers whose results have been verified in the Isabelle theorem prover.
 I have joined a NICTA project "L4.verified" to produce
an operating system microkernel verified in Isabelle,
and I have developed theories and enhancements for
Isabelle as required for the project.
In particular I have developed Isabelle theories for words (bitstrings)
of fixed but arbitrary lengths.
In 2006 and 2007 I did 50% of the teaching of a semesterlong
undergraduate course, ``Formal Methods in Software Engineering'',
in the Department of Computer Science, ANU.
 Feb 2000  Jan 2003 :
 Senior Research Associate,
Automated Reasoning Group, Research School of Information Sciences and
Engineering, Australian National University.
I worked on a ARC Grant held by Rajeev Goré.
In this position
 I implemented a Display Calculus in Isabelle/HOL,
including the proof of the cutelimination theorem;
in implementing the published proof of the strong normalisation theorem,
I discovered a bug, and found and implemented a new proof.
 I investigated the use of Lax Logic for use in automatically generating
timing constraints as part of hardware verification.
 I used the theorem prover Isabelle to model and prove theorems about
the Timed Interval Calculus, and about the "general correctness" approach to
program semantics.
 I worked on a commercial project to automate the votecounting in
ACT Government elections (using the complex HareClark
proportional representation voting system), writing a prototype system in
Standard ML.
 I taught a unit of the Automated Reasoning Group's
Logic Summer School, and
did some casual lecturing on logic programming and its semantics.
 Jan 1999  Jan 2000 :
 Research Scientist, ANUTECH
(in Department of Computer Science),
Australian National University.
Duties  software development for parallel computers,
This included
 rewriting software which partitioned a sparse matrix,
according to its zero/nonzero structure, into parts which would be worked on
in separate processors,
for the purpose of implementing linear algebra algorithms, and
 writing code to speed up the transfer of messages between
processors on a MIMD parallel machine
I also conducted tutorial classes for a 3rd year Algorithms course.
 Jan 1998  Jan 1999 :
 Associate Lecturer, Department of Computer Science and Automated Reasoning
Project, Australian National University.
In this position I
 implemented part of the semantics of the Java Virtual
Machine in the HOL theorem proving system,
 implemented the Display Logic formulation of some substructural logics in
the Isabelle theorem prover,
 taught a 3rdyear course, Formal Languages, Computability and
Complexity,
 handled tutorial/lab groups for courses in
Functional and Logic Programming (3rd year) and
Compiler Construction (2nd year)
 Jan 1986  Dec 1997 :
 Australian Public Service, in the following positions

 Apr 1995  Dec 1997 :
 Senior Research Scientist, Trusted Computer Systems Group,
Defence Science and Technology Organization.
I managed a group doing research into and development of
technologies for computer security evaluation, particularly formal
verification of software (using Isabelle and ML).
 Dec 1988  Apr 1995 :
 Senior Information Technology Officer Grades C and B,
Computer Security Section, Department of Defence.
I was in the computer security evaluation area,
where I advised on and evaluated trusted (secure)
computer systems (US TCSEC and EC ITSEC evaluations),
especially high assurance systems.
This work involved planning and examining computerbased
systems to ensure that they satisified their security requirements.
It included examining the design and development techniques
(ie the software engineering practices) used,
and sometimes involved formal specification and verification.
I also experimented with theorem prover design,
developing of prototype tool (C, Unix).
 Aug 1986  Nov 1988 :
 Administrative Service Officer Grades 5 and 6, Australian Government
Retirement Benefits Office.
Duties  reconsideration of Office decisions
and assisting in AAT appeals
concerning superannuation entitlements.
 Jan 1986  Aug 1986 :
 Computer Systems Officer Grade 2,
Application Software Section, Australian Bureau of Statistics.
Duties  programming (PL/1 on Fujitsu mainframe), planning changes to
structures in data dictionary.
 Sep 1984  Jan 1986 :
 Programmer Grade 2, Dept of Physiology,
Australian National University.
Duties  system management, programming (C, Unix), assisting research staff in
computing and mathematical matters.
 Dec 1978  Sep 1984 :
 Research Scientist, Dept of Mathematics and Statistics, CSIRO.
Duties  mathematical research (combinatorial mathematics),
planning and statistical analysis of agricultural and other experiments,
programming for research projects (Fortran, Pascal, Unix).
 Jun 1982  Jun 1983 :
 (while on leave from CSIRO)
Teaching Fellow, Dept of Mathematics, National University of Singapore.
Duties  lecturing and tutoring in mathematics;
I lectured 3rd year Combinatorial
Mathematics and took 1st year Engineering Mathematics
tutorial classes.
 Mar  Jun 1980 (parttime) :
 Casual lecturing, Dept of Mathematics,
Australian National University;
I lectured 3rd year Combinatorial Mathematics.
 Oct 1977  Sep 1978 :
 Lecturer, Dept of Pure Mathematics, University of Glasgow.
Duties  lecturing and tutoring in mathematics;
I lectured 1st year Algebra and 1st year Analysis,
and took 1st and 2nd year problem classes.
 Feb 1974  Jan 1975 :
 Professional Officer Grade 1, Dept of Industrial Engineering,
University of N.S.W.
Duties  assisting with Operations Research research projects, programming
(PL/1 on IBM OS/360).
Feb  Oct 2001 
Electronic Voting and Counting 
Software Improvements Pty Ltd 
$8000 
Feb 2001  May 2002 
Hardware Verification using Lax Logic 
University of Sheffield 
$40000 
My Ph.D. thesis and much of my subsequent research were in
combinatorial mathematics, especially matroid theory.
This included some work on efficient algorithms for matroids.
My work in Defence computer security evaluation led to an interest in the
formal verification of the correctness of computer programs
(both hardware and software).
Through this work I became interested in the formal verification of
software and hardware, the automated reasoning necessary for any
nontrivial verification activity, and automated proof tools
(such as Isabelle and HOL).
I have considerable experience using the computerbased theorem
provers Isabelle and HOL, most recently with Isabelle.
Arising out of this interest and experience,
I did a Graduate Diploma project in 1997,
in which I automated the Display Logic proof
system for abstract relation algebras in Isabelle, and
explored the relationship between it and other proof systems.
Since then my research in logic has been related to this interest, and has
included the following work.
 implementing the Display Calculus (sequent calculus)
for abstract relation algebras as an Isabelle theory
 developing relevant tactics to facilitate derivations
 looking at alternative proof systems, and examining how their
axioms and proof methods can be reproduced in the Display Logic calculus
 implementing in Isabelle a proof of Belnap's cutelimination
theorem, for the relation algebra Display Calculus
 adapting some of the Isabelle Display Logic theories to prove results
about interpolation for Display Logic;
this work involved programming (in Standard ML) complex proof search routines
 implementing in Isabelle proofs of cutelimination theorems
for sequent calculi, including for the provability logic GL
 proving the strong normalisation result for cutelimination
for the relation algebra Display Calculus,
and implementing the proof in Isabelle
(I intended to implement an existing proof in Isabelle, but in doing so
discovered an error, so I developed a new proof)
 generalising the above strong normalisation result into
publishable results on termination of rewrite systems generally,
generalising other known results in the area
 helping to develop theories for analysing the spicalculus, and
decision procedures for deducibility constraint systems and for bitrace
consistency, and formally verifying these
 developing aspects of the implementation of using Lax Logic
to calculate timing constraints while proving logical (timefree)
properties of hardware circuitry
 formalising and proving most of the laws of the
``Timed Interval Calculus'' in Isabelle
 formalising and proving results about the "general correctness"
and other approaches to program semantics, based on work by Steve Dunne
 formalising and proving results (in the HOL theorem prover)
about compound monads, relating a distributive law for monads to one monad
in the Kleisli category of another
The proofs referred to above (except the work on monads)
were implemented in the Isabelle theorem prover.
I have gained extensive
experience in functional programming (in Standard ML).
This led to an interest in functional programming per se
and type systems,
from the point of view of increasing the efficiency and reliability of
software development.
I have done some work on compound monads.
More broadly,
my interests centre around the development of methods and
tools for ensuring the correctness of computer systems,
including
 implementing reasoning frameworks on a computer
 efficient techniques for proof searching

semantics and applications of functional programming languages
and their type systems
I have about 50 publications, which are listed at
http://rsise.anu.edu.au/~jeremy/cv/papers.html
.
 Development of code to efficiently translate propositions about words
(including arithmetic operations on them) into propositions about bits,
to pass them to a SAT solver, and to translate the results of this into
Isabelle proofs (Isabelle / Standard ML, 20078)
 Development of Isabelle theories for words (bitstrings) of fixed but
arbitrary length (Isabelle / Standard ML, 20057)
 Isabelle proofs of theorems about termination of termrewriting systems
(Isabelle / Standard ML, 20035)
 Isabelle implementations of Display Calculi: shallow embeddings of
relation algebras and tense logic (1997), deep embedding of relation algebra
calculus with proofs of cutelimination and strong normalisation (20003),
including programming complex tactics (Standard ML).
 Prototype votecounting system: this program implemented the HareClark
vote counting system (a preferential/proportional system for multimember
constintuencies, used in the ACT), in Standard ML.
 Prototype theorem proving program: the aim was to explore new capabilities
for an existing prover. (Program contained significant new capabilities, but
inferior to LCFstyle provers). (C, 198992).
 Program to parse PL/1 DECLARE statements, and create data dictionary entry
from them. (PL/1, 1986).
 Program to find all vertices of a convex polyhedron, using an adaptation
of linear programming algorithms. Recursive program was capable of
punching out current state when execution time limit approached, for
recommencement in later run. (PL/1, 1974).

Member of school council of Trinity Christian School, 1995  1998.

Member of APFACTS (Association of Parents and Friends of ACT Schools),
as representative of Canberra Grammar School P&F, 2005  2009.

Member of Committee of Christians for an Ethical Society,
2008  2010 and 2011  present.