Michael Fourman >> research
Students Tools EPSRC Projects Publications
Manifesto
My research interests are centred around applications of logics in Computer Science, Artificial Intelligence, and Cognitive Science.
I started my academic career as a mathematical logician, viewed by mathematicians as a kind of philosopher, and by philosophers, somewhat more accurately, as a mathematician. Now I'm counted a computer scientist, and hope to contribute to the development of the new science of Informatics. Between these times, I've worked in Electronic Engineering. Yet, all the while, my interests have hardly changed. How is this?
Whatever diverse aspects of the world we represent within a computer, we reduce to formal symbols. In computer science, we characterise computation as the methodical, or algorithmic, processing of formal representations. Logicians study reasoning, represented as the methodical processing of formal statements. More generally, they study the relationships between formal representations and their meanings.
The processing of formal representations encompasses both logic and computation, but without meaning, both are dry. Meaning relates our formal representations to the world, and brings them to life.
To grasp the world, we model it. To interact, we communicate. Increasingly, we use formal, digital representations, largely because computer technology makes them tractable. A global network of computers supports the representation, transformation and communication of information. We see similar phenomena in human communication. We have mental models, we reason, we communicate. Can these phenomena be understood in terms of traditional accounts of logic and computation? Perhaps not. But these traditions provide a good basis from which to start, complemented by the traditions of cognitive science, psychology and linguistics.
We define Informatics to be the study of the structure, behaviour, and interactions of natural and artificial computational systems: a science of information. We seek to relate cognition, communication, and computation; to understand what information is, how it is represented, and how it is transformed--whether by computation or communication, whether by organisms or artefacts.
The science of information is emerging as a new division of science, alongside the physical and biological sciences. It is contributing to a revolution in the ways we think about the world, and ourselves - about perception, about decision, about action.
Interests
Logic
My early work in logic concerned intuitionistic logic, connections between category theory and logic, independence results in constructive analysis, and models for Brouwer's notion of choice sequence.
Hardware Specification and Verification
I then became interested in hardware design, applying formal models of behaviour to build tools formalising the design process, for the inferential construction of correct systems. This led to the LAMBDA system developed by Abstract Hardware Limited, a tool implemented in the SML programming language.
Programming Language Semantics
I have worked on applying category theory to programming language semantics - in particular, categorical semantics for the SML module system, and semantics for partial functions.
This led to joint work with John Longley and Gordon Plotkin on ``Notions of Computability for General Datatypes'', a project funded by EPSRC.
Longley, Fleuriot and I had EPSRC funding (2001-2004) for a project, A Proof System for Correct Program Development. This exploited advances in semantic understanding, coming from Longley's work on notions of computability. Randy Pollack worked on this project, to integrate programming and proof by implementing in Isabelle a logic whose terms are defined using the programming language (a subset of ML).
This style of integration was first introduced in the LAMBDA system.
AI Planning
In 2000, I applied model-checking techniques using Binary Decision Diagrams to implement PropPlan, an AI Planning system.
Statistical Satisfiability
I have more recently been working on integrating logical and probabilistic reasoning. The StatSat Project is building a representation and reasoning engine based on these ideas.