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 available • Publisher's version at www.springerlink.com
  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.com • Slides 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.com • Slides 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. Porting the HOL light analysis library: some lessons (Keynote lecture)
    CPP 2017 Sixth ACM SIGPLAN Conference on Certified Programs and Proofs.
    Paris, France, January 2017. Slides available
  31. Proof assistants: from symbolic logic to real mathematics?
    "Jacques Morgenstern" Colloquium.
    Inria Sophia-Antipolis, France, May 2017. Slides available
  32. Proof assistants: from symbolic logic to real mathematics?
    Big Proof programme, Isaac Newton Institute for Mathematical Sciences.
    Cambridge, UK, July 2017.
  33. Proof support for hybrid system analysis.
    Logical Methods for Safety and Security of Software Systems
    (Summer School Marktoberdorf, August 2017).
  34. Automatic theorem proving: impressions from the interactive world.
    Herbrand Award acceptance speech. Conference on Automated Deduction (CADE-26).
    Gothenburg, Sweden, August 2017. Slides available
  35. A career in research: Mike Gordon and hardware verification.
    Automated Reasoning Workshop.
    Cambridge, UK, April 2018. Slides available
  36. Formalising mathematics in simple type theory.
    Big Proof programme, International Centre for Mathematical Sciences.
    Edinburgh, UK, May 2019. Slides available
  37. Machine learning and the formalisation of mathematics: research challenges.
    Keynote lecture for Conference on Artificial Intelligence and Theorem Proving (AITP). Aussois, France (virtual), September 2020.
    Slides available
  38. Doing Mathematics with simple types: infinitary combinatorics in Isabelle/HOL.
    Harvard University Center Of Mathematical Sciences and Applications (virtual), March 2021.
    Slides available
  39. Formalising contemporary mathematics in simple type theory.
    Topos Institute Colloquium (virtual), July 2021.
    Slides available
  40. Formalised mathematics: obstacles and achievements.
    Zhejiang University (virtual), September 2021.
    Slides on types • Slides on formalising mathematics
  41. Automated theorem proving: a technology roadmap.
    Huawei Mathematical Theorem Proving Workshop. Cambridge, UK, April 2022.
    Slides available
  42. Formalising Erdős and Larson: ordinal partition theory.
    Leeds Logic Seminar, University of Leeds, UK, March 2023.
    Slides available
  43. Formalising a number theory textbook: lessons learnt.
    University of Cambridge Symposium for Andrew Pitts, Cambridge, UK, August 2023.
    Slides available • 20-minute video
  44. Large-scale formal proof for the working mathematician: lessons learnt from ALEXANDRIA.
    Keynote lecture for Conference on Intelligent Computer Mathematics, Cambridge, UK, September 2023.
    Slides available
  45. Formalising 21st-Century Mathematics.
    London Mathematical Society / Formal Aspects of Computing evening seminar (virtual). January 2024.
    Slides available