- The Integration and Interaction of Multiple Mathematical Reasoning Processes (Google site)
- A Cognitively Based Model of Theory Formulation and Reformulation
- Dynamic Ontology Refinement
- Theory Formation
- Distributed Theorem Proving
- Ontology Evolution in Physics
- A Category-Theoretic Framework for Ontology Management
- Proof Engineering: Refactoring Proof: developing refactoring techniques for proof scripts.
- Proof Guided Ontology Development
- Faulty Ontology Detection and Repair

- A Generic Approach to Proof Planning - development of the IsaPlanner system
- Automated Discovery of Inductive Lemmas

- Security and Verification:
- Automated Analysis of Security Critical Systems
- Coral - finding counterexamples to false inductive conjectures
- NuSPADE: Automatic Guidance for the Formal Verification of High Integrity Ada
- The Use of Proof in the Location of Programming Errors

- Mathematics and Formalisation:
- Formal Verification of Computational Geometry
- Isabelle Projects
- MATHsAiD - Automatically generating mathematical theorems
- Quantomatic - Automated Reasoning for Quantum Computations
- MathSoMac - The Social Machine of Mathematics

- the Grid, E-Science, Web Services and Beyond:
- Inferring Quality of Service Properties for Grid Applications
- Deductive Synthesis of Grid Workflows for e-Science
- MathServe - a framework for integrating reasoning systems as Web Services
- Open Knowledge Project - a unifying framework for Web service composition

- PolyML - Our various Standard ML/PolyML projects
- Recommender System for an Interactive Theorem Prover
- Anastasia - a functional programming editor that uses formal verification
- Hierarchical Proofs and Graphs (HiProofs and HiGraphs)
- Proof General - a generic interface for proof assistants.