Lawrence C. Paulson

Orcid: 0000-0003-0288-4279

Affiliations:
  • University of Cambridge, UK


According to our database1, Lawrence C. Paulson authored at least 187 papers between 1981 and 2024.

Collaborative distances:
  • Dijkstra number2 of two.
  • Erdős number3 of three.

Awards

ACM Fellow

ACM Fellow 2008, "For contributions to theorem provers and verification techniques.".

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Dataset
Other 

Links

Online presence:

On csauthors.net:

Bibliography

2024
A formalised theorem in the partition calculus.
Ann. Pure Appl. Log., January, 2024

Formal Probabilistic Methods for Combinatorial Structures using the Lovász Local Lemma.
Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2024

2023
Formalising Szemerédi's Regularity Lemma and Roth's Theorem on Arithmetic Progressions in Isabelle/HOL.
J. Autom. Reason., 2023

Formal Probabilistic Methods for Combinatorial Structures in Isabelle/HOL.
CoRR, 2023

Knuth-Morris-Pratt String Search.
Arch. Formal Proofs, 2023

Euler's Polyhedron Formula.
Arch. Formal Proofs, 2023

Hypergraph Colouring Bounds.
Arch. Formal Proofs, 2023

Large-Scale Formal Proof for the Working Mathematician - Lessons Learnt from the ALEXANDRIA Project.
Proceedings of the Intelligent Computer Mathematics - 16th International Conference, 2023

2022
Formal Verification of Transcendental Fixed- and Floating-point Algorithms using an Automatic Theorem Prover.
Formal Aspects Comput., 2022

Irrationality and Transcendence Criteria for Infinite Series in Isabelle/HOL.
Exp. Math., 2022

Formalizing Ordinal Partition Relations Using Isabelle/HOL.
Exp. Math., 2022

Simple Type Theory is not too Simple: Grothendieck's Schemes Without Dependent Types.
Exp. Math., 2022

Mathematical Proof Between Generations.
CoRR, 2022

Ackermann's Function Is Not Primitive Recursive.
Arch. Formal Proofs, 2022

Wetzel's Problem and the Continuum Hypothesis.
Arch. Formal Proofs, 2022

Young's Inequality for Increasing Functions.
Arch. Formal Proofs, 2022

Irrational numbers from THE BOOK.
Arch. Formal Proofs, 2022

Khovanskii's Theorem.
Arch. Formal Proofs, 2022

The Plünnecke-Ruzsa Inequality.
Arch. Formal Proofs, 2022

Constructing the Reals as Dedekind Cuts of Rationals.
Arch. Formal Proofs, 2022

Fisher's Inequality: Linear Algebraic Proof Techniques for Combinatorics.
Arch. Formal Proofs, 2022

Wetzel: Formalisation of an Undecidable Problem Linked to the Continuum Hypothesis.
Proceedings of the Intelligent Computer Mathematics - 15th International Conference, 2022

Formalising Fisher's Inequality: Formal Linear Algebraic Proof Techniques in Combinatorics.
Proceedings of the 13th International Conference on Interactive Theorem Proving, 2022

Bayesian Ranking for Strategy Scheduling in Automated Theorem Provers.
Proceedings of the Automated Reasoning - 11th International Joint Conference, 2022

2021
Ackermann's function in iterative Form: a Proof Assistant Experiment.
Bull. Symb. Log., 2021

Combinatorial Design Theory.
Arch. Formal Proofs, 2021

Roth's Theorem on Arithmetic Progressions.
Arch. Formal Proofs, 2021

Szemerédi's Regularity Lemma.
Arch. Formal Proofs, 2021

Grothendieck's Schemes in Algebraic Geometry.
Arch. Formal Proofs, 2021

A Modular First Formalisation of Combinatorial Design Theory.
Proceedings of the Intelligent Computer Mathematics - 14th International Conference, 2021

IsarStep: a Benchmark for High-level Mathematical Reasoning.
Proceedings of the 9th International Conference on Learning Representations, 2021

2020
Evaluating Winding Numbers and Counting Complex Roots Through Cauchy Indices in Isabelle/HOL.
J. Autom. Reason., 2020

Modelling High-Level Mathematical Reasoning in Mechanised Declarative Proofs.
CoRR, 2020

Ordinal Partitions.
Arch. Formal Proofs, 2020

The Nash-Williams Partition Theorem.
Arch. Formal Proofs, 2020

