Invited Lectures

  1. Compiler generation from denotational semantics
    In: B. Lorho (editor), Methods and Tools for Compiler Construction (Cambridge University Press, 1984), 219-251.
  2. Lessons learned from LCF. DDC Workshop on Combining Specification Methods, Nyborg, Denmark (1984)
  3. Joint BCS/SERC Workshop on Program Specification and Verification, York (1983)
  4. BCS Formal Aspects of Computing Science, London (1984)
  5. Specification and Derivation of Programs, Marstrand, Sweden (1985)
  6. IEE/BCS Colloquium on Theorem Provers in Theory and Practice, London (1987)
  7. Experience with Isabelle: a generic theorem prover
    In: P. Martin-Löf &G. Mints (editors), COLOG-88: International Conf. in Computer Logic.Tallinn, Estonia (1988). Preliminary proceedings.
  8. Applications of proof theory to Isabelle, Leeds Proof Theory Summer School (1990)
  9. Tool support for logics of programs. In: M. Broy (editor), Mathematical Methods in Program Development (Summer School Marktoberdorf 1996), Springer-Verlag,
    Slides available
  10. Strategic principles in the design of Isabelle.
    CADE-15 Workshop on Strategies in Automated Deduction, Lindau, Germany (1998), 11–17.
    Slides available
  11. Security protocols and their correctness.
    Automated Reasoning Workshop 1998. St. Andrews, Scotland (1998)
    Slides available
  12. Proving security protocols correct.
    IEEE Symposium on Logic in Computer Science.
    Trento, Italy (1999).
    Slides available
  13. Getting started with Isabelle.
    EEF Foundations School on Deduction and Theorem Proving
    . Edinburgh, Scotland (2000).
  14. SET Cardholder Registration: the secrecy proofs.
    Automated Reasoning: First International Joint Conference. IJCAR,
    Siena, Italy (2001), 5–12.
    Slides availablePublisher's version at
  15. Verifying the SET protocol: overview.
    FASec 2002: Formal Aspects of Security. Royal Holloway College, University of London, England, December 2002.
    Slides available
  16. Formalizing abstract mathematics: issues and progress.
    Computer-Supported Mathematical Theory Development. Cork, Ireland, July 2004.
    Slides available
  17. Computational logic and the quest for greater automation.
    Inaugural lecture upon conferment of the title of Distinguished Affiliated Professor, Munich, Germany (2006).
    Slides available
  18. Automated assistance for proof assistants.
    Colloquium in Honour of Gérard Huet, Paris, France, June 2007.
    Slides available
  19. Automation for interactive proof: techniques, lessons and prospects. Tools and Techniques for Verification of System Infrastructure, Royal Society, London, UK, March 2008.
  20. The relative consistency of the axiom of choice — mechanized using Isabelle/ZF,
    Computability in Europe 2008 Special Session on Formalising Mathematics and Extracting Algorithms from Proofs, Athens, Greece, June 2008.
    Extended abstract available; see also original paper
  21. Three years of experience with Sledgehammer, a practical link between automatic and interactive theorem provers. PAAR-2010: Workshop on Practical Aspects of Automated Reasoning. Edinburgh, Scotland, July 2010. (Talk given by Jasmin Christian Blanchette.) An updated version appeared in G. Sutcliffe, E. Ternovska, and S. Schulz (eds) 8th International Workshop on the Implementation of Logics (IWIL-2010). Yogyakarta, Indonesia, October 2010.
  22. LCF + logical frameworks = Isabelle (25 years later).
    Milner Symposium.
    Edinburgh, Scotland, April 2012.
    Slides available
  23. Overcoming intractable complexity in an automatic theorem prover for real-valued functions.
    CCA 2012: Ninth International Conference on Computability and Complexity in Analysis.
    Cambridge, England, June 2012.
    Slides available
  24. MetiTarski: past and future.
    Interactive Theorem Proving — ITP 2012
    Princeton, New Jersey, August 2012.
    Publisher's version at www.springerlink.comSlides available
  25. Isabelle/HOL Tutorial: verifying functional programs and inductively defined sets.
    International Conference on Relational and Algebraic Methods in Computer Science (RAMiCS 13).
    Cambridge, England, September 2012.
  26. MetiTarski's menagerie of cooperating systems.
    Plenary lecture for the FroCoS and Tableaux conferences.
    Nancy, France, September 2013.
    Publisher's version at www.springerlink.comSlides available
  27. Theorem proving and the real numbers: overview and challenges.
    Keynote lecture for NASA Formal Methods.
    Houston, Texas, April 2014. Slides available
  28. Automated theorem proving for special functions: the next phase.
    Keynote lecture for SNC 2014 (Symbolic-Numeric Computation).
    Shanghai, China, July 2014.
    Slides available
  29. The future of formalised mathematics.
    Keynote lecture for EACA 2016 (XV Encuentro de Álgebra Computacional y Aplicaciones). Logroño, Spain, June 2016.
    Slides available
  30. ACM DL Author-ize servicePorting the HOL light analysis library: some lessons (Keynote lecture)
    CPP 2017 Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, Paris, January 2017 Slides available

Last revised: 3 April, 2017

Lawrence C. PaulsonComputer LaboratoryUniversity of Cambridge