Stop the war!Остановите войну!
for scientists:
default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDLawrence C. Paulson
Person information
- affiliation: University of Cambridge, UK
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
showing all ?? records
2020 – today
- 2023
[j86]Chelsea Edmonds
, Angeliki Koutsoukou-Argyraki, Lawrence C. Paulson:
Formalising Szemerédi's Regularity Lemma and Roth's Theorem on Arithmetic Progressions in Isabelle/HOL. J. Autom. Reason. 67(1): 2 (2023)- [c76]Lawrence C. Paulson:
Large-Scale Formal Proof for the Working Mathematician - Lessons Learnt from the ALEXANDRIA Project. CICM 2023: 3-15 - 2022
- [j85]Chelsea Edmonds, Lawrence C. Paulson:
Fisher's Inequality: Linear Algebraic Proof Techniques for Combinatorics. Arch. Formal Proofs 2022 (2022) - [j84]Jacques D. Fleuriot, Lawrence C. Paulson:
Constructing the Reals as Dedekind Cuts of Rationals. Arch. Formal Proofs 2022 (2022) - [j83]Angeliki Koutsoukou-Argyraki, Lawrence C. Paulson:
The Plünnecke-Ruzsa Inequality. Arch. Formal Proofs 2022 (2022) - [j82]Angeliki Koutsoukou-Argyraki, Lawrence C. Paulson:
Khovanskii's Theorem. Arch. Formal Proofs 2022 (2022) - [j81]Lawrence C. Paulson:
Irrational numbers from THE BOOK. Arch. Formal Proofs 2022 (2022) - [j80]Lawrence C. Paulson:
Young's Inequality for Increasing Functions. Arch. Formal Proofs 2022 (2022) - [j79]Lawrence C. Paulson:
Wetzel's Problem and the Continuum Hypothesis. Arch. Formal Proofs 2022 (2022) - [j78]Lawrence C. Paulson:
Ackermann's Function Is Not Primitive Recursive. Arch. Formal Proofs 2022 (2022) - [j77]Anthony Bordg, Lawrence C. Paulson, Wenda Li:
Simple Type Theory is not too Simple: Grothendieck's Schemes Without Dependent Types. Exp. Math. 31(2): 364-382 (2022) - [j76]Mirna Dzamonja, Angeliki Koutsoukou-Argyraki, Lawrence C. Paulson:
Formalizing Ordinal Partition Relations Using Isabelle/HOL. Exp. Math. 31(2): 383-400 (2022) - [j75]Angeliki Koutsoukou-Argyraki, Wenda Li, Lawrence C. Paulson:
Irrationality and Transcendence Criteria for Infinite Series in Isabelle/HOL. Exp. Math. 31(2): 401-412 (2022) - [j74]Samuel Coward, Lawrence C. Paulson, Theo Drane, Emiliano Morini:
Formal Verification of Transcendental Fixed- and Floating-point Algorithms using an Automatic Theorem Prover. Formal Aspects Comput. 34(2): 1-22 (2022) - [c75]Chaitanya Mangla, Sean B. Holden, Lawrence C. Paulson:
Bayesian Ranking for Strategy Scheduling in Automated Theorem Provers. IJCAR 2022: 559-577 - [c74]Chelsea Edmonds, Lawrence C. Paulson:
Formalising Fisher's Inequality: Formal Linear Algebraic Proof Techniques in Combinatorics. ITP 2022: 11:1-11:19 - [c73]Lawrence C. Paulson:
Wetzel: Formalisation of an Undecidable Problem Linked to the Continuum Hypothesis. CICM 2022: 92-106 - [i44]Lawrence C. Paulson:
Wetzel: Formalisation of an Undecidable Problem Linked to the Continuum Hypothesis. CoRR abs/2205.03159 (2022) - [i43]Chelsea Edmonds, Lawrence C. Paulson:
Formalising Fisher's Inequality: Formal Linear Algebraic Proof Techniques in Combinatorics. CoRR abs/2207.02728 (2022) - [i42]Jonas Bayer, Christoph Benzmüller, Kevin Buzzard, Marco David, Leslie Lamport, Yuri V. Matiyasevich, Lawrence C. Paulson, Dierk Schleicher, Benedikt Stock, Efim I. Zelmanov:
Mathematical Proof Between Generations. CoRR abs/2207.04779 (2022) - [i41]Chelsea Edmonds, Angeliki Koutsoukou-Argyraki, Lawrence C. Paulson:
Formalising Szemerédi's Regularity Lemma and Roth's Theorem on Arithmetic Progressions in Isabelle/HOL. CoRR abs/2207.07499 (2022) - 2021
- [j73]Anthony Bordg, Lawrence C. Paulson, Wenda Li:
Grothendieck's Schemes in Algebraic Geometry. Arch. Formal Proofs 2021 (2021) - [j72]Chelsea Edmonds, Angeliki Koutsoukou-Argyraki, Lawrence C. Paulson:
Szemerédi's Regularity Lemma. Arch. Formal Proofs 2021 (2021) - [j71]Chelsea Edmonds, Angeliki Koutsoukou-Argyraki, Lawrence C. Paulson:
Roth's Theorem on Arithmetic Progressions. Arch. Formal Proofs 2021 (2021) - [j70]Chelsea Edmonds, Lawrence C. Paulson:
Combinatorial Design Theory. Arch. Formal Proofs 2021 (2021) - [j69]Lawrence C. Paulson:
Ackermann's function in iterative Form: a Proof Assistant Experiment. Bull. Symb. Log. 27(4): 426-435 (2021) - [c72]Wenda Li, Lei Yu, Yuhuai Wu, Lawrence C. Paulson:
IsarStep: a Benchmark for High-level Mathematical Reasoning. ICLR 2021 - [c71]Chelsea Edmonds, Lawrence C. Paulson:
A Modular First Formalisation of Combinatorial Design Theory. CICM 2021: 3-18 - [i40]Angeliki Koutsoukou-Argyraki, Wenda Li, Lawrence C. Paulson:
Irrationality and Transcendence Criteria for Infinite Series in Isabelle/HOL. CoRR abs/2101.05257 (2021) - [i39]Anthony Bordg, Lawrence C. Paulson, Wenda Li:
Simple Type Theory is not too Simple: Grothendieck's Schemes without Dependent Types. CoRR abs/2104.09366 (2021) - [i38]Lawrence C. Paulson:
Ackermann's Function in Iterative Form: A Proof Assistant Experiment. CoRR abs/2104.11157 (2021) - [i37]Lawrence C. Paulson:
The Relative Consistency of the Axiom of Choice Mechanized Using Isabelle/ZF. CoRR abs/2104.12674 (2021) - [i36]Lawrence C. Paulson:
A Mechanised Proof of Gödel's Incompleteness Theorems using Nominal Isabelle. CoRR abs/2104.13792 (2021) - [i35]Lawrence C. Paulson:
The Inductive Approach to Verifying Cryptographic Protocols. CoRR abs/2105.06319 (2021) - [i34]Chelsea Edmonds, Lawrence C. Paulson:
A Modular First Formalisation of Combinatorial Design Theory. CoRR abs/2105.13583 (2021) - 2020
- [j68]Lawrence C. Paulson:
The Nash-Williams Partition Theorem. Arch. Formal Proofs 2020 (2020) - [j67]Lawrence C. Paulson:
Ordinal Partitions. Arch. Formal Proofs 2020 (2020) - [j66]Wenda Li, Lawrence C. Paulson:
Evaluating Winding Numbers and Counting Complex Roots Through Cauchy Indices in Isabelle/HOL. J. Autom. Reason. 64(2): 331-360 (2020) - [c70]Agnieszka Slowik, Chaitanya Mangla, Mateja Jamnik, Sean B. Holden, Lawrence C. Paulson:
Bayesian Optimisation for Premise Selection in Automated Theorem Proving (Student Abstract). AAAI 2020: 13919-13920 - [c69]Paulo Emílio de Vilhena, Lawrence C. Paulson:
Algebraically Closed Fields in Isabelle/HOL. IJCAR (2) 2020: 204-220 - [c68]Chaitanya Mangla, Sean B. Holden, Lawrence C. Paulson:
Bayesian Optimisation of Solver Parameters in CBMC. SMT 2020: 37-47 - [i33]Wenda Li, Lei Yu, Yuhuai Wu, Lawrence C. Paulson:
Modelling High-Level Mathematical Reasoning in Mechanised Declarative Proofs. CoRR abs/2006.09265 (2020)
2010 – 2019
- 2019
- [j65]Lawrence C. Paulson:
Fourier Series. Arch. Formal Proofs 2019 (2019) - [j64]Lawrence C. Paulson:
Zermelo Fraenkel Set Theory in Higher-Order Logic. Arch. Formal Proofs 2019 (2019) - [j63]Lawrence C. Paulson, Tobias Nipkow, Makarius Wenzel:
From LCF to Isabelle/HOL. Formal Aspects Comput. 31(6): 675-698 (2019) - [j62]Wenda Li, Grant Olney Passmore, Lawrence C. Paulson:
Deciding Univariate Polynomial Problems Using Untrusted Certificates in Isabelle/HOL. J. Autom. Reason. 62(1): 69-91 (2019) - [j61]Mohammad Abdulaziz, Lawrence C. Paulson:
An Isabelle/HOL Formalisation of Green's Theorem. J. Autom. Reason. 63(3): 763-786 (2019) - [j60]Zongyan Huang, Matthew England, David J. Wilson, James P. Bridge, James H. Davenport, Lawrence C. Paulson:
Using Machine Learning to Improve Cylindrical Algebraic Decomposition. Math. Comput. Sci. 13(4): 461-488 (2019) - [c67]Wenda Li, Lawrence C. Paulson:
Counting polynomial roots in isabelle/hol: a formal proof of the budan-fourier theorem. CPP 2019: 52-64 - [c66]Agnieszka Slowik, Chaitanya Mangla, Mateja Jamnik, Sean B. Holden, Lawrence C. Paulson:
Bayesian Optimisation for Heuristic Configuration in Automated Theorem Proving. Vampire 2019: 45-51 - [i32]Lawrence C. Paulson, Tobias Nipkow, Makarius Wenzel:
From LCF to Isabelle/HOL. CoRR abs/1907.02836 (2019) - [i31]Lawrence C. Paulson:
Inductive Analysis of the Internet Protocol TLS. CoRR abs/1907.07559 (2019) - [i30]Lawrence C. Paulson:
Defining Functions on Equivalence Classes. CoRR abs/1907.07591 (2019) - [i29]Agnieszka Slowik, Chaitanya Mangla, Mateja Jamnik, Sean B. Holden, Lawrence C. Paulson:
Bayesian Optimisation with Gaussian Processes for Premise Selection. CoRR abs/1909.09137 (2019) - 2018
- [j59]Mohammad Abdulaziz, Lawrence C. Paulson:
An Isabelle/HOL formalisation of Green's Theorem. Arch. Formal Proofs 2018 (2018) - [j58]Manuel Eberl, Lawrence C. Paulson:
The Prime Number Theorem. Arch. Formal Proofs 2018 (2018) - [j57]Lawrence C. Paulson:
Quaternions. Arch. Formal Proofs 2018 (2018) - [j56]Jeremy Avigad, Jasmin Christian Blanchette, Gerwin Klein, Lawrence C. Paulson, Andrei Popescu, Gregor Snelting:
Introduction to Milestones in Interactive Theorem Proving. J. Autom. Reason. 61(1-4): 1-8 (2018) - [i28]Wenda Li, Lawrence C. Paulson:
Evaluating Winding Numbers and Counting Complex Roots through Cauchy Indices in Isabelle/HOL. CoRR abs/1804.03922 (2018) - [i27]Lawrence C. Paulson:
Formalising Mathematics In Simple Type Theory. CoRR abs/1804.07860 (2018) - [i26]Zongyan Huang, Matthew England, David J. Wilson, James H. Davenport, Lawrence C. Paulson:
Using Machine Learning to Improve Cylindrical Algebraic Decomposition. CoRR abs/1804.10520 (2018) - [i25]Lawrence C. Paulson:
Michael John Caldwell Gordon (FRS 1994), 28 February 1948 - 22 August 2017. CoRR abs/1806.04002 (2018) - [i24]Wenda Li, Lawrence C. Paulson:
Counting Polynomial Roots in Isabelle/HOL: A Formal Proof of the Budan-Fourier Theorem. CoRR abs/1811.11093 (2018) - 2017
- [c65]Lawrence C. Paulson:
Porting the HOL light analysis library: some lessons (invited talk). CPP 2017: 1 - [i23]Lawrence C. Paulson:
Computational Logic: Its Origins and Applications. CoRR abs/1712.04375 (2017) - 2016
- [j55]Quentin Hibon, Lawrence C. Paulson:
Source Coding Theorem. Arch. Formal Proofs 2016 (2016) - [j54]Lawrence C. Paulson:
The Cartan Fixed Point Theorems. Arch. Formal Proofs 2016 (2016) - [j53]Jasmin Christian Blanchette, Cezary Kaliszyk, Lawrence C. Paulson, Josef Urban:
Hammering towards QED. J. Formaliz. Reason. 9(1): 101-148 (2016) - [c64]Wenda Li, Lawrence C. Paulson:
A modular, efficient formalisation of real algebraic numbers. CPP 2016: 66-75 - [c63]Mohammad Abdulaziz, Lawrence C. Paulson:
An Isabelle/HOL Formalisation of Green's Theorem. ITP 2016: 3-19 - [c62]Wenda Li, Lawrence C. Paulson:
A Formal Proof of Cauchy's Residue Theorem. ITP 2016: 235-251 - [c61]Zongyan Huang, Matthew England, James H. Davenport, Lawrence C. Paulson:
Using Machine Learning to Decide When to Precondition Cylindrical Algebraic Decomposition with Groebner Bases. SYNASC 2016: 45-52 - [i22]Zongyan Huang, Matthew England, James H. Davenport, Lawrence C. Paulson:
Using Machine Learning to Decide When to Precondition Cylindrical Algebraic Decomposition With Groebner Bases. CoRR abs/1608.04219 (2016) - 2015
- [j52]Lawrence C. Paulson:
Finite Automata in Hereditarily Finite Set Theory. Arch. Formal Proofs 2015 (2015) - [j51]Jean Everson Martina, Lawrence C. Paulson:
Verifying multicast-based security protocols using the inductive method. Int. J. Inf. Sec. 14(2): 187-204 (2015) - [j50]Lawrence C. Paulson:
A Mechanised Proof of Gödel's Incompleteness Theorems Using Nominal Isabelle. J. Autom. Reason. 55(1): 1-37 (2015) - [j49]Christoph Benzmüller, Nik Sultana, Lawrence C. Paulson, Frank Theiss:
The Higher-Order Prover Leo-II. J. Autom. Reason. 55(4): 389-404 (2015) - [c60]Lawrence C. Paulson:
A Formalisation of Finite Automata Using Hereditarily Finite Sets. CADE 2015: 231-245 - [c59]Nik Sultana, Christoph Benzmüller, Lawrence C. Paulson:
Proofs and Reconstructions. FroCos 2015: 256-271 - [i21]Lawrence C. Paulson:
A Formalisation of Finite Automata using Hereditarily Finite Sets. CoRR abs/1505.01662 (2015) - [i20]Wenda Li, Grant Olney Passmore, Lawrence C. Paulson:
A Complete Decision Procedure for Univariate Polynomial Problems in Isabelle/HOL. CoRR abs/1506.08238 (2015) - 2014
- [j48]Lawrence C. Paulson:
Real-Valued Special Functions: Upper and Lower Bounds. Arch. Formal Proofs 2014 (2014) - [j47]Zongyan Huang, Matthew England, David J. Wilson, James H. Davenport, Lawrence C. Paulson:
A Comparison of Three Heuristics to Choose the Variable Ordering for Cylindrical Algebraic Decomposition. ACM Commun. Comput. Algebra 48(3/4): 121-123 (2014) - [j46]James P. Bridge, Sean B. Holden, Lawrence C. Paulson:
Machine Learning for First-Order Theorem Proving - Learning to Select a Good Heuristic. J. Autom. Reason. 53(2): 141-172 (2014) - [j45]Lawrence C. Paulson:
A Machine-Assisted Proof of Gödel's Incompleteness theorems for the Theory of Hereditarily Finite Sets. Rev. Symb. Log. 7(3): 484-498 (2014) - [c58]Zongyan Huang, Matthew England, David J. Wilson, James H. Davenport, Lawrence C. Paulson, James P. Bridge:
Applying Machine Learning to the Problem of Choosing a Heuristic to Select the Variable Ordering for Cylindrical Algebraic Decomposition. CICM 2014: 92-107 - [c57]Paul B. Jackson, Andrew Sogokon, James P. Bridge, Lawrence C. Paulson:
Verifying Hybrid Systems Involving Transcendental Functions. NASA Formal Methods 2014: 188-202 - [c56]Lawrence C. Paulson:
Automated theorem proving for special functions: the next phase. SNC 2014: 3-8 - [i19]Zongyan Huang, Matthew England, David J. Wilson, James H. Davenport, Lawrence C. Paulson, James P. Bridge:
Applying machine learning to the problem of choosing a heuristic to select the variable ordering for cylindrical algebraic decomposition. CoRR abs/1404.6369 (2014) - [i18]Zongyan Huang, Matthew England, David J. Wilson, James H. Davenport, Lawrence C. Paulson:
A comparison of three heuristics to choose the variable ordering for CAD. CoRR abs/1405.6082 (2014) - 2013
- [j44]Lawrence C. Paulson:
Gödel's Incompleteness Theorems. Arch. Formal Proofs 2013 (2013) - [j43]Lawrence C. Paulson:
The Hereditarily Finite Sets. Arch. Formal Proofs 2013 (2013) - [j42]Nik Sultana, Jasmin Christian Blanchette, Lawrence C. Paulson:
LEO-II and Satallax on the Sledgehammer test bench. J. Appl. Log. 11(1): 91-102 (2013) - [j41]James P. Bridge, Lawrence C. Paulson:
Case Splitting in an Automatic Theorem Prover for Real-Valued Special Functions. J. Autom. Reason. 50(1): 99-117 (2013) - [j40]Jasmin Christian Blanchette, Sascha Böhme, Lawrence C. Paulson:
Extending Sledgehammer with SMT Solvers. J. Autom. Reason. 51(1): 109-128 (2013) - [j39]Christoph Benzmüller, Lawrence C. Paulson:
Quantified Multimodal Logics in Simple Type Theory. Logica Universalis 7(1): 7-20 (2013) - [c55]Lawrence C. Paulson:
MetiTarski's Menagerie of Cooperating Systems. FroCos 2013: 1-6 - [c54]Jean Everson Martina, Lawrence C. Paulson:
Verifying multicast-based security protocols using the inductive method. SAC 2013: 1824-1829 - [d1]James P. Bridge, Sean B. Holden, Lawrence C. Paulson:
First-order theorem proving. UCI Machine Learning Repository, 2013
- 2012
- [j38]Ralph Romanos, Lawrence C. Paulson:
Proving the Impossibility of Trisecting an Angle and Doubling the Cube. Arch. Formal Proofs 2012 (2012) - [c53]Grant Olney Passmore, Lawrence C. Paulson, Leonardo Mendonça de Moura:
Real Algebraic Strategies for MetiTarski Proofs. AISC/MKM/Calculemus 2012: 358-370 - [c52]Lawrence C. Paulson:
MetiTarski: Past and Future. ITP 2012: 1-10 - 2011
- [c51]Jasmin Christian Blanchette, Sascha Böhme, Lawrence C. Paulson:
Extending Sledgehammer with SMT Solvers. CADE 2011: 116-130 - 2010
- [j37]Christoph Benzmüller, Lawrence C. Paulson:
Multimodal and intuitionistic logics in simple type theory. Log. J. IGPL 18(6): 881-892 (2010) - [j36]Behzad Akbarpour, Lawrence C. Paulson:
MetiTarski: An Automatic Theorem Prover for Real-Valued Special Functions. J. Autom. Reason. 44(3): 175-205 (2010) - [c50]Lawrence C. Paulson:
Three Years of Experience with Sledgehammer, a Practical Link between Automatic and Interactive Theorem Provers. PAAR@IJCAR 2010: 1-10 - [c49]Rajeev Narayanan, Behzad Akbarpour, Mohamed H. Zaki, Sofiène Tahar, Lawrence C. Paulson:
Formal verification of analog circuits in the presence of noise and process variation. DATE 2010: 1309-1312 - [c48]Lawrence C. Paulson, Jasmin Christian Blanchette:
Three years of experience with Sledgehammer, a Practical Link Between Automatic and Interactive Theorem Provers. IWIL@LPAR 2010: 1-11 - [e1]Matt Kaufmann, Lawrence C. Paulson:
Interactive Theorem Proving, First International Conference, ITP 2010, Edinburgh, UK, July 11-14, 2010. Proceedings. Lecture Notes in Computer Science 6172, Springer 2010, ISBN 978-3-642-14051-8 [contents] - [r1]Lawrence C. Paulson:
Functional Programming in ML. Encyclopedia of Software Engineering 2010: 333-346
2000 – 2009
- 2009
- [j35]Jia Meng, Lawrence C. Paulson:
Lightweight relevance filtering for machine-generated resolution problems. J. Appl. Log. 7(1): 41-57 (2009) - [c47]William Denman, Behzad Akbarpour, Sofiène Tahar, Mohamed H. Zaki, Lawrence C. Paulson:
Formal verification of analog designs using MetiTarski. FMCAD 2009: 93-100 - [c46]Behzad Akbarpour, Lawrence C. Paulson:
Applications of MetiTarski in the Verification of Control and Hybrid Systems. HSCC 2009: 1-15 - [i17]Christoph Benzmüller, Lawrence C. Paulson:
Quantified Multimodal Logics in Simple Type Theory. CoRR abs/0905.2435 (2009) - 2008
- [j34]Tobias Nipkow, Lawrence C. Paulson:
Fun With Tilings. Arch. Formal Proofs 2008 (2008) - [j33]Jia Meng, Lawrence C. Paulson:
Translating Higher-Order Clauses to First-Order Clauses. J. Autom. Reason. 40(1): 35-60 (2008) - [c45]Behzad Akbarpour, Lawrence C. Paulson:
MetiTarski: An Automatic Prover for the Elementary Functions. AISC/MKM/Calculemus 2008: 217-231 - [c44]Christoph Benzmüller, Lawrence C. Paulson, Frank Theiss, Arnaud Fietzke:
LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description). IJCAR 2008: 162-170 - [c43]Lawrence C. Paulson:
The Relative Consistency of the Axiom of Choice - Mechanized Using Isabelle/ZF. CiE 2008: 486-490 - [c42]Makarius Wenzel, Lawrence C. Paulson, Tobias Nipkow:
The Isabelle Framework. TPHOLs 2008: 33-38 - 2007
- [j32]Bernhard Beckert, Lawrence C. Paulson:
Preface. J. Autom. Reason. 38(1-3): 1-2 (2007) - [c41]Jia Meng, Lawrence C. Paulson, Gerwin Klein:
A Termination Checker for Isabelle Hoare Logic. VERIFY 2007 - [c40]Behzad Akbarpour, Lawrence C. Paulson:
Extending a Resolution Prover for Inequalities on Elementary Functions. LPAR 2007: 47-61 - [c39]Lawrence C. Paulson, Kong Woei Susanto:
Source-Level Proof Reconstruction for Interactive Theorem Proving. TPHOLs 2007: 232-245 - 2006
- [j31]