Bayesian Optimisation of Solver Parameters in CBMC.
Proceedings of the 18th International Workshop on Satisfiability Modulo Theories co-located with the 10th International Joint Conference on Automated Reasoning (IJCAR 2020), 2020

Algebraically Closed Fields in Isabelle/HOL.
Proceedings of the Automated Reasoning - 10th International Joint Conference, 2020

Bayesian Optimisation for Premise Selection in Automated Theorem Proving (Student Abstract).
Proceedings of the Thirty-Fourth AAAI Conference on Artificial Intelligence, 2020

2019
Using Machine Learning to Improve Cylindrical Algebraic Decomposition.
Math. Comput. Sci., 2019

Deciding Univariate Polynomial Problems Using Untrusted Certificates in Isabelle/HOL.
J. Autom. Reason., 2019

From LCF to Isabelle/HOL.
Formal Aspects Comput., 2019

Bayesian Optimisation with Gaussian Processes for Premise Selection.
CoRR, 2019

Zermelo Fraenkel Set Theory in Higher-Order Logic.
Arch. Formal Proofs, 2019

Fourier Series.
Arch. Formal Proofs, 2019

Bayesian Optimisation for Heuristic Configuration in Automated Theorem Proving.
Proceedings of the Vampire 2018 and Vampire 2019. The 5th and 6th Vampire Workshops, 2019

Counting polynomial roots in isabelle/hol: a formal proof of the budan-fourier theorem.
Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2019

2018
Introduction to Milestones in Interactive Theorem Proving.
J. Autom. Reason., 2018

Michael John Caldwell Gordon (FRS 1994), 28 February 1948 - 22 August 2017.
CoRR, 2018

Using Machine Learning to Improve Cylindrical Algebraic Decomposition.
CoRR, 2018

Formalising Mathematics In Simple Type Theory.
CoRR, 2018

Quaternions.
Arch. Formal Proofs, 2018

The Prime Number Theorem.
Arch. Formal Proofs, 2018

An Isabelle/HOL formalisation of Green's Theorem.
Arch. Formal Proofs, 2018

2017
Computational Logic: Its Origins and Applications.
CoRR, 2017

Porting the HOL light analysis library: some lessons (invited talk).
Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, 2017

2016
Hammering towards QED.
J. Formaliz. Reason., 2016

The Cartan Fixed Point Theorems.
Arch. Formal Proofs, 2016

Source Coding Theorem.
Arch. Formal Proofs, 2016

Using Machine Learning to Decide When to Precondition Cylindrical Algebraic Decomposition with Groebner Bases.
Proceedings of the 18th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, 2016

A Formal Proof of Cauchy's Residue Theorem.
Proceedings of the Interactive Theorem Proving - 7th International Conference, 2016

A modular, efficient formalisation of real algebraic numbers.
Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, 2016

2015
A Mechanised Proof of Gödel's Incompleteness Theorems Using Nominal Isabelle.
J. Autom. Reason., 2015

The Higher-Order Prover Leo-II.
J. Autom. Reason., 2015

Verifying multicast-based security protocols using the inductive method.
Int. J. Inf. Sec., 2015

A Complete Decision Procedure for Univariate Polynomial Problems in Isabelle/HOL.
CoRR, 2015

Finite Automata in Hereditarily Finite Set Theory.
Arch. Formal Proofs, 2015

Proofs and Reconstructions.
Proceedings of the Frontiers of Combining Systems - 10th International Symposium, 2015

A Formalisation of Finite Automata Using Hereditarily Finite Sets.
Proceedings of the Automated Deduction - CADE-25, 2015

2014
A Machine-Assisted Proof of Gödel's Incompleteness theorems for the Theory of Hereditarily Finite Sets.
Rev. Symb. Log., 2014

Machine Learning for First-Order Theorem Proving - Learning to Select a Good Heuristic.
J. Autom. Reason., 2014

A comparison of three heuristics to choose the variable ordering for CAD.
CoRR, 2014

A Comparison of Three Heuristics to Choose the Variable Ordering for Cylindrical Algebraic Decomposition.
ACM Commun. Comput. Algebra, 2014

Real-Valued Special Functions: Upper and Lower Bounds.
Arch. Formal Proofs, 2014

Automated theorem proving for special functions: the next phase.
Proceedings of the Symbolic-Numeric Computation 2014, 2014

