- 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*: 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*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: 25 May, 2017

Lawrence C. Paulson • Computer Laboratory • University of Cambridge