| 2026 | ITP | Nitro Isolation Engine: Formally Verifying a Production Hypervisor (Invited Talk). | Hanno Becker, Nathan Chong, Robert Dockins, Jim Grundy, Jason Z. S. Hu, Ike Mulder, Dominic P. Mulligan, Paul Mure, Bryan Parno, Lawrence C. Paulson, Konrad Slind |
| 2026 | ITP | From Weierstra to Dedekind via Jacobi: Formalising Foundations of Modular Forms. | Manuel Eberl, Wenda Li, Lawrence C. Paulson |
| 2025 | ITP | Formalising New Mathematics in Isabelle: Diagonal Ramsey. | Lawrence C. Paulson |
| 2024 | CPP | Formal Probabilistic Methods for Combinatorial Structures using the Lovsz Local Lemma. | Chelsea Edmonds, Lawrence C. Paulson |
| 2024 | ITP | Formalising Half of a Graduate Textbook on Number Theory (Short Paper). | Manuel Eberl, Anthony Bordg, Lawrence C. Paulson, Wenda Li |
| 2022 | CADE | Bayesian Ranking for Strategy Scheduling in Automated Theorem Provers. | Chaitanya Mangla, Sean B. Holden, Lawrence C. Paulson |
| 2022 | ITP | Formalising Fisher's Inequality: Formal Linear Algebraic Proof Techniques in Combinatorics. | Chelsea Edmonds, Lawrence C. Paulson |
| 2021 | ICLR | IsarStep: a Benchmark for High-level Mathematical Reasoning. | Wenda Li, Lei Yu, Yuhuai Wu, Lawrence C. Paulson |
| 2020 | AAAI | Bayesian Optimisation for Premise Selection in Automated Theorem Proving (Student Abstract). | Agnieszka Slowik, Chaitanya Mangla, Mateja Jamnik, Sean B. Holden, Lawrence C. Paulson |
| 2020 | CADE | Algebraically Closed Fields in Isabelle/HOL. | Paulo Emlio de Vilhena, Lawrence C. Paulson |
| 2019 | CPP | Counting polynomial roots in isabelle/hol: a formal proof of the budan-fourier theorem. | Wenda Li, Lawrence C. Paulson |
| 2017 | CPP | Porting the HOL light analysis library: some lessons (invited talk). | Lawrence C. Paulson |
| 2016 | CPP | A modular, efficient formalisation of real algebraic numbers. | Wenda Li, Lawrence C. Paulson |
| 2016 | ITP | An Isabelle/HOL Formalisation of Green's Theorem. | Mohammad Abdulaziz, Lawrence C. Paulson |
| 2016 | ITP | A Formal Proof of Cauchy's Residue Theorem. | Wenda Li, Lawrence C. Paulson |
| 2016 | SYNASC | Using Machine Learning to Decide When to Precondition Cylindrical Algebraic Decomposition with Groebner Bases. | Zongyan Huang, Matthew England, James H. Davenport, Lawrence C. Paulson |
| 2015 | CADE | A Formalisation of Finite Automata Using Hereditarily Finite Sets. | Lawrence C. Paulson |
| 2013 | SAC | Verifying multicast-based security protocols using the inductive method. | Jean Everson Martina, Lawrence C. Paulson |
| 2012 | AISC | Real Algebraic Strategies for MetiTarski Proofs. | Grant Olney Passmore, Lawrence C. Paulson, Leonardo Mendona de Moura |
| 2012 | ITP | MetiTarski: Past and Future. | Lawrence C. Paulson |
| 2011 | CADE | Extending Sledgehammer with SMT Solvers. | Jasmin Christian Blanchette, Sascha Bhme, Lawrence C. Paulson |
| 2010 | CADE | Three Years of Experience with Sledgehammer, a Practical Link between Automatic and Interactive Theorem Provers. | Lawrence C. Paulson |
| 2010 | DATE | Formal verification of analog circuits in the presence of noise and process variation. | Rajeev Narayanan, Behzad Akbarpour, Mohamed H. Zaki, Sofine Tahar, Lawrence C. Paulson |
| 2010 | LPAR | Three years of experience with Sledgehammer, a Practical Link Between Automatic and Interactive Theorem Provers. | Lawrence C. Paulson, Jasmin Christian Blanchette |
| 2009 | FMCAD | Formal verification of analog designs using MetiTarski. | William Denman, Behzad Akbarpour, Sofine Tahar, Mohamed H. Zaki, Lawrence C. Paulson |
| 2008 | AISC | MetiTarski: An Automatic Prover for the Elementary Functions. | Behzad Akbarpour, Lawrence C. Paulson |
| 2008 | CADE | LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description). | Christoph Benzmller, Lawrence C. Paulson, Frank Theiss, Arnaud Fietzke |
| 2008 | CiE | The Relative Consistency of the Axiom of Choice - Mechanized Using Isabelle/ZF. | Lawrence C. Paulson |
| 2007 | CADE | A Termination Checker for Isabelle Hoare Logic. | Jia Meng, Lawrence C. Paulson, Gerwin Klein |
| 2007 | LPAR | Extending a Resolution Prover for Inequalities on Elementary Functions. | Behzad Akbarpour, Lawrence C. Paulson |
| 2004 | CADE | Experiments on Supporting Interactive Proof Using Resolution. | Jia Meng, Lawrence C. Paulson |
| 2002 | CADE | The Reflection Theorem: A Study in Meta-theoretic Reasoning. | Lawrence C. Paulson |
| 2002 | CCS | The verification of an industrial payment protocol: the SET purchase phase. | Giampaolo Bella, Lawrence C. Paulson, Fabio Massacci |
| 2001 | CADE | SET Cardholder Registration: The Secrecy Proofs. | Lawrence C. Paulson |
| 2000 | ESORICS | Formal Verification of Cardholder Registration in SET. | Giampaolo Bella, Fabio Massacci, Lawrence C. Paulson, Piero Tramontano |
| 1999 | LICS | Proving Security Protocols Correct. | Lawrence C. Paulson |
| 1998 | AISC | Reasoning About Coding Theory: The Benefits We Get from Computer Algebra. | Clemens Ballarin, Lawrence C. Paulson |
| 1998 | CADE | A Combination of Nonstandard Analysis and Geometry Theorem Proving, with Application to Newton's Principia. | Jacques D. Fleuriot, Lawrence C. Paulson |
| 1998 | CAV | Mechanising BAN Kerberos by the Inductive Method. | Giampaolo Bella, Lawrence C. Paulson |
| 1998 | ESORICS | Kerberos Version 4: Inductive Analysis of the Secrecy Goals. | Giampaolo Bella, Lawrence C. Paulson |
| 1994 | CADE | A Fixedpoint Approach to Implementing (Co)Inductive Definitions. | Lawrence C. Paulson |
| 1992 | CADE | Isabelle-91. | Tobias Nipkow, Lawrence C. Paulson |
| 1988 | CADE | Isabelle: The Next Seven Hundred Theorem Provers. | Lawrence C. Paulson |
| 1982 | POPL | A Semantics-Directed Compiler Generator. | Lawrence C. Paulson |