Jeremy Edward DAWSON
Curriculum Vitae

Personal

Born 29 June 1952, Sydney, N.S.W., Australia.
Married, with 2 children.
Australian citizenship.
Address : 36 Bateman St, Kambah, ACT 2902, Australia. (phone 02-6231-2102)
Email : jeremy@rsise.anu.edu.au

Education

Ph.D.
in Pure Mathematics (combinatorial mathematics), University of Sheffield, Jan 1976 - Jun 1978 (part-time 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 first-class 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 (part-time).

part of M.Eng.Sc
in Operations Research, University of N.S.W., Feb - Nov 1974 (part-time, subjects taken amounted to 33% of whole degree).

part of M.Sc
in Applied Statistics, Australian National University, Feb - Jun 1980 (part-time, subjects taken amounted to 37% of whole degree).

Employment

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 semester-long 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 semester-long 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 Spi-calculus, 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 cut-elimination 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 (bit-strings) of fixed but arbitrary lengths.
In 2006 and 2007 I did 50% of the teaching of a semester-long 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 cut-elimination 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 vote-counting in ACT Government elections (using the complex Hare-Clark 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/non-zero 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 3rd-year 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 computer-based 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 (part-time) :
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).

Contracts

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

Research

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 non-trivial verification activity, and automated proof tools (such as Isabelle and HOL). I have considerable experience using the computer-based 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.

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

I have about 50 publications, which are listed at http://rsise.anu.edu.au/~jeremy/cv/papers.html.

Software

Other Activities