Verifying Hybrid Systems Involving Transcendental Functions.
Proceedings of the NASA Formal Methods - 6th International Symposium, NFM 2014, Houston, TX, USA, April 29, 2014

Applying Machine Learning to the Problem of Choosing a Heuristic to Select the Variable Ordering for Cylindrical Algebraic Decomposition.
Proceedings of the Intelligent Computer Mathematics - International Conference, 2014

2013
First-order theorem proving.
Dataset, April, 2013

Quantified Multimodal Logics in Simple Type Theory.
Logica Universalis, 2013

Case Splitting in an Automatic Theorem Prover for Real-Valued Special Functions.
J. Autom. Reason., 2013

Extending Sledgehammer with SMT Solvers.
J. Autom. Reason., 2013

LEO-II and Satallax on the Sledgehammer test bench.
J. Appl. Log., 2013

The Hereditarily Finite Sets.
Arch. Formal Proofs, 2013

Gödel's Incompleteness Theorems.
Arch. Formal Proofs, 2013

MetiTarski's Menagerie of Cooperating Systems.
Proceedings of the Frontiers of Combining Systems, 2013

2012
Proving the Impossibility of Trisecting an Angle and Doubling the Cube.
Arch. Formal Proofs, 2012

MetiTarski: Past and Future.
Proceedings of the Interactive Theorem Proving - Third International Conference, 2012

Real Algebraic Strategies for MetiTarski Proofs.
Proceedings of the Intelligent Computer Mathematics - 11th International Conference, 2012

2010
Functional Programming in ML.
Proceedings of the Encyclopedia of Software Engineering, 2010

MetiTarski: An Automatic Theorem Prover for Real-Valued Special Functions.
J. Autom. Reason., 2010

Multimodal and intuitionistic logics in simple type theory.
Log. J. IGPL, 2010

Three years of experience with Sledgehammer, a Practical Link Between Automatic and Interactive Theorem Provers.
Proceedings of the 8th International Workshop on the Implementation of Logics, 2010

Formal verification of analog circuits in the presence of noise and process variation.
Proceedings of the Design, Automation and Test in Europe, 2010

Three Years of Experience with Sledgehammer, a Practical Link between Automatic and Interactive Theorem Provers.
Proceedings of the 2nd Workshop on Practical Aspects of Automated Reasoning, 2010

2009
Lightweight relevance filtering for machine-generated resolution problems.
J. Appl. Log., 2009

Applications of MetiTarski in the Verification of Control and Hybrid Systems.
Proceedings of the Hybrid Systems: Computation and Control, 12th International Conference, 2009

Formal verification of analog designs using MetiTarski.
Proceedings of 9th International Conference on Formal Methods in Computer-Aided Design, 2009

2008
Translating Higher-Order Clauses to First-Order Clauses.
J. Autom. Reason., 2008

Fun With Tilings.
Arch. Formal Proofs, 2008

The Isabelle Framework.
Proceedings of the Theorem Proving in Higher Order Logics, 21st International Conference, 2008

The Relative Consistency of the Axiom of Choice - Mechanized Using Isabelle/ZF.
Proceedings of the Logic and Theory of Algorithms, 2008

LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description).
Proceedings of the Automated Reasoning, 4th International Joint Conference, 2008

MetiTarski: An Automatic Prover for the Elementary Functions.
Proceedings of the Intelligent Computer Mathematics, 9th International Conference, 2008

2007
Preface.
J. Autom. Reason., 2007

Source-Level Proof Reconstruction for Interactive Theorem Proving.
Proceedings of the Theorem Proving in Higher Order Logics, 20th International Conference, 2007

Extending a Resolution Prover for Inequalities on Elementary Functions.
Proceedings of the Logic for Programming, 2007

A Termination Checker for Isabelle Hoare Logic.
Proceedings of 4th International Verification Workshop in connection with CADE-21, 2007

2006
Defining functions on equivalence classes.
ACM Trans. Comput. Log., 2006

Accountability protocols: Formalized and verified.
ACM Trans. Inf. Syst. Secur., 2006

Verifying the SET Purchase Protocols.
J. Autom. Reason., 2006

Erratum to "Automation for interactive proof: First prototype" [Inform. and Comput. 204(2006) 1575-1596].
Inf. Comput., 2006

Automation for interactive proof: First prototype.
Inf. Comput., 2006

