Overview

This group is concerned with developing mathematical models and theories that underpin the design and analysis of programming languages and help explain computational phenomena, such as real number computation. The research primarily focuses on logical, categorical, topological, and order-theoretic structures, and the relationship between them. Future work will concentrate on the challenge of efficient exact real number computation and logical foundations of programming calculi.

Main Academic Staff:

PhD Students:

Domain Theory:

A denotational semantics maps programming constructs into a mathematical universe of semantic spaces. These semantic spaces carry a lot of structure because they reflect the fact that one program can be better than another one (e.g. by being able to process a wider range of inputs), that loops are equivalent to the limits of their finite unwindings, and that programs can be executed effectively. Consequently, we find that semantic spaces carry an order relation, a topology, and an effective structure. Because of the interaction between these aspects, the mathematical theory of these objects becomes very rich and interesting. The first person to introduce semantic spaces into denotational semantics was Dana Scott; he called them "domains". His approach has proven to be very robust and to play a useful role in many different contexts, but there are now also some alternative approaches. Members of the group have contributed substantially to the understanding and the structural analysis of semantic universes. Most recently, for example, Achim Jung, in collaboration with Mathias Kegelmann (Darmstadt) and Andrew Moshier (USA), have developed a sequent calculus which provides a purely logical analysis (via cut-elimination) of domain-theoretic constructions. The corresponding semantic spaces are stably compact topological spaces with topologically closed relations as morphism. A large number of relevant closure properties of this universe have been established, most recently that of bilimits and the probabilistic powerdomain.

Exact numerical computation:

This research is based on a rigorous mathematical model of the real numbers which avoids the round-off errors inherent in the traditional floating-point representation. Martin Escardo extended PCF with real numbers. The work has laid foundations for further work in many places (Imperial, St Andrews, Paris). He established the fundamental properties of adequacy and universality for higher-order exact real number computation. Integration, as an important example of a higher-order operation has also been studied. With Martin Hofmann and Thomas Streicher (Darmstadt) he discovered the inherent parallelism of basic functions in this approach. Together with Achim Jung, Michal Konecny characterised precisely those real-valued functions which are computable by a resource restricted device. Future work will concentrate on the impact of representation on the efficiency of real-number algorithms. The collaboration with St Andrews on the integration of exact numerical computation into computer algebra systems will continue.

Computational Logic:

In this area, the emphasis of has been on linear logic and linear lambda calculi. Valeria De Paiva, Eike Ritter and Neil Ghani designed the first explicit substitution calculus for linear logic and proved important meta-theoretic properties, using categorical semantics to clarify subtle interactions between explicit substitutions and linearity. De Paiva, Ritter, Maria Maietti and Paola Maneggia gave a systematic account of the relationships between various linear lambda-calculi and their models. De Paiva, Ritter and Ghani applied techniques from linear logic to modal logic and obtained a novel characterisation of computation in stages. Ritter solved the long-standing termination problem for calculi with explicit substitution. Ritter and David Pym (Queen Mary) showed how intuitionistic proof search can be seen as a special case of their counterparts in classical logic. Future work will concentrate on the semantic characterisation of proof search, automatic program optimisation of staged computation, and modal logic for knowledge representation. A new collaboration with Viviana Bono (Turin) will study languages combining functional and object-oriented features.

Logic of Topology and Toposes:

The Scott topology on domains is of central importance, since computable functions are naturally continuous. Moreover, this can be explained in an information-theoretic way, with open sets corresponding to properties of programs that can be "finitely observed at run-time". Such insights have led to a computer science interest in the more general foundations of topology and its relationship with logic (such as logical theories of observation), and has made computer scientists active participants in the pure mathematical study of those topics. The topology is often approached in a "point-free" style (in which the logic is prior to the points), and also involves algebra and category theory. In Birmingham Steve Vickers works on the so-called "geometric" logic, which is particularly closely connected to topology and naturally extends to the generalized topology of toposes. For deep logical reasons it is useful to know whether ordinary mathematics can be done within the constraints of geometric logic, and Steve has been finding positive answers in a range of case studies. Along the way he has developed new techniques in point-free topology, such as tools using powerlocales (or point-free hyperspaces: spaces whose points are subspaces of other spaces).

In a new EPSRC-funded project "Applications of geometric logic to topos approaches to quantum theory", Steve and Bertfried Fauser are studying the interaction between those ideas and recent topos applications to the foundations of quantum physics.