Dr David Wolfram

Visitor and Former Staff
BSc (Hons), MSc Melb, MBA (Exec) NSW and Syd, PhD Camb, FBCS, FRSA

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.

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.




Guest Editor


Special Issues:  Electronic Notes in Theoretical Computer Science;  and Theoretical Computer Science 


Journal referee


Electronic Notes in Theoretical Computer Science; IEEE Transactions on ComputersInformation and Computation; Information Processing Letters; Journal of Automated Reasoning; Journal of Future Computing SystemsJournal of Symbolic Computation; Mathematical Structures in Computer Science; Science of Computer ProgrammingTechnique 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.


Conference Referee


Numerous conferences


Grant Reviewer


The Netherlands Computer Science Research Foundation, (Stichting Informatica Onderzoek in Nederland)


Book Proofreading


Lawrence C. Paulson, ML for the Working Programmer, Cambridge University Press, First edition, 1991.


Updated:  10 August 2021/Responsible Officer:  Dean, CECS/Page Contact:  CECS Marketing