Refereed Articles

A BibTeX file of these articles is available.

  1. L. C. Paulson.
    Principles of Programming Languages (1982), 224–233.
  2. L. C. Paulson.
    A higher-order implementation of rewriting. Science of Computer Programming 3 (1983), 119–149. Publisher's version
  3. L. C. Paulson.
    Deriving structural induction in LCF. In: G. Kahn, D. B. MacQueen, G. Plotkin, editors, Semantics of Data Types (Springer, 1984), 197–214.
  4. L. C. Paulson.
    Verifying the unification algorithm in LCF. Science of Computer Programming 5 (1985), 143–170.
  5. L. C. Paulson.
    Lessons learned from LCF: a survey of natural deduction proofs. Computer J. 28 (1985), 474–479.
  6. L. C. Paulson.
    Proving termination of normalization functions for conditional expressions. J. Automated Reasoning 2 (1986), 63–74. Publisher's version
  7. L. C. Paulson.
    Constructing recursion operators in Intuitionistic Type Theory. J. Symbolic Computation 2 (1986), 325–355. Publisher's version
  8. L. C. Paulson.
    Natural deduction as higher-order resolution. J. Logic Programming 3 (1986), 237–258. Publisher's version
  9. L. C. Paulson.
    Isabelle: the next seven hundred theorem provers (system abstract). In: E. Lusk and R. Overbeek (editors), 9th International Conf. on Automated Deduction (Springer LNCS 310, 1988), 772–773.
  10. L. C. Paulson.
    The foundation of a generic theorem prover. J. Automated Reasoning 5 (1989), 363–397. Publisher's version
  11. L. C. Paulson.
    A formulation of the simple theory of types (for Isabelle). In: P. Martin-Löf and G. Mints (editors), COLOG-88: International Conf. in Computer Logic.Tallinn, Estonia (1988). Published as Springer LNCS 417, 1990), 246–274.
  12. L. C. Paulson.
    Isabelle: the next 700 theorem provers. In: P. Odifreddi (editor), Logic and Computer Science (Academic Press, 1990), 361–386.
  13. L. C. Paulson and A. W. Smith.
    Logic programming, functional programming, and inductive definitions. In: P. Schroeder-Heister (editor), Extensions of Logic Programming (Springer, 1991), 283–310.
  14. L. C. Paulson.
    Designing a theorem prover. In: S. Abramsky, D. M. Gabbay and T. S. E. Maibaum (editors), Handbook of Logic in Computer Science, Vol II (Oxford, 1992), 415–475.
  15. Tobias Nipkow and L. C. Paulson.
    Isabelle-91 (system abstract). In: D. Kapur (editor), 11th International Conf. on Automated Deduction (Springer LNAI 607, 1992), 673–676.
  16. L. C. Paulson.
    Set theory for verification: I. From foundations to functions. J. Automated Reasoning 11 (1993), 353–389.
  17. L. C. Paulson.
    A fixedpoint approach to implementing (co)inductive definitions. In: A. Bundy (editor), 12th International Conf. on Automated Deduction (Springer LNAI 814, 1994), 148–161.
    Slides available
  18. L. C. Paulson.
    Set theory for verification: II. Induction and recursion. J. Automated Reasoning 15 (1995), 167–215.
  19. L. C. Paulson.
    A concrete final coalgebra theorem for ZF set theory. In: P. Dybjer, B. Nordstrm and J. Smith (editors), Types for Proofs and Programs '94 (Springer LNCS 996, published 1995), 120–139.
  20. L. C. Paulson and Krzysztof Grąbczewski.
    Mechanizing set theory: cardinal arithmetic and the axiom of choice. J. Automated Reasoning 17 (1996), 291–323. Slides availablePublisher's version at www.springerlink.com
  21. L. C. Paulson.
    Mechanizing coinduction and corecursion in higher-order logic. J. Logic and Computation 7 (March 1997), 175–204. Publisher's version
  22. L. C. Paulson.
    Generic automatic proof tools. In: Robert Veroff (editor), Automated Reasoning and its Applications: Essays in Honor of Larry Wos (MIT Press, 1997), 23–47.
  23. L. C. Paulson.
    Proving properties of security protocols by induction. 10th Computer Security Foundations Workshop (June 1997), 70–83. Slides available
  24. L. C. Paulson.
    Mechanized proofs for a recursive authentication protocol. 10th Computer Security Foundations Workshop (June 1997), 84–95. Slides:available
  25. Giampaolo Bella and L. C. Paulson.
    Using Isabelle to prove properties of the Kerberos authentication system. DIMACS Workshop on Design and Formal Verification of Security Protocols, 1997.
  26. L. C. Paulson.
    The inductive approach to verifying cryptographic protocols. J. Computer Security 6 (1998), 85–128. Publisher's version
  27. Giampaolo Bella and L. C. Paulson.
    Mechanising BAN Kerberos by the inductive method. In: Alan J. Hu and Moshe Y. Vardi (editors), Computer-Aided Verification: CAV '98 (Springer LNCS 1427, 1998), 416–427.
  28. J. Fleuriot and L. C. Paulson.
    A combination of nonstandard analysis and geometry theorem proving, with application to Newton's Principia (revised version). In: C. Kirchner and H. Kirchner (editors), 15th International Conf. on Automated Deduction: CADE-15 (Springer LNAI 1421, 1998), 3–16. Publisher's version
  29. L. C. Paulson.
    A generic tableau prover and its integration with Isabelle (preliminary version). CADE-15 Workshop on Integration of Deductive Systems (1998), 51–60. Also Report 441, Computer Lab (1998). Slides available
  30. C. Ballarin and L. C. Paulson.
    Reasoning about coding theory: the benefits we get from computer algebra. In: Jacques Calmet and Jan Plaza (editors), Artificial Intelligence and Symbolic Computation: AISC '98 (Springer LNAI 1476, 1998), 55–66.
  31. Giampaolo Bella and L. C. Paulson.
    Kerberos version IV: inductive analysis of the secrecy goals. In: Jean-Jacques Quisquater et al. (editors), Computer Security — ESORICS (Springer LNCS 1485, 1998), 361–375.
  32. J. Fleuriot and L. C. Paulson.
    Proving Newton's Propositio Kepleriana Using geometry and nonstandard analysis in Isabelle In: Xiao-Shan Gao, Dongming Wang and Lu Yang (editors), Automated Deduction in Geometry, Second International Workshop, ADG '98 (Springer LNCS 1669, published 1999), 47–66. Publisher's version
  33. F. Kammüller and L. C. Paulson.
    A formal proof of Sylow's theorem: An experiment in abstract algebra with Isabelle HOL. J. Automated Reasoning 23 (1999), 235–264. Publisher's version
  34. L. C. Paulson.
    ACM Trans. on Information and System Security 2 3 (1999), 332–351. Slides available
  35. L. C. Paulson.
    Final coalgebras as greatest fixed points in ZF set theory. Mathematical Structures in Computer Science 9 (1999), 545–567. Publisher's version
  36. C. Ballarin and L. C. Paulson.
    A pragmatic approach to extending provers by computer algebra - with applications to coding theory. Fundamenta Informaticae 39 (1999), 1–20.
  37. L. Lamport and L. C. Paulson.
    ACM Trans. on Programming Languages and Systems 21 3 (1999), 502–526.
  38. F. Kammüller, M. Wenzel and L. C. Paulson.
    Locales: A sectioning concept for Isabelle. In: Y. Bertot, G. Dowek, A. Hirshchowitz, Ch. Paulin, L. Théry (editors), Theorem Proving in Higher Order Logics (Springer LNCS 1690, 1999), 149-166.
  39. L. C. Paulson.
    A generic tableau prover and its integration with Isabelle.
    J. Universal Computer Science 5 3 (1999), 73–87.
  40. L. C. Paulson.
    ACM Trans. on Computational Logic 1 1 (2000), 3–32.
  41. L. C. Paulson.
    A fixedpoint approach to (co)inductive and (co)datatype definitions In: G. Plotkin, C. Stirling, and M. Tofte (editors), Proof, Language, and Interaction: Essays in Honour of Robin Milner (MIT Press, 2000), 187–211.
  42. Giampaolo Bella, Fabio Massacci, L. C. Paulson and Piero Tramontano.
    Formal verification of Cardholder Registration in SET. In: F. Cuppens et al. (editors), Computer Security — ESORICS (Springer LNCS 1895, 2000), 159–174.
  43. Jacques Fleuriot and L. C. Paulson.
    Mechanising nonstandard real analysis.
    LMS J. Computation and Mathematics 3 (2000), 140–190.
  44. L. C. Paulson.
    Relations between secrets: two formal analyses of the Yahalom protocol. J. Computer Security 9 3 (2001), 197–216. Publisher's version
  45. L. C. Paulson.
    A simple formalization and proof for the mutilated chess board.
    Logic J. of the IGPL 9 3 (2001), 499–509.
  46. Giampaolo Bella and L. C. Paulson.
    Mechanical proofs about a non-repudiation protocol. In: Richard J. Boulton and Paul B. Jackson (editors),Theorem Proving in Higher Order Logics (Springer LNCS 2152, 2001), 91-104.
  47. L. C. Paulson.
    ACM Trans. on Programming Languages and Systems 25 5 (2001), 626–656.
  48. Sidi O. Ehmety and L. C. Paulson.
    Program composition in Isabelle/UNITY. In: Michel Charpentier and Beverly Sanders (editors),Formal Methods for Parallel Programming: Theory and Application (2002).
  49. L. C. Paulson.
    The reflection theorem: a study in meta-theoretic reasoning.
    In: A. Voronkov (editor), 18th International Conf. on Automated Deduction: CADE-18 (Springer LNAI 2392, 2002), 377–391. Publisher's versionSlides available
  50. Giampaolo Bella, Fabio Massacci and L. C. Paulson.
    In: Vijay Atluri (editor), 9th ACM Conference on Computer and Communications Security (ACM Press, 2002), pages 12–20.
  51. Giampaolo Bella, Fabio Massacci and L. C. Paulson.
    Verifying the SET registration protocols. IEEE Journal on Selected Areas in Communications 21 1 (2003), 77–87.
  52. Giampaolo Bella, Cristiano Longo and L. C. Paulson.
    Verifying second-level security protocols. In: David Basin and Burkhart Wolff (editors),Theorem Proving in Higher Order Logics (Springer LNCS 2758, 2003), pages 352-366. Slides available
  53. L. C. Paulson.
    The relative consistency of the axiom of choice mechanized using Isabelle/ZF.
    LMS J. Computation and Mathematics 6 (2003), 198-248. Slides and theory document available
  54. Jia Meng and L. C. Paulson.
    Experiments on supporting interactive proof using resolution. In: David Basin and Michaël Rusinowitch (editors), Automated Reasoning-Second International Joint Conference, IJCAR 2004 (Springer LNCS 3097, 2004), 372-384. Publisher's version
  55. L. C. Paulson.
    Organizing numerical theories using axiomatic type classes. J. Automated Reasoning 33 1 (2004), 29–49. Publisher's versionSlides available
  56. Giampaolo Bella, Fabio Massacci and L. C. Paulson.
    An overview of the verification of SET. International J. Information Security 4 (2005), 17–28. Publisher's version
  57. Sidi O. Ehmety and L. C. Paulson.
    Mechanizing compositional reasoning for concurrent systems: some lessons. Formal Aspects of Computing 17 (2005), 58–68. Publisher's version
  58. Tobias Nipkow and L. C. Paulson. Proof Pearl: defining functions over finite sets. In: Joe Hurd and Tom Melham (editors),Theorem Proving in Higher Order Logics (Springer LNCS 3603, 2005), 385-396. Publisher's version
  59. L. C. Paulson.
    ACM Trans. on Computational Logic 7 4 (2006), 658–675. Slides available
  60. Giampaolo Bella, Fabio Massacci and L. C. Paulson.
    Verifying the SET purchase protocols. J. Automated Reasoning 36 (2006), 5–37. Publisher's version
  61. Jia Meng, Claire Quigley and L. C. Paulson.
    Automation for interactive proof: first prototype. Information and Computation 204 10 (2006), 1575–1596. Publisher's version
  62. Giampaolo Bella and L. C. Paulson.
    ACM Trans. on Information and System Security 9 2 (2006), 138–161.
  63. Jia Meng and L. C. Paulson.
    Lightweight relevance filtering for machine-generated resolution problems. In: Geoff Sutcliffe, Renate Schmidt and Stephan Schulz (editors), ESCoR: Empirically Successful Computerized Reasoning (CEUR Workshop Proceedings, Vol. 192, 2006), 53-69. (See journal version below.)
  64. Jia Meng and L. C. Paulson.
    Translating higher-order problems to first-order clauses. In: Geoff Sutcliffe, Renate Schmidt and Stephan Schulz (editors), ESCoR: Empirically Successful Computerized Reasoning (CEUR Workshop Proceedings, Vol. 192, 2006), 70-80.
  65. Behzad Akbarpour and L. C. Paulson.
    Towards automatic proofs of inequalities involving elementary functions. In: Byron Cook and Roberto Sebastiani (editors), PDPAR 2006: Pragmatics of Decision Procedures in Automated Reasoning, 27-37.
  66. Jia Meng, L. C. Paulson and Gerwin Klein
    A termination checker for Isabelle Hoare logic. In: Bernhard Beckert (editor), 4th International Verification Workshop, VERIFY'07 (CEUR Workshop Proceedings, Vol. 259, 2007), 104–118.
  67. L. C. Paulson and Kong Woei Susanto.
    Source-level proof reconstruction for interactive theorem proving. In: Klaus Schneider and Jens Brandt (editors), Theorem Proving in Higher Order Logics (Springer LNCS 4732, 2007), 232–245. Publisher's versionSlides available
  68. Behzad Akbarpour and L. C. Paulson.
    Extending a resolution prover for inequalities on elementary functions. In: Nachum Dershowitz and Andrei Voronkov (editors), Logic for Programming, Artificial Intelligence, and Reasoning - LPAR 2007 (Springer LNCS 4790), 47–61. Publisher's version at www.springerlink.com
  69. Jia Meng and L. C. Paulson.
    Translating higher-order clauses to first-order clauses. J. Automated Reasoning 40 1 (2008), 35–60. Test data availablePublisher's version at www.springerlink.com
  70. Behzad Akbarpour and L. C. Paulson.
    MetiTarski: an automatic prover for the elementary functions. In: Serge Autexier et al. (editors), Intelligent Computer Mathematics (Springer LNCS 5144, 2008), 217–231. (Proceedings of Calculemus 2008.) Publisher's versionSlides available
  71. Christoph Benzmüller, L. C. Paulson, Frank Theiss and Arnaud Fietzke.
    LEO-II - a cooperative automatic theorem prover for classical higher-order logic. In: Alessandro Armando, Peter Baumgartner, Gilles Dowek (editors), Automated Reasoning—4th International Joint Conference, IJCAR 2008 (Springer LNCS 5195, 2008), 162–170. Publisher's version at www.springerlink.com
  72. Jia Meng and L. C. Paulson.
    Lightweight relevance filtering for machine-generated resolution problems. J. Applied Logic 7 1 (2009), 41-57. Test data availablePublisher's version
  73. Behzad Akbarpour and L. C. Paulson.
    Applications of MetiTarski in the verification of control and hybrid systems. In: Rupak Majumdar and Paulo Tabuada (editors), Hybrid Systems: Computation and Control (Springer LNCS 5469, 2009), 1–15. Publisher's version at www.springerlink.com
  74. William Denman, Behzad Akbarpour, Sofiène Tahar, Mohamed H. Zaki and L. C. Paulson.
    Formal verification of analog designs using MetiTarski.
    In: Armin Biere and Carl Pixley (editors), Formal Methods in Computer Aided Design (2009), 93–100. Publisher's version at ieeexplore.ieee.org
  75. Behzad Akbarpour and L. C. Paulson.
    MetiTarski: an automatic theorem prover for real-valued special functions. J. Automated Reasoning 44 3 (2010), 175–205. Publisher's version at www.springerlink.com
  76. Rajeev Narayanan, Behzad Akbarpour, Mohamed H. Zaki, Sofiène Tahar and L. C. Paulson.
    Formal verification of analog circuits in the presence of noise and process variation. In: DATE 2010: Design, Automation and Test in Europe, 1309–1312.
  77. Christoph Benzmüller and L. C. Paulson.
    Multimodal and intuitionistic logics in simple type theory.
    Logic Journal of the IGPL 18 6 (2010), 881–892.
  78. Jasmin Christian Blanchette, Sascha Böhme and L. C. Paulson.
    Extending Sledgehammer with SMT solvers.
    In: Nikolaj Bjørner and Viorica Sofronie-Stokkermans (editors), 23rd International Conf. on Automated Deduction: CADE-23 (Springer LNAI 6803, 2011), 116–130. Publisher's version at www.springerlink.com
  79. Grant O. Passmore, L. C. Paulson and Leonardo de Moura.
    Real algebraic strategies for metitarski proofs. In: Johan Jeuring (editor), Conferences on Intelligent Computer Mathematics --- CICM 2012 (Springer LNCS 7362, 2012), 358–370. Publisher's version at www.springerlink.com
  80. Christoph Benzmüller and L. C. Paulson.
    Quantified multimodal logics in simple type theory. Logica Universalis 7 1 (2013), 7–20. Publisher's version at www.springerlink.com
  81. James P. Bridge and L. C. Paulson.
    Case splitting in an automatic theorem prover for real-valued special functions.
    J. Automated Reasoning 50 1 (2013), 99–117. Raw data availablePublisher's version at www.springerlink.com
  82. Nik Sultana, Jasmin Christian Blanchette and L. C. Paulson.
    LEO-II and Satallax on the Sledgehammer test bench. J. Applied Logic 11 1 (2013), 91–102. Publisher's version
  83. Jasmin Christian Blanchette, Sascha Böhme and L. C. Paulson.
    Extending Sledgehammer with SMT solvers.
    J. Automated Reasoning 51 1 (2013), 109–128. Publisher's version at www.springerlink.com
  84. Jean E. Martina and L. C. Paulson.
    ACM DL Author-ize serviceVerifying multicast-based security protocols using the inductive method
    SAC '13 Proceedings of the 28th Annual ACM Symposium on Applied Computing (2013), 1824–1829
  85. James P. Bridge, Sean B. Holden and L. C. Paulson.
    Machine learning for first-order theorem proving: learning to select a good heuristic.
    J. Automated Reasoning 53 2 (2014), 141–172. Publisher's version at www.springerlink.com
  86. L. C. Paulson.
    A machine-assisted proof of Gödel’s incompleteness theorems for the theory of hereditarily finite sets.
    Review of Symbolic Logic 7 3 (2014), 484–498. Publisher's version at journals.cambridge.org
    © Association for Symbolic Logic, 2014
  87. Paul Jackson, Andrew Sogokon, James Bridge, L. C. Paulson.
    Verifying hybrid systems involving transcendental functions.
    In: Julia M. Badger and Kristin Y. Rozier (editors), NASA Formal Methods (Springer LNCS 8430, 2014), 188–202. Publisher's version at www.springerlink.com
  88. Zongyan Huang, Matthew England, David Wilson, James H. Davenport, L. C. Paulson and James Bridge.
    Applying machine learning to the problem of choosing a heuristic to select the variable ordering for cylindrical algebraic decomposition.
    In: Stephen Watt (editor), Intelligent Computer Mathematics (Springer LNAI 8543, 2014), 92–107.
  89. Zongyan Huang, Matthew England, David Wilson, James H. Davenport and L. C. Paulson.
    A comparison of three heuristics to choose the variable ordering for CAD.
    In: ISSAC 2014: International Symposium on Symbolic and Algebraic Computation (abstract for poster session). Also ACM Communications in Computer Algebra 48 3 (September 2014), in press.
  90. Jean E. Martina and L. C. Paulson.
    Verifying multicast-based security protocols using the inductive method.
    International Journal of Information Security (2014), in press. Publisher's version at www.springerlink.com

Last revised: 22 September, 2014


Lawrence C. PaulsonComputer LaboratoryUniversity of Cambridge