Lawrence C. Paulson

According to our database1, Lawrence C. Paulson authored at least 128 papers between 1982 and 2019.

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

Awards

ACM Fellow

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

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Other 

Links

Homepages:

On csauthors.net:

Bibliography

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

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

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

Quaternions.
Archive of Formal Proofs, 2018

The Prime Number Theorem.
Archive of Formal Proofs, 2018

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

2016
Hammering towards QED.
J. Formalized Reasoning, 2016

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

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

An Isabelle/HOL Formalisation of Green's Theorem.
Proceedings of the Interactive Theorem Proving - 7th International Conference, 2016

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

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

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

Finite Automata in Hereditarily Finite Set Theory.
Archive of Formal Proofs, 2015

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

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

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

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

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

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

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

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

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

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

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

LEO-II and Satallax on the Sledgehammer test bench.
J. Applied Logic, 2013

The Hereditarily Finite Sets.
Archive of Formal Proofs, 2013

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

Verifying multicast-based security protocols using the inductive method.
Proceedings of the 28th Annual ACM Symposium on Applied Computing, 2013

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

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

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

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

2011
Extending Sledgehammer with SMT Solvers.
Proceedings of the Automated Deduction - CADE-23 - 23rd International Conference on Automated Deduction, Wroclaw, Poland, July 31, 2011

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

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

Multimodal and intuitionistic logics in simple type theory.
Logic Journal of the IGPL, 2010

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

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

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

2009
Lightweight relevance filtering for machine-generated resolution problems.
J. Applied Logic, 2009

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

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

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

Fun With Tilings.
Archive of Formal Proofs, 2008

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

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

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

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

2007
Preface.
J. Autom. Reasoning, 2007

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

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

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

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

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

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

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

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

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

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

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

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

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

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

2003
Verifying the SET registration protocols.
IEEE Journal on Selected Areas in Communications, 2003

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

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

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

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

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

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

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

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

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

Relations Between Secrets: Two Formal Analyses of the Yahalom Protocol.
Journal of Computer Security, 2001

A Simple Formalization and Proof for the Mutilated Chess Board.
Logic Journal of the IGPL, 2001

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

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

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

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

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

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

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

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

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

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

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

Final coalgebras as greatest fixed points in ZF set theory.
Mathematical Structures in Computer Science, 1999

A Generic Tableau Prover and its Integration with Isabelle.
J. UCS, 1999

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

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

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

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

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

1998
The Inductive Approach to Verifying Cryptographic Protocols.
Journal of Computer Security, 1998

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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


  Loading...