- 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,
- 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,
- 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 (Summer School Marktoberdorf 1996), Springer-Verlag,
- Strategic principles in the design of Isabelle.
CADE-15 Workshop on Strategies in Automated Deduction, Lindau, Germany (1998), 11–17.
- Security protocols and their correctness.
Automated Reasoning Workshop 1998. St. Andrews, Scotland (1998)
- Proving security protocols correct.
IEEE Symposium on Logic in Computer Science. Trento, Italy (1999).
- Getting started with Isabelle.
EEF Foundations School on Deduction and Theorem Proving.
Edinburgh, Scotland (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 (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).
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.
Lawrence C. Paulson • Computer Laboratory • University of Cambridge