My principal research field is the theory and practice of programming languages such as first- and higher-order clausal logics, and some constraint logic programming languages.
My work specifically concerns model-theoretic and operational semantics, and empirical and theoretical feasibility analyses of runtime implementation methods for them. These include Artificial Intelligence ones such as constraint solving using search, term rewriting, unification and matching.
These languages are examples of Abstract Clauses, a deductive logical framework. Empirical analyses are enabled by my software, the Abstract Clause Engine (ACE) for implementing specific Abstract Clause languages and programs. ACE is written in Standard ML, and there is a Java version.
My other research has concerned topics in the semantics of concurrent object-oriented languages, linear recurrences such as generalized Fibonacci sequences, model generation, and Artificial Intelligence in medical diagnosis.
These are some publications from when I was a lecturer at ANU.
Volume 31 (Elsevier, Amsterdam, 2000) pages 1-184.
Guest Editor, Proceedings of Computing: the Australasian Theory Symposium, 2000. CATS 2000 was held at ANU and I was Chair of the Programme Committee. The invited speakers were Rod Burstall (Edinburgh), Mariangiola Dezani-Ciancaglini (Turin), Lance Fortnow (NEC, Princeton) and Emo Welzl, (ETH, Zürich).
with Qing Guo and Paliath Narendran
Information and Computation 162 , 3-23 (October 2000)
We consider the complexity of equational unification and matching problems where the equational theory contains a nilpotent function, i.e., a function f satisfying f(x, x)=0 where 0 is a constant. We show that nilpotent unification and matching are NP-complete. In the presence of associativity and commutativity, the problems still remain NP-complete. However, when 0 is also assumed to be the unity for the function f, the problems are solvable in polynomial time. We also show that the problem remains in P even when a homomorphism is added. An application of this result to a subclass of set constraints is illustrated. Second-order matching modulo nilpotence is shown to be undecidable.
Journal of Symbolic Computation 29, 1 (2000) 79-82.
This paper continues some ideas in the one below on generlaised Fibonacci recurrences, and provides a formula for their solution.
We give a formula for the general solution of a d th-order linear difference equation with constant coefficients in terms of one of the solutions of its associated homogeneous equation. The formula neither uses the roots of the characteristic equation nor their multiplicities. It can be readily generalized to the case where the domain of the difference equation is the real numbers, and the initial values are given by a function defined on the interval [0,d ). In both cases, we express the general solution of the difference equation in terms of a single solution of its associated homogeneous equation at integer arguments.
These sequences are defined by the sum of the previous n values where n > 1 and also generalised by using initial functions instead of initial values. Lemma 3.6 in this paper gives bounds on the roots of the characteristic equation of generalised Fibonacci sequences.
This Lemma has been applied widely in other research.
The paper gives the solution in radicals for the positive root of the characteristic equation when n = 4, the Tetranacci constant, and also a series for the positive root for any n > 0. These results were summarised in a Wikipedia article on Generalizations of Fibonacci numbers.
Artificial Intelligence in Medicine 7, 2 (1995) 93-116.
"INTERNIST-I was an expert system designed in the early 1970's to diagnose multiple diseases in internal medicine by modelling the behaviour of clinicians. Its form and operation are described, and evaluations of the system are surveyed. The major result of the project was its knowledge base which has been used in successor systems for medical education and clinical use. We also survey the effects of the project through these systems, and conclude that the most successful of them in the near future is likely to be Quick Medical Reference (QMR) when used as an “electronic textbook” of medicine."
This paper has various citations including one of many in U.S. patent 7230529, for “System, method, and computer program for interfacing an expert system to a clinical information system" that was awarded to Theradoc in 2007.
Fellow of the British Computer Society (FBCS)
Senior Member of the Institute of Electrical and Electronics Engineers
Senior Member of the Association for Computing Machinery
Life Fellow of the Cambridge Philosophical Society (FCPS)
Fellow of the Royal Society of Arts (FRSA), London
DPhil, by incorporation, University of Oxford
Junior Research Fellow, Christ Church, Oxford
Chartered Information Technology Professional (CITP), British Computer Society
Chartered Engineer (CEng), The Engineering Council, London
European Engineer (Eur Ing), European Federation of National Engineering Associations, (FEANI), Brussels
The Rae and Edith Bennett Travelling Scholarship, The University of Melbourne
Overseas Research Students Award (ORS), Committee of Vice-Chancellors and Principals of the Universities of the United Kingdom.
BSc (Hons) The University of Melbourne} First Class Honours in Computer Science. My Honours thesis was on the soundness and completeness of operational semantics of logic programming. I was the lead author of a joint paper based on it and presented the paper at an international logic programming conference at Uppsala University, Sweden.
MSc The University of Melbourne. I defined a backtracking search method called Adaptive Backtracking that learns to avoid repeating fruitless searches while running, and analysed its complexity. I applied it to logic programming, tested its performance and compared it to other Artificial Intelligence search methods. I won a Faculty of Science Postgraduate Writing-Up Award, and published two papers based on it, one in the proceedings of an international conference held at Imperial College, London.
PhD University of Cambridge. Adviser: Larry Paulson. I defined a higher-order programming language called The Clausal Theory of Types and operational and model-theoretic semantics for it. The dissertation was the basis of a book published by Cambridge University Press. Two topics particularly gained the attention of other researchers: a form of higher-order rewriting defined there that was applied to theorem proving and program transformation, and the then open question of the decidability of higher-order matching.
MBA (Executive) The University of New South Wales and The University of Sydney.
Special Issues: Electronic Notes in Theoretical Computer Science; and Theoretical Computer Science
Electronic Notes in Theoretical Computer Science; IEEE Transactions on Computers; Information and Computation; Information Processing Letters; Journal of Automated Reasoning; Journal of Future Computing Systems; Journal of Symbolic Computation; Mathematical Structures in Computer Science; Science of Computer Programming; Technique et Science Informatiques; Theoretical Computer Science.
Chair of Committee, CATS 2000. Computing: The Australasian Theory Symposium, ANU, Canberra.
Member, Programme Committee, Computing: The Australasian Theory Symposium
Member, Organising Committee, Australasian Computer Science Week, Canberra, 2000.
The Netherlands Computer Science Research Foundation, (Stichting Informatica Onderzoek in Nederland)
Lawrence C. Paulson, ML for the Working Programmer, Cambridge University Press, First edition, 1991.