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
- 2025
[j97]Angeliki Koutsoukou-Argyraki, Lawrence C. Paulson:
Transitive Union-Closed Families. Arch. Formal Proofs 2025 (2025)- [j96]Lawrence C. Paulson:
Farey Sequences and Ford Circles. Arch. Formal Proofs 2025 (2025) - [j95]Sophie Tourret, Lawrence C. Paulson:
Compactness Theorem for First-Order Logic. Arch. Formal Proofs 2025 (2025) - [i46]Lawrence C. Paulson:
Formalising New Mathematics in Isabelle: Diagonal Ramsey. CoRR abs/2501.10852 (2025) - 2024
- [j94]Lawrence C. Paulson:
Ramsey Number Bounds. Arch. Formal Proofs 2024 (2024) - [j93]Lawrence C. Paulson:
An Exponential Improvement for Diagonal Ramsey. Arch. Formal Proofs 2024 (2024) - [j92]Lawrence C. Paulson
:
A formalised theorem in the partition calculus. Ann. Pure Appl. Log. 175(Issue 1, Part B): 103246 (2024) - [c78]Chelsea Edmonds, Lawrence C. Paulson:
Formal Probabilistic Methods for Combinatorial Structures using the Lovász Local Lemma. CPP 2024: 132-146 - [c77]Manuel Eberl, Anthony Bordg, Lawrence C. Paulson, Wenda Li:
Formalising Half of a Graduate Textbook on Number Theory (Short Paper). ITP 2024: 40:1-40:7 - [d2]Manuel Eberl, Anthony Bordg, Lawrence C. Paulson, Wenda Li:
Formalising Half of a Graduate Textbook on Number Theory (Formal Proof Development). Zenodo, 2024
- 2023
- [j91]Chelsea Edmonds, Lawrence C. Paulson:
Hypergraph Colouring Bounds. Arch. Formal Proofs 2023 (2023) - [j90]Lawrence C. Paulson:
Euler's Polyhedron Formula. Arch. Formal Proofs 2023 (2023) - [j89]Lawrence C. Paulson:
Knuth-Morris-Pratt String Search. Arch. Formal Proofs 2023 (2023) - [j88]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 - [i45]Chelsea Edmonds, Lawrence C. Paulson:
Formal Probabilistic Methods for Combinatorial Structures in Isabelle/HOL. CoRR abs/2310.00513 (2023) - 2022
- [j87]Chelsea Edmonds, Lawrence C. Paulson:
Fisher's Inequality: Linear Algebraic Proof Techniques for Combinatorics. Arch. Formal Proofs 2022 (2022) - [j86]Jacques D. Fleuriot, Lawrence C. Paulson:
Constructing the Reals as Dedekind Cuts of Rationals. Arch. Formal Proofs 2022 (2022) - [j85]Angeliki Koutsoukou-Argyraki, Lawrence C. Paulson:
The Plünnecke-Ruzsa Inequality. Arch. Formal Proofs 2022 (2022) - [j84]Angeliki Koutsoukou-Argyraki, Lawrence C. Paulson:
Khovanskii's Theorem. Arch. Formal Proofs 2022 (2022) - [j83]Lawrence C. Paulson:
Irrational numbers from THE BOOK. Arch. Formal Proofs 2022 (2022) - [j82]Lawrence C. Paulson:
Young's Inequality for Increasing Functions. Arch. Formal Proofs 2022 (2022) - [j81]Lawrence C. Paulson:
Wetzel's Problem and the Continuum Hypothesis. Arch. Formal Proofs 2022 (2022) - [j80]Lawrence C. Paulson:
Ackermann's Function Is Not Primitive Recursive. Arch. Formal Proofs 2022 (2022) - [j79]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) - [j78]Mirna Dzamonja, Angeliki Koutsoukou-Argyraki, Lawrence C. Paulson:
Formalizing Ordinal Partition Relations Using Isabelle/HOL. Exp. Math. 31(2): 383-400 (2022) - [j77]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) - [j76]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
- [j75]Anthony Bordg, Lawrence C. Paulson, Wenda Li:
Grothendieck's Schemes in Algebraic Geometry. Arch. Formal Proofs 2021 (2021) - [j74]Chelsea Edmonds, Angeliki Koutsoukou-Argyraki, Lawrence C. Paulson:
Szemerédi's Regularity Lemma. Arch. Formal Proofs 2021 (2021) - [j73]Chelsea Edmonds, Angeliki Koutsoukou-Argyraki, Lawrence C. Paulson:
Roth's Theorem on Arithmetic Progressions. Arch. Formal Proofs 2021 (2021) - [j72]Chelsea Edmonds, Lawrence C. Paulson:
Combinatorial Design Theory. Arch. Formal Proofs 2021 (2021) - [j71]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
- [j70]Lawrence C. Paulson:
The Nash-Williams Partition Theorem. Arch. Formal Proofs 2020 (2020) - [j69]Lawrence C. Paulson:
Ordinal Partitions. Arch. Formal Proofs 2020 (2020) - [j68]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
- [j67]Lawrence C. Paulson:
Fourier Series. Arch. Formal Proofs 2019 (2019) - [j66]Lawrence C. Paulson:
Zermelo Fraenkel Set Theory in Higher-Order Logic. Arch. Formal Proofs 2019 (2019) - [j65]Lawrence C. Paulson, Tobias Nipkow, Makarius Wenzel:
From LCF to Isabelle/HOL. Formal Aspects Comput. 31(6): 675-698 (2019) - [j64]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) - [j63]Mohammad Abdulaziz, Lawrence C. Paulson:
An Isabelle/HOL Formalisation of Green's Theorem. J. Autom. Reason. 63(3): 763-786 (2019) - [j62]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
- [j61]Mohammad Abdulaziz, Lawrence C. Paulson:
An Isabelle/HOL formalisation of Green's Theorem. Arch. Formal Proofs 2018 (2018) - [j60]Manuel Eberl, Lawrence C. Paulson:
The Prime Number Theorem. Arch. Formal Proofs 2018 (2018) - [j59]Lawrence C. Paulson:
Quaternions. Arch. Formal Proofs 2018 (2018) - [j58]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
- [j57]Quentin Hibon, Lawrence C. Paulson:
Source Coding Theorem. Arch. Formal Proofs 2016 (2016) - [j56]Lawrence C. Paulson:
The Cartan Fixed Point Theorems. Arch. Formal Proofs 2016 (2016) - [j55]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
- [j54]Lawrence C. Paulson:
Finite Automata in Hereditarily Finite Set Theory. Arch. Formal Proofs 2015 (2015) - [j53]Jean Everson Martina, Lawrence C. Paulson:
Verifying multicast-based security protocols using the inductive method. Int. J. Inf. Sec. 14(2): 187-204 (2015) - [j52]Lawrence C. Paulson:
A Mechanised Proof of Gödel's Incompleteness Theorems Using Nominal Isabelle. J. Autom. Reason. 55(1): 1-37 (2015) - [j51]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
- [j50]Lawrence C. Paulson:
Real-Valued Special Functions: Upper and Lower Bounds. Arch. Formal Proofs 2014 (2014) - [j49]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) - [j48]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) - [j47]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
- [j46]Lawrence C. Paulson:
Gödel's Incompleteness Theorems. Arch. Formal Proofs 2013 (2013) - [j45]Lawrence C. Paulson:
The Hereditarily Finite Sets. Arch. Formal Proofs 2013 (2013) - [j44]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) - [j43]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) - [j42]Jasmin Christian Blanchette, Sascha Böhme, Lawrence C. Paulson:
Extending Sledgehammer with SMT Solvers. J. Autom. Reason. 51(1): 109-128 (2013) - [j41]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
- [j40]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
- [j39]Christoph Benzmüller, Lawrence C. Paulson:
Multimodal and intuitionistic logics in simple type theory. Log. J. IGPL 18(6): 881-892 (2010) - [j38]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
- [j37]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
- [j36]Tobias Nipkow, Lawrence C. Paulson:
Fun With Tilings. Arch. Formal Proofs 2008 (2008) - [j35]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
- [j34]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
- [j33]Jia Meng, Claire Quigley, Lawrence C. Paulson:
Automation for interactive proof: First prototype. Inf. Comput. 204(10): 1575-1596 (2006) - [j32]Jia Meng, Claire Quigley, Lawrence C. Paulson:
Erratum to "Automation for interactive proof: First prototype" [Inform. and Comput. 204(2006) 1575-1596]. Inf. Comput. 204(12): 1852 (2006) - [j31]Giampaolo Bella, Fabio Massacci, Lawrence C. Paulson:
Verifying the SET Purchase Protocols. J. Autom. Reason. 36(1-2): 5-37 (2006) - [j30]Giampaolo Bella, Lawrence C. Paulson:
Accountability protocols: Formalized and verified. ACM Trans. Inf. Syst. Secur. 9(2): 138-161 (2006) - [j29]Lawrence C. Paulson:
Defining functions on equivalence classes. ACM Trans. Comput. Log. 7(4): 658-675 (2006) - [p1]Markus Wenzel, Lawrence C. Paulson:
Isabelle/Isar. The Seventeen Provers of the World 2006: 41-49 - 2005
- [j28]Sidi O. Ehmety, Lawrence C. Paulson:
Mechanizing compositional reasoning for concurrent systems: some lessons. Formal Aspects Comput. 17(1): 58-68 (2005) - [j27]Giampaolo Bella, Fabio Massacci, Lawrence C. Paulson:
An overview of the verification of SET. Int. J. Inf. Sec. 4(1-2): 17-28 (2005) - [c38]Tobias Nipkow, Lawrence C. Paulson:
Proof Pearl: Defining Functions over Finite Sets. TPHOLs 2005: 385-396 - 2004
- [j26]Lawrence C. Paulson:
Organizing Numerical Theories Using Axiomatic Type Classes. J. Autom. Reason. 33(1): 29-49 (2004) - [c37]Jia Meng, Lawrence C. Paulson:
Experiments on Supporting Interactive Proof Using Resolution. IJCAR 2004: 372-384 - 2003
- [j25]Giampaolo Bella, Fabio Massacci, Lawrence C. Paulson:
Verifying the SET registration protocols. IEEE J. Sel. Areas Commun. 21(1): 77-87 (2003) - [j24]Lawrence C. Paulson:
The Relative Consistency of the Axiom of Choice Mechanized Using Isabelle⁄zf. LMS J. Comput. Math. 6: 198-248 (2003) - [c36]Giampaolo Bella, Cristiano Longo, Lawrence C. Paulson:
Is the Verification Problem for Cryptographic Protocols Solved?. Security Protocols Workshop 2003: 183-189 - [c35]Giampaolo Bella, Cristiano Longo, Lawrence C. Paulson:
Verifying Second-Level Security Protocols. TPHOLs 2003: 352-366 - 2002
- [b6]Tobias Nipkow, Lawrence C. Paulson, Markus Wenzel:
Isabelle/HOL - A Proof Assistant for Higher-Order Logic. Lecture Notes in Computer Science 2283, Springer 2002, ISBN 3-540-43376-7 - [c34]Lawrence C. Paulson:
The Reflection Theorem: A Study in Meta-theoretic Reasoning. CADE 2002: 377-391 - [c33]Giampaolo Bella, Lawrence C. Paulson, Fabio Massacci:
The verification of an industrial payment protocol: the SET purchase phase. CCS 2002: 12-20 - [c32]Lawrence C. Paulson:
Verifying the SET Protocol: Overview. FASec 2002: 4-14 - [c31]Sidi O. Ehmety, Lawrence C. Paulson:
Program Composition in Isabelle/UNITY. IPDPS 2002 - [c30]Giampaolo Bella, Lawrence C. Paulson:
Analyzing Delegation Properties. Security Protocols Workshop 2002: 120-127 - 2001
- [j23]Lawrence C. Paulson:
A Simple Formalization and Proof for the Mutilated Chess Board. Log. J. IGPL 9(3): 475-485 (2001) - [j22]Lawrence C. Paulson:
Relations Between Secrets: Two Formal Analyses of the Yahalom Protocol. J. Comput. Secur. 9(3): 197-216 (2001) - [j21]Lawrence C. Paulson:
Mechanizing a theory of program composition for UNITY. ACM Trans. Program. Lang. Syst. 23(5): 626-656 (2001) - [c29]Lawrence C. Paulson:
SET Cardholder Registration: The Secrecy Proofs. IJCAR 2001: 5-12 - [c28]Giampaolo Bella, Lawrence C. Paulson:
A Proof of Non-repudiation. Security Protocols Workshop 2001: 119-125 - [c27]Lawrence C. Paulson:
A Proof of Non-repudiation (Transcript of Discussion). Security Protocols Workshop 2001: 126-133 - [c26]Giampaolo Bella, Lawrence C. Paulson:
Mechanical Proofs about a Non-repudiation Protocol. TPHOLs 2001: 91-104 - 2000
- [j20]Jacques D. Fleuriot, Lawrence C. Paulson:
Mechanizing Nonstandard Real Analysis. LMS J. Comput. Math. 3: 140-190 (2000) - [j19]Lawrence C. Paulson:
Mechanizing UNITY in Isabelle. ACM Trans. Comput. Log. 1(1): 3-32 (2000) - [c25]Lawrence C. Paulson:
A fixedpoint approach to (co)inductive and (co)datatype definitions. Proof, Language, and Interaction 2000: 187-212 - [c24]Giampaolo Bella, Fabio Massacci, Lawrence C. Paulson, Piero Tramontano:
Formal Verification of Cardholder Registration in SET. ESORICS 2000: 159-174 - [c23]Giampaolo Bella, Fabio Massacci, Lawrence C. Paulson, Piero Tramontano:
Making Sense of Specifications: The Formalization of SET. Security Protocols Workshop 2000: 74-81 - [c22]Lawrence C. Paulson:
Making Sense of Specifications: The Formalization of SET (Transcript of Discussion). Security Protocols Workshop 2000: 82-86
1990 – 1999
- 1999
- [j18]Clemens Ballarin, Lawrence C. Paulson:
A Pragmatic Approach to Extending Provers by Computer Algebra - with Applications to Coding Theory. Fundam. Informaticae 39(1-2): 1-20 (1999) - [j17]Florian Kammüller, Lawrence C. Paulson:
A Formal Proof of Sylow's Theorem. J. Autom. Reason. 23(3-4): 235-264 (1999) - [j16]Lawrence C. Paulson:
A Generic Tableau Prover and its Integration with Isabelle. J. Univers. Comput. Sci. 5(3): 73-87 (1999) - [j15]Lawrence C. Paulson:
Final coalgebras as greatest fixed points in ZF set theory. Math. Struct. Comput. Sci. 9(5): 545-567 (1999) - [j14]Lawrence C. Paulson:
Inductive Analysis of the Internet Protocol TLS. ACM Trans. Inf. Syst. Secur. 2(3): 332-351 (1999) - [j13]Leslie Lamport, Lawrence C. Paulson:
Should your specification language be typed. ACM Trans. Program. Lang. Syst. 21(3): 502-526 (1999) - [c21]Lawrence C. Paulson:
Proving Security Protocols Correct. LICS 1999: 370-381 - [c20]Lawrence C. Paulson:
Relatios Between Secrets: The Yahalom Protocol. Security Protocols Workshop 1999: 73-84 - [c19]Florian Kammüller, Markus Wenzel, Lawrence C. Paulson:
Locales - A Sectioning Concept for Isabelle. TPHOLs 1999: 149-166 - 1998
- [j12]Lawrence C. Paulson:
The Inductive Approach to Verifying Cryptographic Protocols. J. Comput. Secur. 6(1-2): 85-128 (1998) - [c18]Jacques D. Fleuriot, Lawrence C. Paulson:
Proving Newton's Propositio Kepleriana Using Geometry and Nonstandard Analysis in Isabelle. Automated Deduction in Geometry 1998: 47-66 - [c17]Clemens Ballarin, Lawrence C. Paulson:
Reasoning About Coding Theory: The Benefits We Get from Computer Algebra. AISC 1998: 55-66 - [c16]Jacques D. Fleuriot, Lawrence C. Paulson:
A Combination of Nonstandard Analysis and Geometry Theorem Proving, with Application to Newton's Principia. CADE 1998: 3-16 - [c15]Giampaolo Bella, Lawrence C. Paulson:
Mechanising BAN Kerberos by the Inductive Method. CAV 1998: 416-427 - [c14]Giampaolo Bella, Lawrence C. Paulson:
Kerberos Version 4: Inductive Analysis of the Secrecy Goals. ESORICS 1998: 361-375 - [c13]Lawrence C. Paulson:
Inductive Analysis of the Internet Protocol TLS (Position Paper). Security Protocols Workshop 1998: 1-12 - [c12]Lawrence C. Paulson:
Inductive Analysis of the Internet Protocol TLS (Transcript of Discussion). Security Protocols Workshop 1998: 13-23 - 1997
- [j11]Lawrence C. Paulson:
Mechanizing Coinduction and Corecursion in Higher-Order Logic. J. Log. Comput. 7(2): 175-204 (1997) - [c11]Lawrence C. Paulson:
Proving Properties of Security Protocols by Induction. CSFW 1997: 70-83 - [c10]Lawrence C. Paulson:
Mechanized proofs for a recursive authentication protocol. CSFW 1997: 84-95 - [i16]Lawrence C. Paulson:
Mechanizing Coinduction and Corecursion in Higher-order Logic. CoRR cs.LO/9711105 (1997) - [i15]Lawrence C. Paulson:
Generic Automatic Proof Tools. CoRR cs.LO/9711106 (1997) - 1996
- [b5]Lawrence C. Paulson:
ML for the working programmer (2. ed.). Cambridge University Press 1996, ISBN 978-0-521-57050-3, pp. I-XVIII, 1-476 - [j10]Lawrence C. Paulson, Krzysztof Grabczewski:
Mechanizing Set Theory. J. Autom. Reason. 17(3): 291-323 (1996) - [i14]Lawrence C. Paulson, Krzysztof Grabczewski:
Mechanizing Set Theory: Cardinal Arithmetic and the Axiom of Choice. CoRR cs.LO/9612104 (1996) - 1995
- [j9]Lawrence C. Paulson:
Set Theory for Verification. II: Induction and Recursion. J. Autom. Reason. 15(2): 167-215 (1995) - [i13]Lawrence C. Paulson:
Set Theory for Verification: II. Induction and Recursion. CoRR abs/cs/9511102 (1995) - [i12]Lawrence C. Paulson:
A Concrete Final Coalgebra Theorem for ZF Set Theory. CoRR abs/cs/9511103 (1995) - 1994
- [b4]Lawrence C. Paulson:
Isabelle - A Generic Theorem Prover (with a contribution by T. Nipkow). Lecture Notes in Computer Science 828, Springer 1994, ISBN 3-540-58244-4 - [c9]Lawrence C. Paulson:
A Fixedpoint Approach to Implementing (Co)Inductive Definitions. CADE 1994: 148-161 - [c8]Lawrence C. Paulson:
A Concrete Final Coalgebra Theorem for ZF Set Theory. TYPES 1994: 120-139 - 1993
- [j8]Lawrence C. Paulson:
Set Theory for Verification: I. From Foundations to Functions. J. Autom. Reason. 11(3): 353-389 (1993) - [i11]Lawrence C. Paulson:
Verifying the Unification Algorithm in LCF. CoRR cs.LO/9301101 (1993) - [i10]Lawrence C. Paulson:
Constructing Recursion Operators in Intuitionistic Type Theory. CoRR cs.LO/9301102 (1993) - [i9]Lawrence C. Paulson:
Proving Termination of Normalization Functions for Conditional Expressions. CoRR cs.LO/9301103 (1993) - [i8]Lawrence C. Paulson:
Natural Deduction as Higher-Order Resolution. CoRR cs.LO/9301104 (1993) - [i7]Lawrence C. Paulson:
The Foundation of a Generic Theorem Prover. CoRR cs.LO/9301105 (1993) - [i6]Lawrence C. Paulson:
Isabelle: The Next 700 Theorem Provers. CoRR cs.LO/9301106 (1993) - [i5]Lawrence C. Paulson:
A Formulation of the Simple Theory of Types (for Isabelle). CoRR cs.LO/9301107 (1993) - [i4]Lawrence C. Paulson:
A Higher-Order Implementation of Rewriting. CoRR cs.LO/9301108 (1993) - [i3]Lawrence C. Paulson, Andrew W. Smith:
Logic Programming, Functional Programming, and Inductive Definitions. CoRR cs.LO/9301109 (1993) - [i2]Lawrence C. Paulson:
Designing a Theorem Prover. CoRR cs.LO/9301110 (1993) - [i1]Lawrence C. Paulson:
Set Theory for Verification: I. From Foundations to Functions. CoRR cs.LO/9311103 (1993) - 1992
- [c7]Tobias Nipkow, Lawrence C. Paulson:
Isabelle-91. CADE 1992: 673-676 - 1991
- [b3]Lawrence C. Paulson:
ML for the working programmer. Cambridge University Press 1991, ISBN 978-0-521-39022-4, pp. I-X, 1-429
1980 – 1989
- 1989
- [j7]Lawrence C. Paulson:
The Foundation of a Generic Theorem Prover. J. Autom. Reason. 5(3): 363-397 (1989) - [c6]Lawrence C. Paulson, Andrew W. Smith:
Logic Programming, Functional Programming, and Inductive Definitions. ELP 1989: 283-309 - 1988
- [c5]Lawrence C. Paulson:
Isabelle: The Next Seven Hundred Theorem Provers. CADE 1988: 772-773 - [c4]Lawrence C. Paulson:
A formulation of the simple theory of types (for Isabelle). Conference on Computer Logic 1988: 246-274 - 1987
- [b2]Lawrence C. Paulson:
Logic and computation - interactive proof with Cambridge LCF. Cambridge tracts in theoretical computer science 2, Cambridge University Press 1987, ISBN 978-0-521-34632-0, pp. 1-302 - 1986
- [j6]Lawrence C. Paulson:
Proving Termination of Normalization Functions for Conditional Experessions. J. Autom. Reason. 2(1): 63-74 (1986) - [j5]Lawrence C. Paulson:
Natural Deduction as Higher-Order Resolution. J. Log. Program. 3(3): 237-258 (1986) - [j4]Lawrence C. Paulson:
Constructing Recursion Operators in Intuitionistic Type Theory. J. Symb. Comput. 2(4): 325-355 (1986) - 1985
- [j3]Lawrence C. Paulson:
Lessons Learned from LCF: A Survey of Natural Deduction Proofs. Comput. J. 28(5): 474-479 (1985) - [j2]Lawrence C. Paulson:
Verifying the Unification Algorithm in LCF. Sci. Comput. Program. 5(2): 143-169 (1985) - 1984
- [c3]Lawrence C. Paulson:
Deriving Structural Induction in LCF. Semantics of Data Types 1984: 197-214 - 1983
- [j1]Lawrence C. Paulson:
A Higher-Order Implementation of Rewriting. Sci. Comput. Program. 3(2): 119-149 (1983) - [c2]Lawrence C. Paulson:
Compiler Generation from Denotational Semantics. Method and tools for compiler construction 1983: 219-252 - 1982
- [c1]Lawrence C. Paulson:
A Semantics-Directed Compiler Generator. POPL 1982: 224-233 - 1981
- [b1]Lawrence C. Paulson:
A compiler generator for semantic grammars. Stanford University, USA, 1981
Coauthor Index
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from 
to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the 
of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from 
, 
, and 
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from 
.
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2025-07-02 19:02 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
