Research Grants

• LEO II: An Effective Higher-Order Theorem Prover (10/2006–10/2007)
• Beyond Linear Arithmetic: Automatic Proof Procedures for the Reals (10/2005–10/2008)
• Automation for Interactive Proof (1/2004–1/2007)
• Verifying Electronic Commerce Protocols (10/2000–9/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)
• Types for Proofs and Programs: ESPRIT-funded Working Group (9/1996–8/1999) and research action (9/1992–8/1995)
• Logical Frameworks: Design, Implementation and Experiment (6/1989–3/1992). ESPRIT Basic Research Action 3245
• 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.

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