Isabelle/Isar.
Proceedings of the Seventeen Provers of the World, Foreword by Dana S. Scott, 2006

2005
An overview of the verification of SET.
Int. J. Inf. Sec., 2005

Mechanizing compositional reasoning for concurrent systems: some lessons.
Formal Aspects Comput., 2005

Proof Pearl: Defining Functions over Finite Sets.
Proceedings of the Theorem Proving in Higher Order Logics, 18th International Conference, 2005

2004
Organizing Numerical Theories Using Axiomatic Type Classes.
J. Autom. Reason., 2004

Experiments on Supporting Interactive Proof Using Resolution.
Proceedings of the Automated Reasoning - Second International Joint Conference, 2004

2003
Verifying the SET registration protocols.
IEEE J. Sel. Areas Commun., 2003

Verifying Second-Level Security Protocols.
Proceedings of the Theorem Proving in Higher Order Logics, 16th International Conference, 2003

Is the Verification Problem for Cryptographic Protocols Solved?.
Proceedings of the Security Protocols, 2003

2002
Analyzing Delegation Properties.
Proceedings of the Security Protocols, 2002

Program Composition in Isabelle/UNITY.
Proceedings of the 16th International Parallel and Distributed Processing Symposium (IPDPS 2002), 2002

Verifying the SET Protocol: Overview.
Proceedings of the Formal Aspects of Security, First International Conference, 2002

The verification of an industrial payment protocol: the SET purchase phase.
Proceedings of the 9th ACM Conference on Computer and Communications Security, 2002

The Reflection Theorem: A Study in Meta-theoretic Reasoning.
Proceedings of the Automated Deduction, 2002

Isabelle/HOL - A Proof Assistant for Higher-Order Logic
Lecture Notes in Computer Science 2283, Springer, ISBN: 3-540-43376-7, 2002

2001
Mechanizing a theory of program composition for UNITY.
ACM Trans. Program. Lang. Syst., 2001

Relations Between Secrets: Two Formal Analyses of the Yahalom Protocol.
J. Comput. Secur., 2001

A Simple Formalization and Proof for the Mutilated Chess Board.
Log. J. IGPL, 2001

Mechanical Proofs about a Non-repudiation Protocol.
Proceedings of the Theorem Proving in Higher Order Logics, 14th International Conference, 2001

A Proof of Non-repudiation (Transcript of Discussion).
Proceedings of the Security Protocols, 2001

A Proof of Non-repudiation.
Proceedings of the Security Protocols, 2001

SET Cardholder Registration: The Secrecy Proofs.
Proceedings of the Automated Reasoning, First International Joint Conference, 2001

2000
Mechanizing UNITY in Isabelle.
ACM Trans. Comput. Log., 2000

Making Sense of Specifications: The Formalization of SET (Transcript of Discussion).
Proceedings of the Security Protocols, 2000

Making Sense of Specifications: The Formalization of SET.
Proceedings of the Security Protocols, 2000

Formal Verification of Cardholder Registration in SET.
Proceedings of the Computer Security, 2000

A fixedpoint approach to (co)inductive and (co)datatype definitions.
Proceedings of the Proof, Language, and Interaction, Essays in Honour of Robin Milner, 2000

1999
Should your specification language be typed.
ACM Trans. Program. Lang. Syst., 1999

Inductive Analysis of the Internet Protocol TLS.
ACM Trans. Inf. Syst. Secur., 1999

Final coalgebras as greatest fixed points in ZF set theory.
Math. Struct. Comput. Sci., 1999

A Generic Tableau Prover and its Integration with Isabelle.
J. Univers. Comput. Sci., 1999

A Formal Proof of Sylow's Theorem.
J. Autom. Reason., 1999

A Pragmatic Approach to Extending Provers by Computer Algebra - with Applications to Coding Theory.
Fundam. Informaticae, 1999

Locales - A Sectioning Concept for Isabelle.
Proceedings of the Theorem Proving in Higher Order Logics, 12th International Conference, 1999

Relatios Between Secrets: The Yahalom Protocol.
Proceedings of the Security Protocols, 1999

Proving Security Protocols Correct.
Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science, 1999

1998
The Inductive Approach to Verifying Cryptographic Protocols.
J. Comput. Secur., 1998

Inductive Analysis of the Internet Protocol TLS (Transcript of Discussion).
Proceedings of the Security Protocols, 1998

