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-5104-0941)
Email : jeremy@cecs.anu.edu.au Mobile Phone: 0415551466

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, Logic and Computation Group, Research School of Computer Science, (formerly Automated Reasoning Group, Research School of Information Sciences and Engineering), Australian National University. I worked in various positions, mostly on ARC Grants held by Rajeev Goré, developing and implementing proofs in meta-logic in the Isabelle, HOL4 and Coq theorem provers. Topics included

• interpolation for display calculi
• the question of decidability of ticket entailment
• Full Intuitionistic Linear Logic
• cut admissibility for Dyckhoff's LJT system for intuitionistic logic
• syntactic proof of cut admissibility for linear logic
• well-founded unions of well-founded relations
• dual tableaux for intuitionistic logic

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

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.

• 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 cut-elimination 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 cut-elimination theorems for sequent calculi, including for the provability logic GL
• proving the strong normalisation result for cut-elimination 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 spi-calculus, and decision procedures for deducibility constraint systems and for bi-trace consistency, and formally verifying these
• developing aspects of the implementation of using Lax Logic to calculate timing constraints while proving logical (time-free) 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

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://users.cecs.anu.edu.au/~jeremy/cv/papers.html.

Software

• 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, 2007-8)
• Development of Isabelle theories for words (bit-strings) of fixed but arbitrary length (Isabelle / Standard ML, 2005-7)
• Isabelle proofs of theorems about termination of term-rewriting systems (Isabelle / Standard ML, 2003-5)
• Isabelle implementations of Display Calculi: shallow embeddings of relation algebras and tense logic (1997), deep embedding of relation algebra calculus with proofs of cut-elimination and strong normalisation (2000-3), including programming complex tactics (Standard ML).
• Prototype vote-counting system: this program implemented the Hare-Clark vote counting system (a preferential/proportional system for multi-member 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 LCF-style provers). (C, 1989-92).
• 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).

Other Activities

• 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.
• Board member and Treasurer of Synergy Youth and Children (organization of the Anglican Diocese of Canberra and Goulburn) 2012 - present.