Refereed Articles

The full texts of all my articles are available free of charge, both from this page and (in most cases) from online repositories such as ArXiV or Cambridge's Apollo.

  1. L. C. Paulson.
    A semantics-directed compiler generator. Principles of Programming Languages (1982), 224–233. Publisher's version
  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. Publisher's version
  4. L. C. Paulson.
    Verifying the unification algorithm in LCF. Science of Computer Programming 5 (1985), 143–170. Publisher's version
  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. Publisher's version
  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. Publisher's version
  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. Publisher's version
  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 availablePublisher's version
  18. L. C. Paulson.
    Set theory for verification: II. Induction and recursion. J. Automated Reasoning 15 (1995), 167–215. Publisher's version
  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. Publisher's version
  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
  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. Publisher's version
  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. Publisher's version
  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. Inductive analysis of the Internet protocol TLS.
    ACM Trans. on Information and System Security 2:3 (1999), 332–351. Publisher's versionSlides 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.
    Should your specification language be typed?
    ACM Trans. on Programming Languages and Systems
    21:3 (1999), 502–526. Publisher's version
  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. Publisher's version
  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.
    Mechanizing UNITY in Isabelle ACM Trans. on Computational Logic 1:1 (2000), 3–32. Publisher's version
  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. Publisher's version
  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. Publisher's version
  47. L. C. Paulson.
    Mechanizing a theory of program composition for UNITY ACM Trans. on Programming Languages and Systems 25:5 (2001), 626–656. Publisher's version
  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.
    The verification of an industrial payment protocol: the SET purchase phase.
    In: Vijay Atluri (editor), 9th ACM Conference on Computer and Communications Security (ACM Press, 2002), pages 12–20. Publisher's version
  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. Publisher's versionSlides 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.
    Defining functions on equivalence classes. ACM Trans. on Computational Logic 7:4 (2006), 658–675 Publisher's versionSlides 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.
    Accountability protocols: formalized and verified ACM Trans. on Information and System Security 9:2 (2006), 138–161. Publisher's version
  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
  69. Jia Meng and L. C. Paulson.
    Translating higher-order clauses to first-order clauses. J. Automated Reasoning 40:1 (2008), 35–60. Publisher's version
  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 LNAI 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
  72. Jia Meng and L. C. Paulson.
    Lightweight relevance filtering for machine-generated resolution problems. J. Applied Logic 7:1 (2009), 41-57. Publisher'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
  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
  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
  79. Grant O. Passmore, L. C. Paulson and Leonardo de Moura.
    Real algebraic strategies for Metitarski proofs. In: Johan Jeuring (editor), Intelligent Computer Mathematics (Springer LNAI 7362, 2012), 358–370. Publisher's version
  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
  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
  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
  84. Jean E. Martina and L. C. Paulson.
    Verifying multicast-based security protocols using the inductive method.
    SAC '13 Proceedings of the 28th Annual ACM Symposium on Applied Computing (2013), 1824–1829. Publisher's version
  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
  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
  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. Publisher's version
  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 (poster abstract). Also ACM Communications in Computer Algebra 48:3 (2014), 121–123. Publisher's version
  90. Jean E. Martina and L. C. Paulson.
    Verifying multicast-based security protocols using the inductive method.
    International Journal of Information Security 14:2 (2015), 187–204. Publisher's version
  91. L. C. Paulson.
    A mechanised proof of Gödel's incompleteness theorems using Nominal Isabelle.

    J. Automated Reasoning 55:1 (2015), 1–37. Publisher's version
  92. L. C. Paulson. A formalisation of finite automata using hereditarily finite sets.
    In: Amy P. Felty and Aart Middeldorp (editors), 25th International Conf. on Automated Deduction: CADE-25 (Springer LNAI 9195, 2015), 231–245. Publisher's version
  93. Christoph Benzmüller, Nik Sultana, L. C. Paulson and Frank Theiss.
    The higher-order prover Leo-II.
    J. Automated Reasoning 55:4 (2015), 389–404.
  94. Nik Sultana, Christoph Benzmüller and L. C. Paulson.
    Proofs and reconstructions.
    In: Carsten Lutz and Silvio Ranise (editors), International Symposium on Frontiers of Combining Systems — FroCoS'15 (Springer LNAI 9322, 2015), 256–274. Publisher's version
  95. Wenda Li and L. C. Paulson.
    A modular, efficient formalisation of real algebraic numbers.
    In: Jeremy Avigad and Adam Chlipala (editors), CPP 2016 — ACM SIGPLAN Conference on Certified Programs and Proofs (2016), 66–75. Publisher's version
  96. Jasmin C. Blanchette, Cezary Kaliszyk, L. C. Paulson and Josef Urban.
    Hammering towards QED.
    J. Formalized Reasoning 9:1 (2016), 101–148.
  97. Mohammad Abdulaziz and L. C. Paulson. An Isabelle/HOL formalisation of Green’s theorem.
    In: Jasmin C. Blanchette and Stephan Merz (editors), ITP 2016: Seventh International Conference on Interactive Theorem Proving (Springer LNCS 9807, 2016), 3–19. Publisher's version
  98. Wenda Li and L. C. Paulson. A formal proof of Cauchy's residue theorem.
    In: Jasmin C. Blanchette and Stephan Merz (editors), ITP 2016: Seventh International Conference on Interactive Theorem Proving (Springer LNCS 9807, 2016), 235–251. Publisher's version
  99. Zongyan Huang, Matthew England, James H. Davenport and L. C. Paulson.
    Using machine learning to decide when to precondition cylindrical algebraic decomposition with Groebner bases.
    SYNASC 2016: Symposium on Symbolic and Numeric Algorithms for Scientific Computing (2016), 45–52. Publisher's version
  100. L. C. Paulson. Computational logic: its origins and applications.
    Proceedings of the Royal Society Series A 474 2210 (2018). Publisher's version
  101. L. C. Paulson.
    Michael John Caldwell Gordon (FRS 1994), 28 February 1948 — 22 August 2017.
    Biographical Memoirs of Fellows of the Royal Society 65 (2018), 89–113. Publisher's version
  102. Wenda Li and L. C. Paulson.
    Counting polynomial roots in Isabelle/HOL: a formal proof of the Budan-Fourier theorem.
    In: Assia Mahboubi and Magnus Myreen (editors), CPP 2019 — The 8th ACM SIGPLAN International Conference on Certified Programs and Proofs (2019), 52–64.
  103. Wenda Li, Grant Olney Passmore and L. C. Paulson.
    Deciding univariate polynomial problems using untrusted certificates in Isabelle/HOL.
    J. Automated Reasoning 62 (2019), 69–91.
  104. Mohammad Abdulaziz and L. C. Paulson.
    An Isabelle/HOL formalisation of Green’s theorem.
    J. Automated Reasoning 63:3 (2019), 763–786. Publisher's version
  105. Zongyan Huang, Matthew England, David Wilson, James H. Davenport and L. C. Paulson.
    Using machine learning to improve cylindrical algebraic decomposition.
    Mathematics in Computer Science special issue on SYNASC 13:4 (2019), 461–488
  106. Lawrence C. Paulson, Tobias Nipkow and Makarius Wenzel.
    From LCF to Isabelle/HOL.
    Formal Aspects of Computing 31:6 (2019), 675–698.
  107. L. C. Paulson.
    Formalising mathematics in simple type theory.
    In: Stefania Centrone, Deborah Kant and Deniz Sarikaya (editors), Reflections on the Foundations of Mathematics: Univalent Foundations, Set Theory and General Thoughts (Springer, 2019), 437–453. Publisher's version
  108. Wenda Li and L. C. Paulson.
    Evaluating winding numbers and counting complex roots through Cauchy indices in Isabelle/HOL.
    J. Automated Reasoning 64:2 (2020), 331–360.
  109. Paulo Emílio de Vilhena and L. C. Paulson.
    Algebraically closed fields in Isabelle/HOL.
    In: Nicolas Peltier and Viorica Sofronie-Stokkermans (editors), IJCAR 2020 — Automated Reasoning, 10th International Joint Conference, Part II (Springer LNCS 12167, 2020), 204–220. Publisher's version
  110. Chelsea Edmonds and L. C. Paulson.
    A modular first formalisation of combinatorial design theory.
    In: Fairouz Kamareddine and Claudio Sacerdoti Coen (editors), Intelligent Computer Mathematics (Springer LNCS 12833, 2021), 3–18. Publisher's version
  111. L. C. Paulson.
    Ackermann’s function in iterative form: a proof assistant experiment.
    Bulletin of Symbolic Logic, 27:4 (2021), 426–435.
  112. Angeliki Koutsoukou-Argyraki, Wenda Li and L. C. Paulson.
    Irrationality and transcendence criteria for infinite series in Isabelle/HOL.
    Experimental Mathematics 31:2 (2022), 401–412.
  113. Mirna Džamonja, Angeliki Koutsoukou-Argyraki and L. C. Paulson.
    Formalising ordinal partition relations using Isabelle/HOL.
    Experimental Mathematics 31:2 (2022), 383–400.
  114. Samuel Coward, L. C. Paulson, Theo Drane and Emiliano Morini.
    Formal verification of transcendental fixed and floating point algorithms using an automatic theorem prover.
    Formal Aspects of Computing 34:2 (2022), 1–22
  115. Anthony Bordg, L. C. Paulson and Wenda Li.
    Simple type theory is not too simple: Grothendieck's schemes without dependent types.
    Experimental Mathematics 31:2 (2022), 364–382.
  116. Chelsea Edmonds and L. C. Paulson.
    Formalising Fisher’s inequality: formal linear algebraic proof techniques in combinatorics.
    In: June Andronick and Leonardo de Moura (editors), 13th International Conference on Interactive Theorem Proving (2022), 11:1–11:19. Slides available
  117. Chaitanya Mangla, Sean B. Holden and and L. C. Paulson.
    Bayesian ranking for strategy scheduling in automated theorem provers.
    In: Jasmin Blanchette, Laura Kovács and Dirk Pattinson (editors), IJCAR 2022 — Automated Reasoning, 11th International Joint Conference (Springer LNAI 13385, 2022), 559–577.
  118. L. C. Paulson.
    Wetzel: formalisation of an undecidable problem linked to the continuum hypothesis.
    In: Kevin Buzzard and Temur Kutsia (editors), Intelligent Computer Mathematics. (Springer LNAI 13467, 2022), 92–106. Slides available
  119. Chelsea Edmonds, Angeliki Koutsoukou-Argyraki and L. C. Paulson.
    Formalising Szemerédi's regularity lemma and Roth's theorem on arithmetic progressions in Isabelle/HOL. Journal of Automated Reasoning 67:1 (2023).
  120. L. C. Paulson.
    A formalised theorem in the partition calculus.
    Annals of Pure and Applied Logic 175 (2024). Publisher's version
  121. Chelsea Edmonds and L. C. Paulson.
    Formal probabilistic methods for combinatorial structures using the Lovász local lemma.
    In: Brigitte Pientka and Sandrine Blazy (editors), CPP 2024: ACM SIGPLAN International Conference on Certified Programs and Proofs (2024), 132–146. Slides available