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.
- Computability
logic
- Deep Inference
- The Logic of
Bunched Implications (BI)
- Separation Logic
- Locus Solens
- Modal Linear
Logic
- Temporal Linear
Logic
- Fibring Logics
- Deduction Modulo
- Disproving
techniques
From an agent
perspective, there are many interesting topics as well, including (but
not limited to):
- AgentSpeak
- Commitment
Machines
- Flexible
Protocols
- BDI
reasoning systems
- Reasoning about
an agent's goals
- Reasoning about
an agent's resources
- Verifying
correct behaviour in an agent system