Overview of my Research Interests

My research is centred around the applications of mathematical logic to computer science. In particular, this is concerned with automated reasoning techniques, which can be used as the basis for a class of programming languages known as logic programming languages. The central idea is that by writing programs as formulae (or statements) in a logic language, we are able to reason directly about the program and its properties, as well as being able to write complex programs more succinctly and understandably than in imperative languages.

One of the key areas of interest is in the development of programming languages based on resource-sensitive logics such as linear logic. This involves a study of the proof theory of such logics, in order to identify appropriate search strategies (and hence computational models), the development of implementation techniques for such languages and application to areas such as database transactions, concurrent programming, reasoning about dynamic environments and agent-oriented programming. One outcome of this research has been the programming language Lygon.

My background is in logic programming, but of a more logically liberal bent then most, and hence many of my interests are in the overlap between logic programming, automated reasoning and mathematical logic. I am particularly interested in the use of logical techniques for the design, implementation and evaluation of programming languages. This has lead me to a significant amount of work on the applications of resource-sensitive logics, such as linear logic, to the design of logic programming languages. The programming language Lygon is the most tangible outcome of this. I am also interested in the development of agent programming languages, which is in many ways an extension of the logic programming approach but in a much less constrainted setting. Partly as a result of having taught Computing Theory to second-year students for many years, I am also interested in other topics in theoretical computer science such as primality testing, cryptography, quantum computing, Busy Beaver machines and NP-completeness.

I think there are many new and interesting developments in logic and proof theory of late, and I am interested in exploring (when I get the time! :-) topics such as those below.
From an agent perspective, there are many interesting topics as well, including (but not limited to):