Lawrence Paulson
#9,644
Most Influential Person Now
American computer scientist
Lawrence Paulson's AcademicInfluence.com Rankings
Lawrence Paulsoncomputer-science Degrees
Computer Science
#734
World Rank
#756
Historical Rank
#395
USA Rank
Automated Reasoning
#7
World Rank
#7
Historical Rank
#3
USA Rank
Database
#832
World Rank
#873
Historical Rank
#258
USA Rank
Download Badge
Computer Science
Why Is Lawrence Paulson Influential?
(Suggest an Edit or Addition)According to Wikipedia, Lawrence Charles Paulson is an American computer scientist. He is a Professor of Computational Logic at the University of Cambridge Computer Laboratory and a Fellow of Clare College, Cambridge. Education Paulson graduated from the California Institute of Technology in 1977, and obtained his PhD in Computer Science from Stanford University in 1981 for research on programming languages and compiler-compilers supervised by John L. Hennessy.
Lawrence Paulson's Published Works
Number of citations in a given year to any of this author's works
Total number of citations to an author for the works they published in a given year. This highlights publication of the most important work(s) by the author
Published Works
- Isabelle/HOL: A Proof Assistant for Higher-Order Logic (2002) (2644)
- Isabelle: A Generic Theorem Prover (1994) (1360)
- The Inductive Approach to Verifying Cryptographic Protocols (2021) (1026)
- A Proof Assistant for Higher-Order Logic (2002) (932)
- ML for the working programmer (1991) (684)
- Isabelle/HOL (2002) (477)
- Isabelle: The Next 700 Theorem Provers (2000) (407)
- Logic and computation - interactive proof with Cambridge LCF (1987) (310)
- Proving properties of security protocols by induction (1997) (309)
- Inductive analysis of the Internet protocol TLS (1999) (304)
- The foundation of a generic theorem prover (1989) (271)
- Extending Sledgehammer with SMT Solvers (2011) (251)
- Three years of experience with Sledgehammer, a Practical Link Between Automatic and Interactive Theorem Provers (2012) (212)
- Natural Deduction as Higher-Order Resolution (1986) (173)
- Quaternions (170)
- The Isabelle Framework (2008) (164)
- Hammering towards QED (2016) (147)
- Kerberos Version 4: Inductive Analysis of the Secrecy Goals (1998) (147)
- ML for the working programmer (2. ed.) (1996) (145)
- Mechanized proofs for a recursive authentication protocol (1997) (136)
- Should your specification language be typed (1999) (126)
- Lightweight relevance filtering for machine-generated resolution problems (2009) (126)
- Locales - A Sectioning Concept for Isabelle (1999) (125)
- MetiTarski: An Automatic Theorem Prover for Real-Valued Special Functions (2010) (124)
- Translating Higher-Order Clauses to First-Order Clauses (2007) (123)
- A Higher-Order Implementation of Rewriting (1983) (118)
- A Generic Tableau Prover and its Integration with Isabelle (1999) (113)
- Quantified Multimodal Logics in Simple Type Theory (2009) (113)
- Logic And Computation (1987) (102)
- A semantics-directed compiler generator (1982) (92)
- Isabelle - A Generic Theorem Prover (with a contribution by T. Nipkow) (1994) (92)
- Relations Between Secrets: Two Formal Analyses of the Yahalom Protocol (2001) (90)
- LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description) (2008) (86)
- Verifying the Unification Algorithm in LCF (1985) (83)
- Source-Level Proof Reconstruction for Interactive Theorem Proving (2007) (82)
- Machine Learning for First-Order Theorem Proving (2014) (77)
- Verifying the SET registration protocols (2003) (77)
- Isabelle tutorial and user’s manual (1990) (74)
- A Fixedpoint Approach to Implementing (Co)Inductive Definitions (1994) (74)
- The Higher-Order Prover Leo-II (2015) (73)
- Automation for interactive proof: First prototype (2006) (71)
- The Isabelle Reference Manual (2007) (69)
- Set theory for verification: I. From foundations to functions (1993) (68)
- Mechanizing Coinduction and Corecursion in Higher-Order Logic (1997) (67)
- The verification of an industrial payment protocol: the SET purchase phase (2002) (65)
- Constructing Recursion Operators in Intuitionistic Type Theory (1986) (64)
- Introduction to Isabelle (1999) (62)
- Formal Verification of Cardholder Registration in SET (2000) (61)
- Verifying the SET Purchase Protocols (2005) (56)
- Multimodal and intuitionistic logics in simple type theory (2010) (55)
- Mechanical Proofs about a Non-repudiation Protocol (2001) (54)
- Applying machine learning to the problem of choosing a heuristic to select the variable ordering for cylindrical algebraic decomposition (2014) (53)
- Set theory for verification. II: Induction and recursion (1995) (52)
- Proving security protocols correct (1999) (50)
- Generic Automatic Proof Tools (1997) (48)
- Mechanizing UNITY in Isabelle (2000) (47)
- Accountability protocols: Formalized and verified (2006) (46)
- Experiments on Supporting Interactive Proof Using Resolution (2004) (43)
- Isabelle: The Next Seven Hundred Theorem Provers (1988) (43)
- Mechanized Proofs of Security Protocols: Needham-Schroeder with Public Keys (1997) (43)
- A fixedpoint approach to (co)inductive and (co)datatype definitions (2000) (39)
- MetiTarski: Past and Future (2012) (39)
- Formal verification of analog designs using MetiTarski (2009) (37)
- A Mechanised Proof of Gödel’s Incompleteness Theorems Using Nominal Isabelle (2015) (37)
- Mechanizing set theory (1996) (36)
- Exploring Properties of Normal Multimodal Logics in Simple Type Theory with LEO-II (2008) (36)
- Mechanizing Set Theory: Cardinal Arithmetic and the Axiom of Choice (2001) (35)
- An overview of the verification of SET (2005) (35)
- A compiler generator for semantic grammars (1981) (34)
- Isabelle-91 (1992) (34)
- Translating higher-order problems to first-order clauses (2006) (33)
- The Relative Consistency of the Axiom of Choice - Mechanized Using Isabelle/ZF (2008) (33)
- Designing a Theorem Prover (1993) (31)
- Mechanising BAN Kerberos by the Inductive Method (1998) (31)
- Natural deduction proof as higher-order resolution (1985) (30)
- Tactics and tacticals in Cambridge LCF (1983) (30)
- IsarStep: a Benchmark for High-level Mathematical Reasoning (2021) (30)
- Defining functions on equivalence classes (2006) (29)
- MetiTarski: An Automatic Prover for the Elementary Functions (2008) (29)
- Isabelle/Isar (2006) (29)
- Applications of MetiTarski in the Verification of Control and Hybrid Systems (2009) (28)
- Co-induction and co-recursion in higher-order logic (1993) (27)
- LEO-II and Satallax on the Sledgehammer test bench (2013) (27)
- A MACHINE-ASSISTED PROOF OF GÖDEL’S INCOMPLETENESS THEOREMS FOR THE THEORY OF HEREDITARILY FINITE SETS (2014) (27)
- Logic Programming, Functional Programming, and Inductive Definitions (1991) (26)
- A Pragmatic Approach to Extending Provers by Computer Algebra - with Applications to Coding Theory (1999) (25)
- Organizing Numerical Theories Using Axiomatic Type Classes (2004) (25)
- Verifying Second-Level Security Protocols (2003) (24)
- A Simple Formalization and Proof for the Mutilated Chess Board (2001) (22)
- A formulation of the simple theory of types (for Isabelle) (1990) (22)
- Using Machine Learning to Decide When to Precondition Cylindrical Algebraic Decomposition with Groebner Bases (2016) (22)
- From LCF to Isabelle/HOL (2019) (22)
- Using Machine Learning to Improve Cylindrical Algebraic Decomposition (2018) (21)
- Mechanizing Nonstandard Real Analysis (2000) (21)
- A Concrete Final Coalgebra Theorem for ZF Set Theory (1994) (21)
- A comparison of the mathematical proof languages Mizar and Isar (2002) (21)
- Computational logic: its origins and applications (2017) (21)
- A Combination of Nonstandard Analysis and Geometry Theorem Proving, with Application to Newton's Principia (1998) (20)
- The Relative Consistency of the Axiom of Choice Mechanized Using Isabelle⁄zf (2021) (20)
- Proof Pearl: Defining Functions over Finite Sets (2005) (20)
- A Formal Proof of Sylow's Theorem An Experiment in Abstract Algebra with Isabelle HOL (1998) (19)
- Real Algebraic Strategies for MetiTarski Proofs (2012) (19)
- The representation of logics in higher-order logic (1987) (19)
- Mechanizing a theory of program composition for UNITY (2001) (19)
- Extending a Resolution Prover for Inequalities on Elementary Functions (2007) (18)
- Verifying the SET Protocol: Overview (2002) (16)
- Deriving Structural Induction in LCF (1984) (16)
- Formal verification of analog circuits in the presence of noise and process variation (2010) (16)
- Lessons Learned from LCF: A Survey of Natural Deduction Proofs (1985) (16)
- Compiler Generation from Denotational Semantics (1984) (16)
- A preliminary users manual for Isabelle (1988) (15)
- Machine Learning for First-Order Theorem Proving - Learning to Select a Good Heuristic (2014) (15)
- Deciding Univariate Polynomial Problems Using Untrusted Certificates in Isabelle/HOL (2015) (15)
- The Isabelle/Isar Implementation (2016) (14)
- A Formal Proof of Sylow's Theorem (1999) (14)
- Progress Report on LEO-II -- An Automatic Theorem Prover for Higher-Order Logic (2007) (14)
- Proving termination of normalization functions for conditional expressions (2000) (14)
- JACQUES HERBRAND : LIFE , LOGIC , AND AUTOMATED DEDUCTION (2007) (13)
- Automation for Interactive Proof (2003) (13)
- A Formal Proof of Cauchy's Residue Theorem (2016) (13)
- Tool support for logics of programs (1997) (12)
- On two formal analyses of the Yahalom protocol (1997) (12)
- A Formalisation of Finite Automata Using Hereditarily Finite Sets (2015) (11)
- A modular, efficient formalisation of real algebraic numbers (2016) (11)
- Interactive Theorem Proving, First International Conference, ITP 2010, Edinburgh, UK, July 11-14, 2010. Proceedings (2010) (11)
- The LEO-II Project (2007) (10)
- An Isabelle/HOL Formalisation of Green’s Theorem (2016) (10)
- Verifying multicast-based security protocols using the inductive method (2013) (10)
- Zermelo Fraenkel Set Theory in Higher-Order Logic (2019) (9)
- Proving Newton's Propositio Kepleriana Using Geometry and Nonstandard Analysis in Isabelle (1998) (9)
- The Reflection Theorem: A Study in Meta-theoretic Reasoning (2002) (9)
- Modelling High-Level Mathematical Reasoning in Mechanised Declarative Proofs (2020) (8)
- The revised logic PPLAMBDA : A reference manual (1983) (8)
- Constructive Type Theory (1994) (8)
- Strategic Principles in the Design of Isabelle (2003) (8)
- Program composition in Isabelle/UNITY (2002) (8)
- Formalizing Ordinal Partition Relations Using Isabelle/HOL (2020) (7)
- Mechanizing compositional reasoning for concurrent systems: some lessons (2005) (7)
- Isabelle's Logics: HOL1 (2000) (7)
- A Termination Checker for Isabelle Hoare Logic (2007) (7)
- Relatios Between Secrets: The Yahalom Protocol (1999) (6)
- The supplemental Isabelle/HOL library (2002) (6)
- Formal verification of card-holder registration in SET (2000) (6)
- 1. The Basics (2002) (6)
- Experience with Isabelle : A generic theorem prover (1988) (6)
- Simple Type Theory is not too Simple: Grothendieck’s Schemes Without Dependent Types (2021) (6)
- Case Splitting in an Automatic Theorem Prover for Real-Valued Special Functions (2012) (6)
- SET Cardholder Registration: The Secrecy Proofs (2001) (5)
- A Modular First Formalisation of Combinatorial Design Theory (2021) (5)
- SErAPIS : A Concept-Oriented Search Engine for the Isabelle Libraries Based on Natural Language (2020) (5)
- The Verification of an Industrial Payment Protocol (2002) (5)
- Zermelo-Fraenkel set theory (1994) (5)
- Evaluating Winding Numbers and Counting Complex Roots Through Cauchy Indices in Isabelle/HOL (2018) (5)
- Final coalgebras as greatest fixed points in ZF set theory (1999) (5)
- Recent developments in LCF: examples of structural induction (1983) (5)
- Mechanized Proofs for a Recursive Authentication Protocol 1 (1997) (4)
- Lightweight relevance filtering for machine-generated resolution (2006) (4)
- Formalising Mathematics In Simple Type Theory (2018) (4)
- A Proof of Non-repudiation (2001) (4)
- ML for the Working Programmer: Reasoning About Functional Programs (1996) (4)
- An Isabelle/HOL Formalisation of Green’s Theorem (2018) (4)
- Issues in modelling the SET protocol (2002) (4)
- Inductive Analysis of the Internet Protocol TLS (Transcript of Discussion) (1998) (4)
- Introduction to Milestones in Interactive Theorem Proving (2018) (4)
- A Comparison of Three Heuristics to Choose the Variable Ordering for Cylindrical Algebraic Decomposition (2015) (4)
- Making Sense of Specifications: The Formalization of SET (2000) (4)
- Foundations of Functional Programming (2000) (3)
- Verifying Hybrid Systems Involving Transcendental Functions (2014) (3)
- Isabelle’s Object-Logics (2011) (3)
- Logic and Computation: Cambridge LCF (1987) (3)
- Grothendieck's Schemes in Algebraic Geometry (2021) (3)
- What we can learn from API security: (Transcript of discussion) (2005) (3)
- Algebraically Closed Fields in Isabelle/HOL (2020) (3)
- Representing Component States in Higher-Order Logic (2002) (3)
- Inductive Analysis of the Internet Protocol TLS (Position Paper) (1998) (3)
- Inductive analysis of the internet protocol TLS. Discussion. Authors' reply (1999) (3)
- A Complete Decision Procedure for Univariate Polynomial Problems in Isabelle/HOL (2015) (3)
- Representing Component States in Higher-Order Logic (2002) (3)
- Are timestamps worth the effort? A formal treatment (1998) (3)
- Gödel's Incompleteness Theorems (2013) (3)
- ML for the Working Programmer: Preface (1996) (3)
- Wetzel: Formalisation of an Undecidable Problem Linked to the Continuum Hypothesis (2022) (2)
- Welcome Defects as a Sign of Innovation (2005) (2)
- Making Sense of Specifications: The Formalization of SET (Transcript of Discussion) (2000) (2)
- 6. Sets, Functions, and Relations (2002) (2)
- Using Machine Learning to Decide When to Precondition Cylindrical Algebraic Decomposition with Groebner Bases (2016) (2)
- Tactics and Tacticals (1987) (2)
- Real-Valued Special Functions: Upper and Lower Bounds (2014) (2)
- Lessons learned from LCF (1984) (2)
- Is the Verification Problem for Cryptographic Protocols Solved? (2003) (2)
- Cardinal Arithmetic and the Axiom of Choice (2000) (2)
- Ordinal Partitions (2020) (2)
- Proving Properties of Security Protocols by In (1997) (2)
- Old Introduction to Isabelle (2009) (2)
- Reasoning About Coding Theory: The Benefits We Get from Computer Algebra (1998) (2)
- Foundations of Computer Science (1999) (2)
- Counting polynomial roots in Isabelle/HOL: a formal proof of the Budan-Fourier theorem (2018) (1)
- 7. Inductively Defined Sets (2002) (1)
- SET Cardholder Registration: the Secrecy Proofs (Extended Abstract) (2001) (1)
- Functional Programming in ML (2010) (1)
- The Prime Number Theorem (2018) (1)
- Higher-order logic (1994) (1)
- Proofs and Reconstructions (2015) (1)
- Old Isabelle Reference Manual (2009) (1)
- Finite Automata in Hereditarily Finite Set Theory (2015) (1)
- ML for the Working Programmer: PREDECLARED IDENTIFIERS (1996) (1)
- Set Theory as a Computational Logic: I. From Foundations to Functions ⁄ (1992) (1)
- Automated theorem proving for special functions: the next phase (2014) (1)
- Beyond Linear Arithmetic : Automatic Proof Procedures for the Reals (2004) (1)
- 147 Should Your Specification Language Be Typed ? (1997) (1)
- Extending Sledgehammer with SMT Solvers (2013) (1)
- Formalising Szemerédi’s Regularity Lemma and Roth’s Theorem on Arithmetic Progressions in Isabelle/HOL (2022) (1)
- Michael John Caldwell Gordon (FRS 1994), 28 February 1948 -- 22 August 2017 (2018) (1)
- A comparison of three heuristics to choose the variable ordering for CAD (2014) (1)
- Bayesian Optimisation for Heuristic Configuration in Automated Theorem Proving (2020) (1)
- Fisher's Inequality: Linear Algebraic Proof Techniques for Combinatorics (2022) (1)
- Automatic Proof Procedures for Polynomials and Special Functions (2010) (1)
- Formal Verification of Transcendental Fixed- and Floating-point Algorithms using an Automatic Theorem Prover (2022) (1)
- Irrationality and Transcendence Criteria for Infinite Series in Isabelle/HOL (2021) (1)
- Logic and Computation by Lawrence C. Paulson (1987) (1)
- Wetzel's Problem and the Continuum Hypothesis (2022) (1)
- Bayesian Optimisation with Gaussian Processes for Premise Selection (2019) (1)
- Proving Properties of Security Protocols by Induction 1 (1997) (1)
- 5. The Rules of the Game (2002) (1)
- Quantified Multimodal Logics in Simple Type Theory (2012) (1)
- Mathematical Proof Between Generations (2022) (1)
- Imperative Programming in ML (1996) (1)
- Bayesian Optimisation for Premise Selection in Automated Theorem Proving (Student Abstract) (2020) (0)
- Isabelle-89 - source code from the interactive theorem prover Isabelle upon its release in 1989 (2016) (0)
- Sutcliffe 7 . 1 CVC 4 0 . 0 (2012) (0)
- A Proof of Non-repudiation (Transcript of Discussion) (2001) (0)
- Combinatorial Design Theory (2021) (0)
- Fourier Series (2019) (0)
- Szemerédi's Regularity Lemma (2021) (0)
- Logic and Computation: Formal Proof in First Order Logic (1987) (0)
- Lent Term, 1997 (2000) (0)
- Using Machine Learning to Improve Cylindrical Algebraic Decomposition (2019) (0)
- The Yahalom Protocol (1999) (0)
- Lent Term, 1997 (2000) (0)
- Syntax of Isabelle Theories (1994) (0)
- Automation for Interactive Proof Prof (2003) (0)
- Proving the Impossibility of Trisecting an Angle and Doubling the Cube (2012) (0)
- Axioms and Inference Rules (1987) (0)
- Evaluating Winding Numbers through Cauchy Indices in Isabelle/HOL (2018) (0)
- Analyzing Delegation Properties (2002) (0)
- Foundations of Functional Programming Computer Science Tripos Part IB Easter Term (2000) (0)
- Abstract Types and Functors (1996) (0)
- Applications of Proof Theory to Isabelle (1996) (0)
- First-order sequent calculus (1994) (0)
- A Tactical Theorem Prover (1996) (0)
- Erratum to "Automation for interactive proof: First prototype" [Inform. and Comput. 204(2006) 1575-1596] (2006) (0)
- Case Splitting in an Automatic Theorem Prover for Real-Valued Special Functions (2012) (0)
- Perspective Computational logic: its origins and applications (2018) (0)
- 9. Advanced Simplification, Recursion, and Induction (2002) (0)
- Research data supporting "A semantics-directed compiler generator" (2016) (0)
- 4. Presenting Theories (2002) (0)
- Proceedings of the First international conference on Interactive Theorem Proving (2010) (0)
- Letters (2004) (0)
- Delegation of responsibilities. Discussion. Authors' reply (1999) (0)
- Theorems and forward proof (1994) (0)
- The Plünnecke-Ruzsa Inequality (2022) (0)
- The Nash-Williams Partition Theorem (2020) (0)
- Bayesian Optimisation of Solver Parameters in CBMC (2020) (0)
- 3. More Functional Programming (2002) (0)
- DoD Value Engineering Conference Report. Value Engineering (VE) - A Tool that Benefits Line Management Held at Leesburg, Virginia on 1-2 November 1984. Part 5. Workshop C: VEP/VECP Administration, Negotiation, and Implementation, (1985) (0)
- Mechanising Temporal Reasoning : Summary (2003) (0)
- Michael John Caldwell Gordon. 28 February 1948—22 August 2017 (2018) (0)
- Logic and Computation: Logic and Computation (1987) (0)
- Security Protocols (1997) (0)
- Large-Scale Formal Proof for the Working Mathematician ALEXANDRIA Section a : State-ofthe-art and objectives The Crisis in Modern Mathematics (2016) (0)
- Computer Science Tripos Part IB Michaelmas Term (1999) (0)
- Towards flexible credential negotiation protocols. Commentary. Authors' reply (2005) (0)
- Tool Support for Logics of Programs International Summer School Marktoberdorf Mathematical Methods in Program Development 2002 (2002) (0)
- ML for the Working Programmer: Functions and Infinite Data (1996) (0)
- Roth's Theorem on Arithmetic Progressions (2021) (0)
- ML for the Working Programmer: Names, Functions and Types (1996) (0)
- Induction and Recursion (2000) (0)
- Syntactic Operations for PPλ (1987) (0)
- The Cartan Fixed Point Theorems (2016) (0)
- Panel session: Is protocol modelling finished? (transcript of discussion). Discussion (2005) (0)
- Is entity authentication necessary? Discussion (2003) (0)
- Writing Interpreters for the λ-Calculus (1996) (0)
- The Protocol and Lowe ’ s Attack 1 3 Modelling the Protocol 2 4 Proving Guarantees for A 3 5 Proving Guarantees for B 5 6 A Glimpse (1998) (0)
- I Tool Support for Logics of Programs 1 Slide 101 What Should Proof Tools Give Us ? (2002) (0)
- Constructing the Reals as Dedekind Cuts of Rationals (2022) (0)
- Logic and Proof Computer Science Tripos Part IB (1999) (0)
- Verifying multicast-based security protocols using the inductive method (2014) (0)
- 1 INTRODUCTION AND LEARNING GUIDE 1 1 Introduction and Learning Guide (2018) (0)
- Functional Programming with Hope (1992) (0)
- DoD Value Engineering Conference Report. Value Engineering (VE) - A Tool that Benefits Line Management Held at Leesburg, Virginia on 1-2 November 1984. Part 6. Workshop D: VE Training/Orientation, (1985) (0)
- Evaluating Winding Numbers and Counting Complex Roots Through Cauchy Indices in Isabelle/HOL (2019) (0)
- Authentication Logics : New Theory and Implementations (2002) (0)
- Analyzing delegation properties. Discussion (2003) (0)
- Trees and Concrete Data (1996) (0)
- Automated Formal Verification of Analog / RF Circuits in the Presence of Noise (2009) (0)
- Khovanskii's Theorem (2022) (0)
- The Descent of BAN (2004) (0)
- Isabelle in The Early Days : A Logical Framework (2019) (0)
- 8. More about Types (2002) (0)
- DoD Value Engineering Conference Report. Value Engineering (VE) - A Tool that Benefits Line Management Held at Leesburg, Virginia on 1-2 November 1984. Part 7. Workshop E: VE in Construction and Architect Engineer Contracts, (1985) (0)
- Computer Science Tripos Part IA, Part II (General) and Diploma Lent Term, 1997 (1997) (0)
- Fun With Tilings (2008) (0)
- MetiTarski's Menagerie of Cooperating Systems (2013) (0)
- Deciding Univariate Polynomial Problems Using Untrusted Certificates in Isabelle/HOL (2017) (0)
- Proceedings of the Automated Reasoning Workshop 2008 (2008) (0)
- Theorem Proving and the Real Numbers : Overview and Challenges (2014) (0)
- Porting the HOL light analysis library: some lessons (invited talk) (2017) (0)
- Computability and Complexity in Analysis – CCA 2012 (2012) (0)
- ACKERMANN’S FUNCTION IN ITERATIVE FORM: A PROOF ASSISTANT EXPERIMENT (2021) (0)
- Insider fraud. Discussion. Authors' reply (1999) (0)
- Compositional Proofs of Concurrent Programs (1999) (0)
- Rewriting and Simplification (1987) (0)
- Automation for Interactive Proof Final Report (2007) (0)
- Source Coding Theorem (2016) (0)
- The Future of Formalised Mathematics (2016) (0)
- Logic and Computation: Bibliography (1987) (0)
- Formal Veri ation ofCardholder Registration in (2000) (0)
- What Should Proof Tools Do For Us ? (1996) (0)
- Getting started with Isabelle (1994) (0)
- A Mechanised Proof of Gödel’s Incompleteness Theorems Using Nominal Isabelle (2015) (0)
- Using Machine Learning to Decide When to Precondition Cylindrical Algebraic Decomposition With Groebner (2016) (0)
- Mobile IPv6 security. Discussion (2003) (0)
- LEO II : An Effective Higher-Order Theorem Prover (2005) (0)
- Verifying Electronic Commerce Protocols (2000) (0)
- A Formalised Theorem in the Partition Calculus (2021) (0)
- Grant Agreement ( Description of the Action ) Part B Proposal Acronym : ALEXANDRIA Proposal number : GA 742178 Proposal Title : Large-Scale Formal Proof for the Working (2017) (0)
- Theories, terms and types (1994) (0)
- 10. Case Study: Verifying a Security Protocol (2002) (0)
- Grant Agreement ( Description of the Action ) Part B Proposal Acronym : ALEXANDRIA Proposal number : GA 742178 Proposal Title : Large-Scale Formal Proof for the Working (2017) (0)
- Irrational numbers from THE BOOK (2022) (0)
- The Higher-Order Prover Leo-II (2015) (0)
- First-order logic (1994) (0)
- Logic and Computation: A Logic of Computable Functions (1987) (0)
- Introduction to Milestones in Interactive Theorem Proving (2018) (0)
- Isabelle-86 - source code from the interactive theorem prover Isabelle upon its original release in 1986 (2016) (0)
- The classical reasoner (1994) (0)
- Formalising Fisher's Inequality: Formal Linear Algebraic Proof Techniques in Combinatorics (2022) (0)
- Machine Learning for First-Order Theorem Proving (2014) (0)
- Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics): Preface (2010) (0)
- Ackermann's Function Is Not Primitive Recursive (2022) (0)
- Proof management: The subgoal module (1994) (0)
- The Hereditarily Finite Sets (2013) (0)
- 2. Functional Programming in HOL (2002) (0)
- Young's Inequality for Increasing Functions (2022) (0)
- How to write research papers, or don't make your readers scream! (2018) (0)
- Natural deduction theorem proving via higher-order resolution (1985) (0)
- Gordon, Michael John Caldwell (1948–2017), computer scientist (2021) (0)
- Basic use of Isabelle (1994) (0)
- Survey and History of LCF (1987) (0)
- Delegating trust. Discussion. Authors' reply (1999) (0)
- The Topology of Lazy Lists (2013) (0)
- Logic and Computation: Theory Structure (1987) (0)
- Bayesian Ranking for Strategy Scheduling in Automated Theorem Provers (2022) (0)
- Logic and Computation: Contents (1987) (0)
- A proof of non-repudiation. Discussion (2002) (0)
- Refocus Fragmented CS Conference Culture. Authors' reply (2009) (0)
- Milieu : Verification and Semantics (2018) (0)
This paper list is powered by the following services:
Other Resources About Lawrence Paulson
What Schools Are Affiliated With Lawrence Paulson?
Lawrence Paulson is affiliated with the following schools:
