Google
Google Scholar
Semantic Scholar
MS Academic
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
- 2021
[i34]Angeliki Koutsoukou Argyraki, Wenda Li, Lawrence C. Paulson:
Irrationality and Transcendence Criteria for Infinite Series in Isabelle/HOL. CoRR abs/2101.05257 (2021)- 2020
- [d15]Lawrence C. Paulson:
The Nash-Williams Partition Theorem. Arch. Formal Proofs 2020 (2020) - [d14]Lawrence C. Paulson:
Ordinal Partitions. Arch. Formal Proofs 2020 (2020) - [j53]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) - [c68]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 - [c67]Paulo Emílio de Vilhena, Lawrence C. Paulson:
Algebraically Closed Fields in Isabelle/HOL. IJCAR (2) 2020: 204-220 - [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
- [d13]Lawrence C. Paulson:
Fourier Series. Arch. Formal Proofs 2019 (2019) - [d12]Lawrence C. Paulson:
Zermelo Fraenkel Set Theory in Higher-Order Logic. Arch. Formal Proofs 2019 (2019) - [j52]Lawrence C. Paulson, Tobias Nipkow, Makarius Wenzel:
From LCF to Isabelle/HOL. Formal Aspects Comput. 31(6): 675-698 (2019) - [j51]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) - [j50]Mohammad Abdulaziz, Lawrence C. Paulson:
An Isabelle/HOL Formalisation of Green's Theorem. J. Autom. Reason. 63(3): 763-786 (2019) - [j49]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) - [c66]Wenda Li, Lawrence C. Paulson:
Counting polynomial roots in isabelle/hol: a formal proof of the budan-fourier theorem. CPP 2019: 52-64 - [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
- [d11]Mohammad Abdulaziz, Lawrence C. Paulson:
An Isabelle/HOL formalisation of Green's Theorem. Arch. Formal Proofs 2018 (2018) - [d10]Manuel Eberl, Lawrence C. Paulson:
The Prime Number Theorem. Arch. Formal Proofs 2018 (2018) - [d9]Lawrence C. Paulson:
Quaternions. Arch. Formal Proofs 2018 (2018) - [j48]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
- [d8]Quentin Hibon, Lawrence C. Paulson:
Source Coding Theorem. Arch. Formal Proofs 2016 (2016) - [d7]Lawrence C. Paulson:
The Cartan Fixed Point Theorems. Arch. Formal Proofs 2016 (2016) - [j47]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
- [d6]Lawrence C. Paulson:
Finite Automata in Hereditarily Finite Set Theory. Arch. Formal Proofs 2015 (2015) - [j46]Jean Everson Martina, Lawrence C. Paulson:
Verifying multicast-based security protocols using the inductive method. Int. J. Inf. Sec. 14(2): 187-204 (2015) - [j45]Lawrence C. Paulson:
A Mechanised Proof of Gödel's Incompleteness Theorems Using Nominal Isabelle. J. Autom. Reason. 55(1): 1-37 (2015) - [j44]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
- [d5]Lawrence C. Paulson:
Real-Valued Special Functions: Upper and Lower Bounds. Arch. Formal Proofs 2014 (2014) - [j43]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) - [j42]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) - [j41]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
- [d4]Lawrence C. Paulson:
Gödel's Incompleteness Theorems. Arch. Formal Proofs 2013 (2013) - [d3]Lawrence C. Paulson:
The Hereditarily Finite Sets. Arch. Formal Proofs 2013 (2013) - [j40]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) - [j39]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) - [j38]Jasmin Christian Blanchette, Sascha Böhme, Lawrence C. Paulson:
Extending Sledgehammer with SMT Solvers. J. Autom. Reason. 51(1): 109-128 (2013) - [j37]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 - 2012
- [d2]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
- [j36]Christoph Benzmüller, Lawrence C. Paulson:
Multimodal and intuitionistic logics in simple type theory. Log. J. IGPL 18(6): 881-892 (2010) - [j35]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
- [j34]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
- [d1]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]Jia Meng, Claire Quigley, Lawrence C. Paulson:
Automation for interactive proof: First prototype. Inf. Comput. 204(10): 1575-1596 (2006) - [j30]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) - [j29]Giampaolo Bella, Fabio Massacci, Lawrence C. Paulson:
Verifying the SET Purchase Protocols. J. Autom. Reason. 36(1-2): 5-37 (2006) - [j28]Giampaolo Bella, Lawrence C. Paulson:
Accountability protocols: Formalized and verified. ACM Trans. Inf. Syst. Secur. 9(2): 138-161 (2006) - [j27]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
- [j26]Sidi O. Ehmety, Lawrence C. Paulson:
Mechanizing compositional reasoning for concurrent systems: some lessons. Formal Aspects Comput. 17(1): 58-68 (2005) - [j25]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
- [j24]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
- [j23]Giampaolo Bella, Fabio Massacci, Lawrence C. Paulson:
Verifying the SET registration protocols. IEEE J. Sel. Areas Commun. 21(1): 77-87 (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
- [b5]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
- [j22]Lawrence C. Paulson:
A Simple Formalization and Proof for the Mutilated Chess Board. Log. J. IGPL 9(3): 475-485 (2001) - [j21]Lawrence C. Paulson:
Relations Between Secrets: Two Formal Analyses of the Yahalom Protocol. J. Comput. Secur. 9(3): 197-216 (2001) - [j20]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
- [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]