Mathematical Foundations and Applications
Dr Russell Bradford, Professor James Davenport, Professor John Fitch, Dr Alessio Guglielmi, Professor Guy McCusker, Prof Nicolai Vorobjov, Dr Marina De Vos, Dr James Laird, Dr John Power
The Department has a wide range of activities based on ideas and techniques in the mathematical foundations of computer science and their applications. One group is based on algorithms:
- Computational algebra, geometry & number theory
- Cryptography, networks & security
- Computational complexity
- Geometry and robot motion planning
Here there is an emphasis on the use of computers to manipulate representations of algebraic and geometric concepts, with applications to topics such as cryptography, security and engineering. The Department is the UK's leading centre for this work in computational mathematics and its applications. Our work spans the spectrum of research from the pure, such as abstract algebra, to the applied, such as symbolic-numeric interfaces. Development of new algorithms for exact computation, manipulation of algebraic numbers and functions, analytic integration and integer factorisation is complemented by implementation of these and other algorithms within a coherent whole.
The design and analysis of secure reliable communication protocols is an area of substantial industrial interest requiring the interplay of mathematics and computer science. This is particularly true for protocols which rely on "public key" cryptography systems for security or authentication. Many of these can be broken by the application of enough computing time, and Bath has been involved in several analyses of algorithms for this, in particular the discrediting of a GF(2^n) variant of the Diffie-Hellman scheme.
The group has strong links with research teams in computer algebra both elsewhere in the UK and worldwide. It is the EU centre of expertise on interfacing computer algebra to numeric calculations.
Applications studied in the group include solid modelling and geometric theorem proving with applications in robotics. We have strong links with NAG Ltd who have funded two PhD students, collaborated on several EU-funded projects and share our interests in interfaces to computer algebra systems, such as Axiom, and "web mathematics" in general.
Staff in this area include: Russell Bradford, James Davenport, Julian Padget, Dan Richardson, Nicolai Vorobjov.
Another group is concentrated in semantics:
- Mathematical logic
- Semantics of computation
- Logic programming & theorem proving
- Resource modelling
Here the focus is on mathematical logic and theoretical computer science. We are concerned with the mathematical understanding of logical reasoning, of programs, of processes, of programming languages, and of the basis for tools such as theorem provers. Our methods include ideas and techniques from category theory, game theory, model theory, proof theory and type theory, as well from more traditionally computational topics such as automata, formal languages and computability.
A particular strength is our activity in resource modelling, based on the development of the logic of bunched implications, BI, which draws upon ideas from mathematical logic, the semantics of programming languages and, from HCI, task analysis and interaction modelling. This work has been applied by our collaborators to the problem of giving an adequate program logic for mutable data structures, solving a problem which had remained open for 30 years.
Staff in this area include: David Pym, Guy McCusker, Dan Richardson, Nicolai Vorobjov, Marina De Vos and Alessio Guglielmi.
Mathematical Knowledge Management is a broad topic spanning the application of theorem proving, formalization of proof procedures, representation of mathematical semantics, mathematical reasoning and recovery of mathematical information from printed and hand-written text. Work at Bath (James Davenport, Julian Padget) focuses on the development of ontological markup to describe mathematical semantics and the use of mathematical reasoning for brokerage in service-oriented architectures.
In addition to these quite tightly focussed activities, the Department has interests in a wide range of software-oriented technologies:
- Agent technologies
- Compiler technology
- E-commerce
- Networking & distributed systems
- Object-oriented programming & design
- Software engineering methodologies
Our work in this area is driven primarily by applications but covers a wide range of activities from the design and implementation of domain-specific languages through specification and refinement, involving concerns such as inheritance, modularity and software re-use.
The mathemetical foundations group runs an occasional seminar series.
Recent publications
Guglielmi, A. (2007). A system of interaction and structure. ACM Transactions on Computational Logic, 8(1):1-64.
McCusker, G. & Pym, D. (2007). A Games Model of Bunched Implications, in Computer Science Logic, Proceedings of the 21st International Workshop CSL 2007. Springer-Verlag Lecture Notes in Computer Science, 4546:573-588.
Hyland, M., Plotkin, G.D. & Power, A.J. (2006). Combining effects: sum and tensor, Theoretical Computer Science, 70--99.
Stratford,J.D. & Davenport,J.H., Unit Knowledge Management. Proc. AISC/Calculemus/MKM 2008 (ed. S. Autexier et al.), Springer Lecture Notes in Artificial Intellgence 5144, Springer-Verlag, pp. 266-280.
