Research Grants

• ALEXANDRIA: Large-Scale Formal Proof for the Working Mathematician (1/9/2017–31/8/2022)
• Automatic Proof Procedures for Polynomials and Special Functions (1/11/2010–31/10/2014)
• Automated Formal Proofs for Polynomial and Transcendental Problems (9/2008–9/2009)
• LEO II: An Effective Higher-Order Theorem Prover (10/2006–10/2007)
• Beyond Linear Arithmetic: Automatic Proof Procedures for the Reals (1/11/2005–31/10/2008)
• Automation for Interactive Proof (1/2004–5/2007)
• Verifying Electronic Commerce Protocols (10/2000–10/2003)
• Compositional Proofs of Concurrent Programs (10/1999–6/2003)
• Authentication Logics: New Theory and Implementations (1/1996–6/1999)
• Mechanising Temporal Reasoning (11/1995–4/1999)
• Combining HOL with Isabelle (9/1992–8/1995)
• Verifying ML Programs Using Evaluation Logic (9/1991–2/1995) [co-investigator]
• Types for Proofs and Programs: EU-funded ESPRIT Working Group (9/1996–8/1999) and research action (9/1992–8/1995)
• Logical Frameworks: Design, Implementation and Experiment (6/1989–3/1992). EU-funded ESPRIT Basic Research Action 3245
• The Alvey Diamond project (7/1986–6/1989). Funded by the SERC, grant references
  GR/E/02369 and GR/F/10811 [co-investigator]
• Supporting Logics (6/1986–11/1989). Funded by the SERC, grant reference GR/E0355.7

The EPSRC publish the official version of my grant portfolio, going back to 1991.

Since 2003 I have belonged to the EPSRC Peer Review College, whose task is to review funding applications.

Last revised: Thursday, 6 October 2022