Inductive Analysis of the Internet Protocol TLS (Position Paper).
Proceedings of the Security Protocols, 1998

Kerberos Version 4: Inductive Analysis of the Secrecy Goals.
Proceedings of the Computer Security, 1998

Mechanising BAN Kerberos by the Inductive Method.
Proceedings of the Computer Aided Verification, 10th International Conference, 1998

A Combination of Nonstandard Analysis and Geometry Theorem Proving, with Application to Newton's Principia.
Proceedings of the Automated Deduction, 1998

Reasoning About Coding Theory: The Benefits We Get from Computer Algebra.
Proceedings of the Artificial Intelligence and Symbolic Computation, 1998

Proving Newton's Propositio Kepleriana Using Geometry and Nonstandard Analysis in Isabelle.
Proceedings of the Automated Deduction in Geometry, 1998

1997
Mechanizing Coinduction and Corecursion in Higher-Order Logic.
J. Log. Comput., 1997

Generic Automatic Proof Tools
CoRR, 1997

Mechanized proofs for a recursive authentication protocol.
Proceedings of the 10th Computer Security Foundations Workshop (CSFW '97), 1997

Proving Properties of Security Protocols by Induction.
Proceedings of the 10th Computer Security Foundations Workshop (CSFW '97), 1997

1996
Mechanizing Set Theory.
J. Autom. Reason., 1996

Mechanizing Set Theory: Cardinal Arithmetic and the Axiom of Choice.
CoRR, 1996

ML for the working programmer (2. ed.).
Cambridge University Press, ISBN: 978-0-521-57050-3, 1996

1995
Set Theory for Verification. II: Induction and Recursion.
J. Autom. Reason., 1995

1994
A Concrete Final Coalgebra Theorem for ZF Set Theory.
Proceedings of the Types for Proofs and Programs, 1994

A Fixedpoint Approach to Implementing (Co)Inductive Definitions.
Proceedings of the Automated Deduction - CADE-12, 12th International Conference on Automated Deduction, Nancy, France, June 26, 1994

Isabelle - A Generic Theorem Prover (with a contribution by T. Nipkow)
Lecture Notes in Computer Science 828, Springer, ISBN: 3-540-58244-4, 1994

1993
Set Theory for Verification: I. From Foundations to Functions.
J. Autom. Reason., 1993

Designing a Theorem Prover
CoRR, 1993

Isabelle: The Next 700 Theorem Provers
CoRR, 1993

Proving Termination of Normalization Functions for Conditional Expressions
CoRR, 1993

1992
Isabelle-91.
Proceedings of the Automated Deduction, 1992

1991
ML for the working programmer.
Cambridge University Press, ISBN: 978-0-521-39022-4, 1991

1989
The Foundation of a Generic Theorem Prover.
J. Autom. Reason., 1989

Logic Programming, Functional Programming, and Inductive Definitions.
Proceedings of the Extensions of Logic Programming, 1989

1988
A formulation of the simple theory of types (for Isabelle).
Proceedings of the COLOG-88, 1988

Isabelle: The Next Seven Hundred Theorem Provers.
Proceedings of the 9th International Conference on Automated Deduction, 1988

1987
Logic and computation - interactive proof with Cambridge LCF.
Cambridge tracts in theoretical computer science 2, Cambridge University Press, ISBN: 978-0-521-34632-0, 1987

1986
Constructing Recursion Operators in Intuitionistic Type Theory.
J. Symb. Comput., 1986

Natural Deduction as Higher-Order Resolution.
J. Log. Program., 1986

Proving Termination of Normalization Functions for Conditional Experessions.
J. Autom. Reason., 1986

1985
Verifying the Unification Algorithm in LCF.
Sci. Comput. Program., 1985

Lessons Learned from LCF: A Survey of Natural Deduction Proofs.
Comput. J., 1985

1984
Deriving Structural Induction in LCF.
Proceedings of the Semantics of Data Types, International Symposium, 1984

1983
A Higher-Order Implementation of Rewriting.
Sci. Comput. Program., 1983

Compiler Generation from Denotational Semantics.
Proceedings of the Method and tools for compiler construction, 1983

1982
A Semantics-Directed Compiler Generator.
Proceedings of the Conference Record of the Ninth Annual ACM Symposium on Principles of Programming Languages, 1982

1981
A compiler generator for semantic grammars.
PhD thesis, 1981


  Loading...