All Stories

  1. Formal Verification of Transcendental Fixed- and Floating-point Algorithms using an Automatic Theorem Prover

    Article • Formal Aspects of Computing, June 2022, ACM (Association for Computing Machinery)

    Professor Lawrence Charles Paulson

  2. Porting the HOL light analysis library: some lessons (invited talk)

    Article • January 2017, ACM (Association for Computing Machinery)

    Professor Lawrence Charles Paulson

  3. Verifying multicast-based security protocols using the inductive method

    Article • International Journal of Information Security, August 2014, Springer Science + Business Media

    Professor Lawrence Charles Paulson

  4. Automated theorem proving for special functions

    Article • July 2014, ACM (Association for Computing Machinery)

    Professor Lawrence Charles Paulson

  5. A MACHINE-ASSISTED PROOF OF GÖDEL’S INCOMPLETENESS THEOREMS FOR THE THEORY OF HEREDITARILY FINITE SETS

    Article • The Review of Symbolic Logic, April 2014, Cambridge University Press

    Professor Lawrence Charles Paulson

  6. Verifying Hybrid Systems Involving Transcendental Functions

    Article • January 2014, Springer Science + Business Media

    Professor Lawrence Charles Paulson

  7. Verifying multicast-based security protocols using the inductive method

    Article • March 2013, ACM (Association for Computing Machinery)

    Professor Lawrence Charles Paulson

  8. Extending Sledgehammer with SMT Solvers

    Article • Journal of Automated Reasoning, March 2013, Springer Science + Business Media

    Professor Lawrence Charles Paulson

  9. MetiTarski’s Menagerie of Cooperating Systems

    Article • January 2013, Springer Science + Business Media

    Professor Lawrence Charles Paulson

  10. Quantified Multimodal Logics in Simple Type Theory

    Article • Logica Universalis, May 2012, Springer Science + Business Media

    Professor Lawrence Charles Paulson

  11. Case Splitting in an Automatic Theorem Prover for Real-Valued Special Functions

    Article • Journal of Automated Reasoning, March 2012, Springer Science + Business Media

    Professor Lawrence Charles Paulson

  12. MetiTarski: Past and Future

    Article • January 2012, Springer Science + Business Media

    Professor Lawrence Charles Paulson

  13. Real Algebraic Strategies for MetiTarski Proofs

    Article • January 2012, Springer Science + Business Media

    Professor Lawrence Charles Paulson

  14. Extending Sledgehammer with SMT Solvers

    Article • January 2011, Springer Science + Business Media

    Professor Lawrence Charles Paulson

  15. Interactive Theorem Proving

    Article • January 2010

    Professor Lawrence Charles Paulson

  16. Formal verification of analog designs using MetiTarski

    Article • November 2009, Institute of Electrical & Electronics Engineers (IEEE)

    Professor Lawrence Charles Paulson

  17. MetiTarski: An Automatic Theorem Prover for Real-Valued Special Functions

    Article • Journal of Automated Reasoning, August 2009, Springer Science + Business Media

    Professor Lawrence Charles Paulson

  18. Lightweight relevance filtering for machine-generated resolution problems

    Article • Journal of Applied Logic, March 2009, Elsevier

    Professor Lawrence Charles Paulson

  19. The Isabelle Framework

    Article • January 2008, Springer Science + Business Media

    Professor Lawrence Charles Paulson

  20. Translating Higher-Order Clauses to First-Order Clauses

    Article • Journal of Automated Reasoning, September 2007, Springer Science + Business Media

    Professor Lawrence Charles Paulson

  21. Preface

    Article • Journal of Automated Reasoning, February 2007, Springer Science + Business Media

    Professor Lawrence Charles Paulson

  22. Defining functions on equivalence classes

    Article • ACM Transactions on Computational Logic, October 2006, ACM (Association for Computing Machinery)

    Professor Lawrence Charles Paulson

  23. Automation for interactive proof: First prototype

    Article • Information and Computation, October 2006, Elsevier

    Professor Lawrence Charles Paulson

  24. Accountability protocols

    Article • ACM Transactions on Information and System Security, May 2006, ACM (Association for Computing Machinery)

    Professor Lawrence Charles Paulson

  25. Verifying the SET Purchase Protocols

    Article • Journal of Automated Reasoning, February 2006, Springer Science + Business Media

    Professor Lawrence Charles Paulson

  26. Mechanizing compositional reasoning for concurrent systems: some lessons

    Article • Formal Aspects of Computing, May 2005, ACM (Association for Computing Machinery)

    Professor Lawrence Charles Paulson

  27. An overview of the verification of SET

    Article • International Journal of Information Security, February 2005, Springer Science + Business Media

    Professor Lawrence Charles Paulson

  28. Is the Verification Problem for Cryptographic Protocols Solved?

    Article • January 2005, Springer Science + Business Media

    Professor Lawrence Charles Paulson

  29. Proof Pearl: Defining Functions over Finite Sets

    Article • January 2005, Springer Science + Business Media

    Professor Lawrence Charles Paulson

  30. Organizing Numerical Theories Using Axiomatic Type Classes

    Article • Journal of Automated Reasoning, July 2004, Springer Science + Business Media

    Professor Lawrence Charles Paulson

  31. Analyzing Delegation Properties

    Article • January 2004, Springer Science + Business Media

    Professor Lawrence Charles Paulson

  32. Experiments on Supporting Interactive Proof Using Resolution

    Article • January 2004, Springer Science + Business Media

    Professor Lawrence Charles Paulson

  33. Verifying the SET Protocol: Overview

    Article • January 2003, Springer Science + Business Media

    Professor Lawrence Charles Paulson

  34. Verifying Second-Level Security Protocols

    Article • January 2003, Springer Science + Business Media

    Professor Lawrence Charles Paulson

  35. Isabelle/HOL

    Article • January 2002

    Professor Lawrence Charles Paulson

  36. A Proof of Non-repudiation

    Article • January 2002, Springer Science + Business Media

    Professor Lawrence Charles Paulson

  37. The Reflection Theorem: A Study in Meta-theoretic Reasoning

    Article • January 2002, Springer Science + Business Media

    Professor Lawrence Charles Paulson

  38. SET Cardholder Registration: The Secrecy Proofs

    Article • January 2001, Springer Science + Business Media

    Professor Lawrence Charles Paulson

  39. Mechanical Proofs about a Non-repudiation Protocol

    Article • January 2001, Springer Science + Business Media

    Professor Lawrence Charles Paulson

  40. Making Sense of Specifications: The Formalization of SET

    Article • January 2001, Springer Science + Business Media

    Professor Lawrence Charles Paulson

  41. Making Sense of Specifications: The Formalization of SET

    Article • January 2001, Springer Science + Business Media

    Professor Lawrence Charles Paulson

  42. Mechanizing UNITY in Isabelle

    Article • ACM Transactions on Computational Logic, July 2000, ACM (Association for Computing Machinery)

    Professor Lawrence Charles Paulson

  43. The Yahalom Protocol

    Article • January 2000, Springer Science + Business Media

    Professor Lawrence Charles Paulson

  44. Relations Between Secrets: The Yahalom Protocol

    Article • January 2000, Springer Science + Business Media

    Professor Lawrence Charles Paulson

  45. Mechanizing Nonstandard Real Analysis

    Article • LMS Journal of Computation and Mathematics, January 2000, Oxford University Press (OUP)

    Professor Lawrence Charles Paulson

  46. Formal Verification of Cardholder Registration in SET

    Article • January 2000, Springer Science + Business Media

    Professor Lawrence Charles Paulson

  47. Inductive analysis of the Internet protocol TLS

    Article • ACM Transactions on Information and System Security, August 1999, ACM (Association for Computing Machinery)

    Professor Lawrence Charles Paulson

  48. Locales A Sectioning Concept for Isabelle

    Article • January 1999, Springer Science + Business Media

    Professor Lawrence Charles Paulson

  49. Inductive Analysis of the Internet Protocol TLS

    Article • January 1998, Springer Science + Business Media

    Professor Lawrence Charles Paulson

  50. Kerberos Version IV: Inductive analysis of the secrecy goals

    Article • January 1998, Springer Science + Business Media

    Professor Lawrence Charles Paulson

  51. Mechanising BAN Kerberos by the inductive method

    Article • January 1998, Springer Science + Business Media

    Professor Lawrence Charles Paulson

  52. Tool Support for Logics of Programs

    Article • January 1997, Springer Science + Business Media

    Professor Lawrence Charles Paulson

  53. Set theory for verification. II: Induction and recursion

    Article • Journal of Automated Reasoning, January 1995, Springer Science + Business Media

    Professor Lawrence Charles Paulson

  54. A concrete final coalgebra theorem for ZF set theory

    Article • January 1995, Springer Science + Business Media

    Professor Lawrence Charles Paulson

  55. Isabelle

    Article • January 1994

    Professor Lawrence Charles Paulson

  56. A fixedpoint approach to implementing (Co)inductive definitions

    Article • January 1994, Springer Science + Business Media

    Professor Lawrence Charles Paulson

  57. Set theory for verification: I. From foundations to functions

    Article • Journal of Automated Reasoning, January 1993, Springer Science + Business Media

    Professor Lawrence Charles Paulson

  58. Book reviews

    Article • Formal Aspects of Computing, September 1992, ACM (Association for Computing Machinery)

    Professor Lawrence Charles Paulson

  59. Isabelle-91

    Article • January 1992, Springer Science + Business Media

    Professor Lawrence Charles Paulson

  60. A formulation of the simple theory of types (for Isabelle)

    Article • January 1990, Springer Science + Business Media

    Professor Lawrence Charles Paulson

  61. The foundation of a generic theorem prover

    Article • Journal of Automated Reasoning, September 1989, Springer Science + Business Media

    Professor Lawrence Charles Paulson

  62. Logic and Computation

    Article • October 1987, Cambridge University Press

    Professor Lawrence Charles Paulson

  63. Survey and History of LCF

    Article • October 1987, Cambridge University Press

    Professor Lawrence Charles Paulson

  64. Formal Proof in First Order Logic

    Article • October 1987, Cambridge University Press

    Professor Lawrence Charles Paulson

  65. A Logic of Computable Functions

    Article • October 1987, Cambridge University Press

    Professor Lawrence Charles Paulson

  66. Syntactic Operations for PPλ

    Article • October 1987, Cambridge University Press

    Professor Lawrence Charles Paulson

  67. Constructing recursion operators in intuitionistic type theory

    Article • Journal of Symbolic Computation, December 1986, Elsevier

    Professor Lawrence Charles Paulson

  68. Natural deduction as higher-order resolution

    Article • The Journal of Logic Programming, October 1986, Elsevier

    Professor Lawrence Charles Paulson

  69. Verifying the unification algorithm in LCF

    Article • Science of Computer Programming, January 1985, Elsevier

    Professor Lawrence Charles Paulson

  70. Deriving structural induction in LCF

    Article • January 1984, Springer Science + Business Media

    Professor Lawrence Charles Paulson

  71. A higher-order implementation of rewriting

    Article • Science of Computer Programming, August 1983, Elsevier

    Professor Lawrence Charles Paulson

  72. A semantics-directed compiler generator

    Article • January 1982, ACM (Association for Computing Machinery)

    Professor Lawrence Charles Paulson

  73. The Descent of BAN

    Article • Springer Science + Business Media

    Professor Lawrence Charles Paulson

  74. Isabelle: The next seven hundred theorem provers

    Article • Springer Science + Business Media

    Professor Lawrence Charles Paulson

  75. Logic programming, functional programming, and inductive definitions

    Article • Springer Science + Business Media

    Professor Lawrence Charles Paulson

  76. Source-Level Proof Reconstruction for Interactive Theorem Proving

    Article • Springer Science + Business Media

    Professor Lawrence Charles Paulson

  77. MetiTarski: An Automatic Prover for the Elementary Functions

    Article • Springer Science + Business Media

    Professor Lawrence Charles Paulson

  78. The Relative Consistency of the Axiom of Choice — Mechanized Using Isabelle/ZF

    Article • Springer Science + Business Media

    Professor Lawrence Charles Paulson