# 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*(1990) - Tool support for logics of programs.
*In*: M. Broy (editor),*Mathematical Methods in Program Development (*Springer-Verlag,*Summer School Marktoberdorf*, 1996),

Slides available - Strategic principles in the design of Isabelle.

*CADE-15 Workshop on Strategies in Automated Deduction,*Lindau, Germany (1998), 11–17.

Slides available - Security protocols and their correctness.

Automated Reasoning Workshop 1998. St. Andrews, Scotland (1998)

*Slides available* - Proving security protocols correct.
Trento, Italy (1999).

IEEE Symposium on Logic in Computer Science.

Slides available - Getting started with Isabelle.
. Edinburgh, Scotland (2000).

EEF Foundations School on Deduction and Theorem Proving - 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 - Verifying the SET protocol: overview.

*FASec 2002: Formal Aspects of Security*. Royal Holloway College, University of London, England, December 2002.

Slides available - Formalizing abstract mathematics: issues and progress.

Computer-Supported Mathematical Theory Development. Cork, Ireland, July 2004.

Slides available - Computational logic and the quest for greater automation.

Inaugural lecture upon conferment of the title of Distinguished Affiliated Professor, Munich, Germany (2006).

Slides available - Automated assistance for proof assistants.

Colloquium in Honour of Gérard Huet, Paris, France, June 2007.

Slides available - 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.

Slides available - 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 - MetiTarski: past and future.

Interactive Theorem Proving — ITP 2012

Princeton, New Jersey, August 2012.

Publisher's version at www.springerlink.com • Slides available - 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.

Publisher's version at www.springerlink.com • Slides available - Theorem proving and the real numbers: overview and challenges.

Keynote lecture for*NASA Formal Methods*.

Houston, Texas, April 2014. Slides available - Automated theorem proving for special functions: the next phase.

Keynote lecture for SNC 2014 (*Symbolic-Numeric Computation*).

Shanghai, China, July 2014.

Slides available - The future of formalised mathematics.

Keynote lecture for EACA 2016 (XV Encuentro de Álgebra Computacional y Aplicaciones). Logroño, Spain, June 2016.

Slides available - 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 - Proof assistants: from symbolic logic to real mathematics?

"Jacques Morgenstern" Colloquium.

Inria Sophia-Antipolis, France, May 2017. Slides available - 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. Slides available - A career in research: Mike Gordon and hardware verification.

Automated Reasoning Workshop.

Cambridge, UK, April 2018. Slides available - Formalising mathematics in simple type theory.

*Big Proof*programme, International Centre for Mathematical Sciences.

Edinburgh, UK, May 2019. Slides available - 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 - Doing Mathematics with simple types:
infinitary combinatorics in Isabelle/HOL.

Harvard University Center Of Mathematical Sciences and Applications (virtual), March 2021.

Slides available - Formalising contemporary mathematics in simple type theory.

Topos Institute Colloquium (virtual), July 2021.

Slides available - Formalised mathematics: obstacles and achievements.

Zhejiang University (virtual), September 2021.

Slides on types • Slides on formalising mathematics - Automated theorem proving: a technology roadmap.

Huawei Mathematical Theorem Proving Workshop. Cambridge, UK, April 2022.

Slides available - Formalising Erdős and Larson: ordinal partition theory.

Leeds Logic Seminar, University of Leeds, UK, March 2023.

Slides available - Formalising a number theory textbook: lessons learnt.

University of Cambridge Symposium for Andrew Pitts, Cambridge, UK, August 2023.

Slides available • 20-minute video - 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 - Formalising 21st-Century Mathematics.

London Mathematical Society / Formal Aspects of Computing evening seminar (virtual). January 2024.

Slides available