Invited Lectures
- Compiler generation from denotational semantics
In: B. Lorho (editor), Methods and Tools for Compiler
Construction (Cambridge University Press, 1984), 219-251.
- Lessons learned from LCF. DDC Workshop on Combining Specification Methods, Nyborg, Denmark (1984)
- Joint BCS/SERC Workshop on Program
Specification and Verification,
York (1983)
- BCS Formal Aspects of Computing
Science, London (1984)
- Specification and Derivation of
Programs, Marstrand, Sweden (1985)
- IEE/BCS Colloquium on Theorem
Provers in Theory and Practice,
London (1987)
- 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.
- Applications of proof theory to Isabelle, Leeds Proof Theory Summer School (July 1990)
- Tool support for logics of programs.
In: M. Broy (editor), Mathematical Methods in Program
Development (Summer School Marktoberdorf, August 1996), Springer-Verlag,
- Strategic principles in the design of Isabelle.
CADE-15 Workshop on Strategies in Automated Deduction, Lindau, Germany (July 1998), 11–17.
- Security protocols and their correctness.
Automated Reasoning Workshop 1998. St. Andrews, Scotland (March 1998)
- Proving security protocols correct.
IEEE Symposium on Logic in Computer Science. Trento, Italy (July 1999).
- Getting started with Isabelle.
EEF Foundations School on Deduction and Theorem Proving.
Edinburgh, Scotland (April 2000).
- SET Cardholder Registration: the secrecy proofs.
Automated Reasoning: First International Joint Conference. IJCAR, Siena, Italy (2001), 5–12.
•
- Verifying the SET protocol: overview.
FASec 2002: Formal Aspects of Security. Royal Holloway College, University of London, England, December 2002.
- Formalizing abstract mathematics: issues and progress.
Computer-Supported Mathematical Theory Development. Cork, Ireland, July 2004.
- Computational logic and the quest for greater automation.
Inaugural lecture upon conferment of the title of Distinguished Affiliated Professor, Munich, Germany (May 2006).
- Automated assistance for proof assistants.
Colloquium in Honour of Gérard Huet, Paris, France, June 2007.
- Automation for interactive proof: techniques, lessons and prospects. Tools and Techniques for Verification of System Infrastructure, Royal Society, London, UK, March 2008.
- 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
- 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.
- LCF + logical frameworks = Isabelle (25 years later).
Milner Symposium.
Edinburgh, Scotland, April 2012.
- 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.
- MetiTarski: past and future.
Interactive Theorem Proving — ITP 2012
Princeton, New Jersey, August 2012.
- 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.
- MetiTarski's menagerie of cooperating systems.
Plenary lecture for the FroCoS and Tableaux conferences.
Nancy, France, September 2013.
- Theorem proving and the real numbers: overview and challenges.
Keynote lecture for NASA Formal Methods.
Houston, Texas, April 2014.
- Automated theorem proving for special functions: the next phase.
Keynote lecture for SNC 2014 (Symbolic-Numeric Computation).
Shanghai, China, July 2014.
- The future of formalised mathematics.
Keynote lecture for EACA 2016 (XV Encuentro de Álgebra Computacional y Aplicaciones). Logroño, Spain, June 2016.
- 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.
- Proof assistants: from symbolic logic to real mathematics?
"Jacques Morgenstern" Colloquium.
Inria Sophia-Antipolis, France, May 2017.
- Proof assistants: from symbolic logic to real mathematics?
Big Proof programme, Isaac Newton Institute for Mathematical Sciences.
Cambridge, UK, July 2017.
- Proof support for hybrid system analysis.
Logical Methods for Safety and Security of Software Systems
(Summer School Marktoberdorf, August 2017).
- Automatic theorem proving: impressions from the interactive world.
Herbrand Award acceptance speech. Conference on Automated Deduction (CADE-26).
Gothenburg, Sweden, August 2017.
- A career in research: Mike Gordon and hardware verification.
Automated Reasoning Workshop.
Cambridge, UK, April 2018.
- Formalising mathematics in simple type theory.
Big Proof programme, International Centre for Mathematical Sciences.
Edinburgh, UK, May 2019.
- 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.
- Doing Mathematics with simple types:
infinitary combinatorics in Isabelle/HOL.
Harvard University Center Of Mathematical Sciences and Applications (virtual), March 2021.
- Formalising contemporary mathematics in simple type theory.
Topos Institute Colloquium (virtual), July 2021.
- Formalised mathematics: obstacles and achievements.
Zhejiang University (virtual), September 2021.
•
- Automated theorem proving: a technology roadmap.
Huawei Mathematical Theorem Proving Workshop. Cambridge, UK, April 2022.
- Formalising Erdős and Larson: ordinal partition theory.
Leeds Logic Seminar, University of Leeds, UK, March 2023.
- Formalising a number theory textbook: lessons learnt.
University of Cambridge
Symposium for Andrew Pitts, Cambridge, UK, August 2023.
•
- Large-scale formal proof for the working mathematician: lessons learnt from ALEXANDRIA.
Keynote lecture for Conference on Intelligent Computer Mathematics, Cambridge, UK, September 2023.
- Formalising 21st-Century Mathematics.
London Mathematical Society / Formal Aspects of Computing evening seminar (virtual). January 2024.
- Formalising Advanced Mathematics in Isabelle/HOL.
Workshop on Prospects of Formal Mathematics, Hausdorff Centre for Mathematics, Bonn, Germany, June 2024
- Sledgehammer: a Saga.
Invited talk, Vampire Workshop, IDMC Nancy, France, June 2024
- Computer Algebra and the Formalisation of New Mathematics.
Invited talk, SC2 Workshop, IDMC Nancy, France, June 2024
And a revised, longer version presented at the Cambridge Department of Pure Mathematics in November 2024.