skip to content

Department of Computer Science and Technology

  • Professor of Computational Logic

For a full account of my interests and background, please see my personal page. Preprints of my publications can be downloaded there too.

Research

My research concerns automated theorem proving and its applications:

Publications

Journal articles

  • Paulson, LC., 2021. The Inductive Approach to Verifying Cryptographic Protocols. CoRR, v. abs/2105.06319
  • Bordg, A., Paulson, LC. and Li, W., 2021. Grothendieck's Schemes in Algebraic Geometry. Arch. Formal Proofs, v. 2021
  • Li, W. and Paulson, LC., 2020. Evaluating Winding Numbers and Counting Complex Roots Through Cauchy Indices in Isabelle/HOL. J. Autom. Reasoning, v. 64
    Doi: http://doi.org/10.1007/s10817-019-09521-3
  • Paulson, LC., 2020. Ordinal Partitions. Arch. Formal Proofs, v. 2020
  • Li, W. and Paulson, LC., 2020. Evaluating Winding Numbers and Counting Complex Roots Through Cauchy Indices in Isabelle/HOL. J. Autom. Reasoning, v. 64
    Doi: http://doi.org/10.1007/s10817-019-09521-3
  • Paulson, LC., 2020. The Nash-Williams Partition Theorem. Arch. Formal Proofs, v. 2020
  • Li, W., Yu, L., Wu, Y. and Paulson, LC., 2020. Modelling High-Level Mathematical Reasoning in Mechanised Declarative Proofs. CoRR, v. abs/2006.09265
  • Paulson, LC., 2019. Zermelo Fraenkel Set Theory in Higher-Order Logic. Arch. Formal Proofs, v. 2019
  • Huang, Z., England, M., Wilson, DJ., Bridge, JP., Davenport, JH. and Paulson, LC., 2019. Using Machine Learning to Improve Cylindrical Algebraic Decomposition. Math. Comput. Sci., v. 13
    Doi: 10.1007/s11786-019-00394-8
  • Paulson, LC., 2019. Fourier Series. Arch. Formal Proofs, v. 2019
  • Paulson, L., Nipkow, T. and Wenzel, M., 2019. From LCF to Isabelle/HOL Formal Aspects of Computing, v. 31
    Doi: http://doi.org/10.1007/s00165-019-00492-1
  • Abdulaziz, M. and Paulson, LC., 2019. An Isabelle/HOL Formalisation of Green’s Theorem Journal of Automated Reasoning, v. 63
    Doi: http://doi.org/10.1007/s10817-018-9495-z
  • Paulson, LC., Nipkow, T. and Wenzel, M., 2019. From LCF to Isabelle/HOL Formal Aspects of Computing, v. 31
    Doi: http://doi.org/10.1007/s00165-019-00492-1
  • Paulson, LC., 2019. Zermelo Fraenkel Set Theory in Higher-Order Logic. Arch. Formal Proofs, v. 2019
  • Abdulaziz, M. and Paulson, LC., 2019. An Isabelle/HOL Formalisation of Green’s Theorem Journal of Automated Reasoning, v. 63
    Doi: 10.1007/s10817-018-9495-z
  • Paulson, LC., 2019. Fourier Series. Arch. Formal Proofs, v. 2019
  • Paulson, LC., Nipkow, T. and Wenzel, M., 2019. From LCF to Isabelle/HOL Formal Aspects of Computing, v. 31
    Doi: 10.1007/s00165-019-00492-1
  • Li, W., Passmore, GO. and Paulson, LC., 2019. Deciding Univariate Polynomial Problems Using Untrusted Certificates in Isabelle/HOL JOURNAL OF AUTOMATED REASONING, v. 62
    Doi: http://doi.org/10.1007/s10817-017-9424-6
  • Paulson, L., Nipkow, T. and Wenzel, M., 2019. From LCF to Isabelle/HOL Formal Aspects of Computing, v. 31
    Doi: http://doi.org/10.1007/s00165-019-00492-1
  • Li, W., Passmore, GO. and Paulson, LC., 2019. Deciding Univariate Polynomial Problems Using Untrusted Certificates in Isabelle/HOL JOURNAL OF AUTOMATED REASONING, v. 62
    Doi: http://doi.org/10.1007/s10817-017-9424-6
  • Eberl, M. and Paulson, LC., 2018. The Prime Number Theorem. Arch. Formal Proofs, v. 2018
  • Paulson, LC., 2018. Predicting Failure of the University COMMUNICATIONS OF THE ACM, v. 61
  • Avigad, J., Blanchette, JC., Klein, G., Paulson, L., Popescu, A. and Snelting, G., 2018. Introduction to Milestones in Interactive Theorem Proving Journal of Automated Reasoning, v. 61
    Doi: http://doi.org/10.1007/s10817-018-9465-5
  • Paulson, LC., 2018. Michael John Caldwell Gordon (FRS 1994), 28 February 1948 -- 22 August 2017 Biographical memoirs of fellows of the Royal Society. Royal Society (Great Britain), v. 65
    Doi: http://doi.org/10.1098/rsbm.2018.0019
  • Paulson, LC., 2018. Predicting Failure of the University COMMUNICATIONS OF THE ACM, v. 61
  • Eberl, M. and Paulson, LC., 2018. The Prime Number Theorem. Arch. Formal Proofs, v. 2018
  • Avigad, J., Blanchette, JC., Klein, G., Paulson, L., Popescu, A. and Snelting, G., 2018. Introduction to Milestones in Interactive Theorem Proving Journal of Automated Reasoning, v. 61
    Doi: http://doi.org/10.1007/s10817-018-9465-5
  • Paulson, LC., 2018. Michael John Caldwell Gordon (FRS 1994), 28 February 1948 -- 22 August 2017 Biographical memoirs of fellows of the Royal Society. Royal Society (Great Britain), v. 65
    Doi: http://doi.org/10.1098/rsbm.2018.0019
  • Paulson, LC., 2017. Time to Retire 'Computational Thinking'? COMMUNICATIONS OF THE ACM, v. 60
  • Paulson, LC., 2017. Time to Retire 'Computational Thinking'? COMMUNICATIONS OF THE ACM, v. 60
  • Li, W. and Paulson, LC., 2016. A formal proof of Cauchy’s residue theorem Lecture Notes in Computer Science, v. 9807
    Doi: http://doi.org/10.1007/978-3-319-43144-4_15
  • Paulson, LC., 2016. The Cartan Fixed Point Theorems. Arch. Formal Proofs, v. 2016
  • Abdulaziz, M. and Paulson, LC., 2016. An Isabelle/HOL formalisation of Green’s theorem Lecture Notes in Computer Science, v. 9807
    Doi: http://doi.org/10.1007/978-3-319-43144-4_1
  • Li, W. and Paulson, LC., 2016. A formal proof of Cauchy’s residue theorem Lecture Notes in Computer Science, v. 9807
    Doi: http://doi.org/10.1007/978-3-319-43144-4_15
  • Hibon, Q. and Paulson, LC., 2016. Source Coding Theorem. Arch. Formal Proofs, v. 2016
  • Blanchette, JC., Kaliszyk, C., Paulson, LC. and Urban, J., 2016. Hammering towards QED Journal of Formalized Reasoning, v. 9
  • Blanchette, JC., Kaliszyk, C., Paulson, LC. and Urban, J., 2016. Hammering towards QED Journal of Formalized Reasoning, v. 9
  • Hibon, Q. and Paulson, LC., 2016. Source Coding Theorem. Arch. Formal Proofs, v. 2016
  • Abdulaziz, M. and Paulson, LC., 2016. An Isabelle/HOL formalisation of Green’s theorem Lecture Notes in Computer Science, v. 9807
    Doi: http://doi.org/10.1007/978-3-319-43144-4_1
  • Paulson, LC., 2015. Finite Automata in Hereditarily Finite Set Theory. Arch. Formal Proofs, v. 2015
  • Martina, JE. and Paulson, LC., 2015. Verifying multicast-based security protocols using the inductive method International Journal of Information Security, v. 14
    Doi: http://doi.org/10.1007/s10207-014-0251-z
  • Paulson, LC., 2015. A Mechanised Proof of Gödel’s Incompleteness Theorems Using Nominal Isabelle Journal of Automated Reasoning,
    Doi: http://doi.org/10.1007/s10817-015-9322-8
  • Martina, JE. and Paulson, LC., 2015. Verifying multicast-based security protocols using the inductive method International Journal of Information Security, v. 14
    Doi: 10.1007/s10207-014-0251-z
  • Paulson, LC., 2015. A Formalisation of Finite Automata using Hereditarily Finite Sets. CoRR, v. abs/1505.01662
  • Paulson, LC., 2015. A Mechanised Proof of Gödel’s Incompleteness Theorems Using Nominal Isabelle Journal of Automated Reasoning,
    Doi: http://doi.org/10.1007/s10817-015-9322-8
  • Paulson, LC., 2015. Abolish Software Warranty Disclaimers COMMUNICATIONS OF THE ACM, v. 58
  • Paulson, LC., 2015. A Mechanised Proof of Gödel’s Incompleteness Theorems Using Nominal Isabelle Journal of Automated Reasoning, v. 55
    Doi: http://doi.org/10.1007/s10817-015-9322-8
  • Benzmüller, C., Sultana, N., Paulson, LC. and Theiß, F., 2015. The Higher-Order Prover Leo-II. J Autom Reason, v. 55
    Doi: http://doi.org/10.1007/s10817-015-9348-y
  • Benzmüller, C., Sultana, N., Paulson, LC. and Theiß, F., 2015. The Higher-Order Prover Leo-II. J Autom Reason, v. 55
    Doi: http://doi.org/10.1007/s10817-015-9348-y
  • Paulson, LC., 2015. A Mechanised Proof of Gödel’s Incompleteness Theorems Using Nominal Isabelle Journal of Automated Reasoning, v. 55
    Doi: 10.1007/s10817-015-9322-8
  • Paulson, LC., 2015. Finite Automata in Hereditarily Finite Set Theory. Arch. Formal Proofs, v. 2015
  • PAULSON, LC., 2014. A MACHINE-ASSISTED PROOF OF GÖDEL'S INCOMPLETENESS THEOREMS FOR THE THEORY OF HEREDITARILY FINITE SETS Review of Symbolic Logic,
    Doi: http://doi.org/10.1017/S1755020314000112
  • Paulson, LC., 2014. Real-Valued Special Functions: Upper and Lower Bounds. Arch. Formal Proofs, v. 2014
  • Paulson, LC., 2014. Provenance of British Computing COMMUNICATIONS OF THE ACM, v. 57
  • Paulson, LC., 2014. Theorem proving and the real numbers: Overview and challenges Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), v. 8430 LNCS
  • Bridge, JP., Holden, SB. and Paulson, LC., 2014. Machine Learning for First-Order Theorem Proving Journal of Automated Reasoning,
  • Paulson, LC., 2014. Real-Valued Special Functions: Upper and Lower Bounds. Arch. Formal Proofs, v. 2014
  • Bridge, JP., Holden, SB. and Paulson, LC., 2014. Machine learning for first-order theorem proving: Learning to select a good Heuristic Journal of Automated Reasoning, v. 53
    Doi: http://doi.org/10.1007/s10817-014-9301-5
  • Paulson, LC., 2014. Theorem proving and the real numbers: Overview and challenges Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), v. 8430 LNCS
  • Bridge, JP., Holden, SB. and Paulson, LC., 2014. Machine learning for first-order theorem proving: Learning to select a good Heuristic Journal of Automated Reasoning, v. 53
    Doi: http://doi.org/10.1007/s10817-014-9301-5
  • Paulson, LC., 2014. Automated theorem proving for special functions: The next phase Proceedings of the 2014 Symposium on Symbolic-Numeric Computation, SNC 2014,
    Doi: http://doi.org/10.1145/2631948.2631950
  • Huang, Z., England, M., Wilson, D., Davenport, JH., Paulson, LC. and Bridge, J., 2014. Applying machine learning to the problem of choosing a heuristic to select the variable ordering for cylindrical algebraic decomposition Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), v. 8543 LNAI
    Doi: http://doi.org/10.1007/978-3-319-08434-3_8
  • Paulson, LC., 2014. A machine-assisted proof of Gödel's incompleteness theorems for the theory of hereditarily finite sets Review of Symbolic Logic, v. 7
    Doi: http://doi.org/10.1017/S1755020314000112
  • Huang, Z., England, M., Wilson, DJ., Davenport, JH., Paulson, LC. and Bridge, JP., 2014. Applying machine learning to the problem of choosing a heuristic to select the variable ordering for cylindrical algebraic decomposition. CoRR, v. abs/1404.6369
  • PAULSON, LC., 2014. A MACHINE-ASSISTED PROOF OF GÖDEL'S INCOMPLETENESS THEOREMS FOR THE THEORY OF HEREDITARILY FINITE SETS Review of Symbolic Logic,
    Doi: http://doi.org/10.1017/S1755020314000112
  • Paulson, LC., 2014. Automated theorem proving for special functions: The next phase Proceedings of the 2014 Symposium on Symbolic-Numeric Computation, SNC 2014,
    Doi: http://doi.org/10.1145/2631948.2631950
  • Paulson, LC., 2014. A machine-assisted proof of Gödel's incompleteness theorems for the theory of hereditarily finite sets Review of Symbolic Logic, v. 7
    Doi: 10.1017/S1755020314000112
  • Huang, Z., England, M., Wilson, DJ., Davenport, JH., Paulson, LC. and Bridge, JP., 2014. Applying machine learning to the problem of choosing a heuristic to select the variable ordering for cylindrical algebraic decomposition. CoRR, v. abs/1404.6369
  • Paulson, LC., 2014. Provenance of British Computing COMMUNICATIONS OF THE ACM, v. 57
  • Bridge, JP., Holden, SB. and Paulson, LC., 2014. Machine Learning for First-Order Theorem Proving Journal of Automated Reasoning,
  • Paulson, LC., 2013. The Hereditarily Finite Sets. Arch. Formal Proofs, v. 2013
  • Paulson, LC., 2013. Gödel's Incompleteness Theorems. Arch. Formal Proofs, v. 2013
  • Paulson, LC., 2013. The Hereditarily Finite Sets. Arch. Formal Proofs, v. 2013
  • Paulson, LC., 2013. Gödel's Incompleteness Theorems. Arch. Formal Proofs, v. 2013
  • Bridge, JP. and Paulson, LC., 2013. Case splitting in an automatic theorem prover for real-valued special functions Journal of Automated Reasoning, v. 50
    Doi: http://doi.org/10.1007/s10817-012-9245-6
  • Sultana, N., Blanchette, JC. and Paulson, LC., 2013. LEO-II and Satallax on the Sledgehammer test bench Journal of Applied Logic, v. 11
    Doi: http://doi.org/10.1016/j.jal.2012.12.002
  • Bridge, JP. and Paulson, LC., 2013. Case splitting in an automatic theorem prover for real-valued special functions Journal of Automated Reasoning, v. 50
    Doi: 10.1007/s10817-012-9245-6
  • Paulson, LC., 2013. What we want from computer science Communications of the ACM, v. 56
    Doi: http://doi.org/10.1145/2483852.2483856
  • Blanchette, JC., Böhme, S. and Paulson, LC., 2013. Extending sledgehammer with SMT solvers Journal of Automated Reasoning, v. 51
    Doi: http://doi.org/10.1007/s10817-013-9278-5
  • Sultana, N., Blanchette, JC. and Paulson, LC., 2013. LEO-II and Satallax on the Sledgehammer test bench Journal of Applied Logic, v. 11
    Doi: http://doi.org/10.1016/j.jal.2012.12.002
  • Paulson, LC., 2013. What we want from computer science Communications of the ACM, v. 56
    Doi: http://doi.org/10.1145/2483852.2483856
  • Benzmüller, C. and Paulson, LC., 2013. Quantified Multimodal Logics in Simple Type Theory Logica Universalis, v. 7
    Doi: http://doi.org/10.1007/s11787-012-0052-y
  • Martina, JE. and Paulson, LC., 2013. Verifying multicast-based security protocols using the inductive method Proceedings of the ACM Symposium on Applied Computing,
    Doi: http://doi.org/10.1145/2480362.2480703
  • Blanchette, JC., Böhme, S. and Paulson, LC., 2013. Extending sledgehammer with SMT solvers Journal of Automated Reasoning, v. 51
    Doi: http://doi.org/10.1007/s10817-013-9278-5
  • Benzmüller, C. and Paulson, LC., 2013. Quantified Multimodal Logics in Simple Type Theory Logica Universalis, v. 7
    Doi: http://doi.org/10.1007/s11787-012-0052-y
  • Martina, JE. and Paulson, LC., 2013. Verifying multicast-based security protocols using the inductive method Proceedings of the ACM Symposium on Applied Computing,
    Doi: http://doi.org/10.1145/2480362.2480703
  • Paulson, LC., 2012. What liability for faulty software? Communications of the ACM, v. 55
    Doi: http://doi.org/10.1145/2076450.2076452
  • Romanos, R. and Paulson, LC., 2012. Proving the Impossibility of Trisecting an Angle and Doubling the Cube. Arch. Formal Proofs, v. 2012
  • Paulson, LC., 2012. What liability for faulty software? Communications of the ACM, v. 55
    Doi: http://doi.org/10.1145/2076450.2076452
  • Romanos, R. and Paulson, LC., 2012. Proving the Impossibility of Trisecting an Angle and Doubling the Cube. Arch. Formal Proofs, v. 2012
  • Blanchette, JC., Böhme, S. and Paulson, LC., 2011. Extending sledgehammer with SMT solvers Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), v. 6803 LNAI
    Doi: http://doi.org/10.1007/978-3-642-22438-6_11
  • Blanchette, JC., Böhme, S. and Paulson, LC., 2011. Extending sledgehammer with SMT solvers Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), v. 6803 LNAI
    Doi: http://doi.org/10.1007/978-3-642-22438-6_11
  • Paulson, LC., 2010. Robin Milner The Elegant Pragmatist (vol 53, pg 20, 2010) COMMUNICATIONS OF THE ACM, v. 53
  • Benzmueller, C. and Paulson, LC., 2010. Multimodal and Intuitionistic Logics in Simple Type Theory Logic Jnl IGPL,
    Doi: http://doi.org/10.1093/jigpal/jzp080
  • Benzmueller, C. and Paulson, LC., 2010. Multimodal and Intuitionistic Logics in Simple Type Theory Logic Jnl IGPL,
    Doi: http://doi.org/10.1093/jigpal/jzp080
  • Akbarpour, B. and Paulson, LC., 2010. MetiTarski: An Automatic Theorem Prover for Real-Valued Special Functions J AUTOM REASONING, v. 44
    Doi: http://doi.org/10.1007/s10817-009-9149-2
  • Akbarpour, B. and Paulson, LC., 2010. MetiTarski: An Automatic Theorem Prover for Real-Valued Special Functions J AUTOM REASONING, v. 44
    Doi: http://doi.org/10.1007/s10817-009-9149-2
  • Paulson, LC., 2009. Refocus Fragmented CS Conference Culture COMMUNICATIONS OF THE ACM, v. 52
  • Akbarpour, B. and Paulson, LC., 2009. MetiTarski: An Automatic Theorem Prover for Real-Valued Special Functions Journal of Automated Reasoning,
  • Akbarpour, B. and Paulson, LC., 2009. MetiTarski: An Automatic Theorem Prover for Real-Valued Special Functions Journal of Automated Reasoning,
  • Meng, J. and Paulson, LC., 2009. Lightweight relevance filtering for machine-generated resolution problems J APPL LOGIC, v. 7
    Doi: http://doi.org/10.1016/j.jal.2007.07.004
  • Meng, J. and Paulson, LC., 2009. Lightweight relevance filtering for machine-generated resolution problems J APPL LOGIC, v. 7
    Doi: http://doi.org/10.1016/j.jal.2007.07.004
  • Paulson, LC., 2009. Refocus Fragmented CS Conference Culture COMMUNICATIONS OF THE ACM, v. 52
  • Meng, J. and Paulson, LC., 2009. Lightweight relevance filtering for machine-generated resolution problems J APPL LOGIC, v. 7
    Doi: http://doi.org/10.1016/j.jal.2007.07.004
  • Paulson, LC., 2009. Refocus fragmented CS conference culture [3] Communications of the ACM, v. 52
    Doi: http://doi.org/10.1145/1536616.1536619
  • Paulson, LC., 2009. Refocus fragmented CS conference culture [3] Communications of the ACM, v. 52
    Doi: http://doi.org/10.1145/1536616.1536619
  • Akbarpour, B. and Paulson, L., 2008. MetiTarski: An Automatic Prover for the Elementary Functions Intelligent Computer Mathematics,
  • Nipkow, T. and Paulson, LC., 2008. Fun With Tilings. Arch. Formal Proofs, v. 2008
  • Nipkow, T. and Paulson, LC., 2008. Fun With Tilings. Arch. Formal Proofs, v. 2008
  • Akbarpour, B. and Paulson, L., 2008. MetiTarski: An Automatic Prover for the Elementary Functions Intelligent Computer Mathematics,
  • Meng, J. and Paulson, LC., 2008. Translating higher-order clauses to first-order clauses J AUTOM REASONING, v. 40
    Doi: http://doi.org/10.1007/s10817-007-9085-y
  • Beckert, B. and Paulson, LC., 2007. Journal of Automated Reasoning: Preface Journal of Automated Reasoning, v. 38
    Doi: http://doi.org/10.1007/s10817-006-9058-6
  • Beckert, B. and Paulson, LC., 2007. Journal of Automated Reasoning: Preface Journal of Automated Reasoning, v. 38
    Doi: http://doi.org/10.1007/s10817-006-9058-6
  • Beckert, B. and Paulson, LC., 2007. Special issue on automated reasoning with analytic tableaux - Preface J AUTOM REASONING, v. 38
    Doi: http://doi.org/10.1007/s10817-006-9058-6
  • Paulson, LC., 2007. Even a good abstraction needs experience and testing, too COMMUNICATIONS OF THE ACM, v. 50
  • Paulson, LC., 2007. Even a good abstraction needs experience and testing, too COMMUNICATIONS OF THE ACM, v. 50
  • Meng, J., Quigley, C. and Paulson, LC., 2006. Automation for Interactive Proof: First Prototype Information and Computation, v. 204
  • Paulson, LC., 2006. Defining Functions on Equivalence Classes TOCL, v. 7
    Doi: http://doi.org/10.1145/1166109.1166111
  • Meng, J., Quigley, C. and Paulson, LC., 2006. Erratum to "Automation for interactive proof: First prototype" [Inform. and Comput. 204 (2006) 1575-1596] (DOI:10.1016/j.ic.2005.05.010) Information and Computation, v. 204
  • Meng, J., Quigley, C. and Paulson, LC., 2006. Erratum to "Automation for interactive proof: First prototype" [Inform. and Comput. 204 (2006) 1575-1596] (DOI:10.1016/j.ic.2005.05.010) Information and Computation, v. 204
  • Meng, J., Quigley, C. and Paulson, LC., 2006. Automation for Interactive Proof: First Prototype Information and Computation, v. 204
  • Paulson, LC., 2006. Defining functions on equivalence classes ACM Transactions on Computational Logic, v. 7
    Doi: http://doi.org/10.1145/1166109.1166111
  • Meng, J., Quigley, C. and Paulson, LC., 2006. Automation for interactive proof: First prototype INFORM COMPUT, v. 204
    Doi: http://doi.org/10.1016/j.ic.2005.05.010
  • Bella, G., Massacci, F. and Paulson, LC., 2006. Verifying the SET purchase protocols J AUTOM REASONING, v. 36
    Doi: http://doi.org/10.1007/s10817-005-9018-6
  • Meng, J., Quigley, C. and Paulson, LC., 2006. Automation for interactive proof: First prototype INFORM COMPUT, v. 204
    Doi: http://doi.org/10.1016/j.ic.2005.05.010
  • Paulson, LC., 2006. Defining functions on equivalence classes ACM Transactions on Computational Logic, v. 7
    Doi: http://doi.org/10.1145/1166109.1166111
  • Meng, J., Quigley, C. and Paulson, LC., 2006. Automation for interactive proof: First prototype (vol 204, pg 1575, 2006) INFORM COMPUT, v. 204
    Doi: http://doi.org/10.1016/j.ic.2006.09.004
  • Bella, G. and Paulson, LC., 2006. Accountability protocols: Formalized and verified ACM Trans. Inf. Syst. Secur., v. 9
    Doi: http://doi.org/10.1145/1151414.1151416
  • Bella, G., Massacci, F. and Paulson, LC., 2006. Verifying the SET purchase protocols J AUTOM REASONING, v. 36
    Doi: http://doi.org/10.1007/s10817-005-9018-6
  • Paulson, LC., 2006. Defining Functions on Equivalence Classes TOCL, v. 7
    Doi: http://doi.org/10.1145/1166109.1166111
  • Bella, G., Massacci, F. and Paulson, LC., 2006. Verifying the SET purchase protocols J AUTOM REASONING, v. 36
    Doi: http://doi.org/10.1007/s10817-005-9018-6
  • Bella, G. and Paulson, LC., 2006. Accountability protocols: Formalized and verified ACM Trans. Inf. Syst. Secur., v. 9
    Doi: http://doi.org/10.1145/1151414.1151416
  • Bella, G., Massacci, F. and Paulson, LC., 2005. An Overview of the Verification of SET International Journal of Information Security, v. 4
    Doi: http://doi.org/10.1007/s10207-004-0047-7
  • Bella, G., Massacci, F. and Paulson, LC., 2005. An Overview of the Verification of SET International Journal of Information Security, v. 4
    Doi: http://doi.org/10.1007/s10207-004-0047-7
  • Ehmety, SO. and Paulson, LC., 2005. Mechanizing compositional reasoning for concurrent systems: some lessons FORM ASP COMPUT, v. 17
    Doi: http://doi.org/10.1007/s00165-004-0053-6
  • Paulson, LC., 2005. Welcome defects as a sign of innovation? [1] Communications of the ACM, v. 48
    Doi: http://doi.org/10.1145/1096000.1096016
  • Bella, G., Massacci, F. and Paulson, LC., 2005. An Overview of the Verification of SET International Journal of Information Security, v. 4
    Doi: http://doi.org/10.1007/s10207-004-0047-7
  • Paulson, LC., 2005. Welcome defects as a sign of innovation? [1] Communications of the ACM, v. 48
    Doi: http://doi.org/10.1145/1096000.1096016
  • Bella, G., Massacci, F. and Paulson, LC., 2005. An Overview of the Verification of SET International Journal of Information Security, v. 4
    Doi: http://doi.org/10.1007/s10207-004-0047-7
  • Paulson, LC., 2004. Organizing Numerical Theories Using Axiomatic Type Classes Journal of Automated Reasoning, v. 33
  • Paulson, LC., 2004. Organizing Numerical Theories Using Axiomatic Type Classes Journal of Automated Reasoning, v. 33
  • Paulson, LC., 2004. Organizing Numerical Theories Using Axiomatic Type Classes Journal of Automated Reasoning, v. 33
  • Paulson, LC., 2003. The Relative Consistency of the Axiom of Choice — Mechanized Using Isabelle/ZF LMS Journal of Computation and Mathematics, v. 6
  • Bella, G., Massacci, F. and Paulson, LC., 2003. Verifying the SET registration protocols IEEE J SEL AREA COMM, v. 21
    Doi: http://doi.org/10.1109/JSAC.2002.806133
  • Paulson, LC., 2003. The Relative Consistency of the Axiom of Choice — Mechanized Using Isabelle/ZF LMS Journal of Computation and Mathematics, v. 6
  • Paulson, LC., 2003. The Relative Consistency of the Axiom of Choice — Mechanized Using Isabelle/ZF LMS Journal of Computation and Mathematics, v. 6
  • Paulson, LC., 2003. The Relative Consistency of the Axiom of Choice — Mechanized Using Isabelle/ZF LMS Journal of Computation and Mathematics, v. 6
  • Nipkow, T., Paulson, LC. and Wenzel, M., 2002. The basics LECT NOTES COMPUT SC, v. 2283
  • Paulson, LC., 2001. Relations Between Secrets: Two Formal Analyses of the Yahalom Protocol. J. Comput. Secur., v. 9
  • Paulson, LC., 2001. Mechanizing a Theory of Program Composition for UNITY ACM Transactions on Programming Languages and Systems, v. 25
  • Paulson, LC., 2001. A Simple Formalization and Proof for the Mutilated Chess Board Logic Journal of the IGPL, v. 9
    Doi: http://doi.org/10.1093/jigpal/9.3.475
  • Paulson, LC., 2001. Keep E-journals affordable COMMUNICATIONS OF THE ACM, v. 44
  • Paulson, LC., 2001. Mechanizing a theory of program composition for UNITY ACM T PROGR LANG SYS, v. 23
  • Paulson, LC., 2001. Relations Between Secrets: Two Formal Analyses of the Yahalom Protocol. J. Comput. Secur., v. 9
  • Paulson, LC., 2001. Mechanizing a Theory of Program Composition for UNITY ACM Transactions on Programming Languages and Systems, v. 25
  • Paulson, LC., 2001. A Simple Formalization and Proof for the Mutilated Chess Board Logic Journal of the IGPL, v. 9
    Doi: http://doi.org/10.1093/jigpal/9.3.475
  • Paulson, LC., 2001. Mechanizing a Theory of Program Composition for UNITY ACM Transactions on Programming Languages and Systems, v. 25
  • Paulson, LC., 2001. Keep E-journals affordable COMMUNICATIONS OF THE ACM, v. 44
  • Paulson, LC., 2001. Mechanizing a Theory of Program Composition for UNITY ACM Transactions on Programming Languages and Systems, v. 25
  • Paulson, LC., 2001. Mechanizing a theory of program composition for UNITY ACM T PROGR LANG SYS, v. 23
  • Paulson, LC., 2001. A Simple Formalization and Proof for the Mutilated Chess Board Logic Journal of the IGPL, v. 9
    Doi: http://doi.org/10.1093/jigpal/9.3.475
  • Paulson, LC., 2000. Mechanizing UNITY in Isabelle. ACM Trans. Comput. Log., v. 1
    Doi: 10.1145/343369.343370
  • Roe, M., Lee, S., Christianson, B., Anderson, R., Wheeler, D., Blaze, M., Gollman, D., Gligor, V., Mao, WB., Paulson, L. and Kuhn, M., 2000. Performance of protocols (Transcript of discussion) SECURITY PROTOCOLS, v. 1796
  • Fleuriot, JD. and Paulson, LC., 2000. Mechanizing Nonstandard Real Analysis LMS Journal of Computation and Mathematics, v. 3
  • Fleuriot, JD. and Paulson, LC., 2000. Mechanizing Nonstandard Real Analysis LMS Journal of Computation and Mathematics, v. 3
  • Fleuriot, JD. and Paulson, LC., 2000. Mechanizing Nonstandard Real Analysis LMS Journal of Computation and Mathematics, v. 3
  • Bergadano, F., Morris, B., Roe, M., Lomas, M., Blaze, M., Lee, S., Christianson, B. and Paulson, L., 2000. Issues in multicast security SECURITY PROTOCOLS, v. 1796
  • Fleuriot, JD. and Paulson, LC., 2000. Mechanizing Nonstandard Real Analysis LMS Journal of Computation and Mathematics, v. 3
  • Paulson, LC., 2000. Mechanizing UNITY in Isabelle. ACM Trans. Comput. Log., v. 1
  • Kammuller, F. and Paulson, LC., 1999. A formal proof of Sylow's theorem - An experiment in abstract algebra with Isabelle HOL J AUTOM REASONING, v. 23
  • Kammuller, F. and Paulson, LC., 1999. A formal proof of Sylow's theorem - An experiment in abstract algebra with Isabelle HOL J AUTOM REASONING, v. 23
  • Kammüller, F. and Paulson, LC., 1999. A Formal Proof of Sylow’s theorem: An Experiment in Abstract Algebra with Isabelle HOL Journal of Automated Reasoning, v. 23
    Doi: http://doi.org/10.1023/A:1006269330992
  • Kammüller, F. and Paulson, LC., 1999. A Formal Proof of Sylow’s theorem: An Experiment in Abstract Algebra with Isabelle HOL Journal of Automated Reasoning, v. 23
    Doi: http://doi.org/10.1023/A:1006269330992
  • Lamport, L. and Paulson, LC., 1999. Should Your Specification Language Be Typed? ACM Transactions on Programming Languages and Systems, v. 21
  • Paulson, LC., 1999. A Generic Tableau Prover and its Integration with Isabelle Journal of Universal Computer Science, v. 5
  • Ballarin, C. and Paulson, LC., 1999. A Pragmatic Approach to Extending Provers by Computer Algebra - with Applications to Coding Theory. Fundam. Informaticae, v. 39
    Doi: 10.3233/FI-1999-391201
  • Lamport, L. and Paulson, LC., 1999. Should Your Specification Language Be Typed? ACM Transactions on Programming Languages and Systems, v. 21
  • Lamport, L. and Paulson, LC., 1999. Should Your Specification Language Be Typed? ACM Transactions on Programming Languages and Systems, v. 21
  • Kammüller, F. and Paulson, LC., 1999. A Formal Proof of Sylow’s theorem: An Experiment in Abstract Algebra with Isabelle HOL Journal of Automated Reasoning, v. 23
    Doi: http://doi.org/10.1023/A:1006269330992
  • Lamport, L. and Paulson, LC., 1999. Should Your Specification Language Be Typed? ACM Transactions on Programming Languages and Systems, v. 21
  • Paulson, LC., 1999. Final coalgebras as greatest fixed points in ZF set theory. Math. Struct. Comput. Sci., v. 9
  • Ballarin, C. and Paulson, LC., 1999. A Pragmatic Approach to Extending Provers by Computer Algebra - with Applications to Coding Theory. Fundam. Informaticae, v. 39
  • Paulson, LC., 1999. Final coalgebras as greatest fixed points in ZF set theory. Math. Struct. Comput. Sci., v. 9
  • Ballarin, C. and Paulson, LC., 1999. A Pragmatic Approach to Extending Provers by Computer Algebra - with Applications to Coding Theory. Fundam. Informaticae, v. 39
  • Paulson, LC., 1999. Final coalgebras as greatest fixed points in ZF set theory. Math. Struct. Comput. Sci., v. 9
  • Paulson, LC., 1999. A Generic Tableau Prover and its Integration with Isabelle Journal of Universal Computer Science, v. 5
  • Ballarin, C. and Paulson, LC., 1999. A Pragmatic Approach to Extending Provers by Computer Algebra - with Applications to Coding Theory. Fundam. Informaticae, v. 39
  • Paulson, LC., 1999. A Generic Tableau Prover and its Integration with Isabelle Journal of Universal Computer Science, v. 5
  • Paulson, LC., 1999. A Generic Tableau Prover and its Integration with Isabelle Journal of Universal Computer Science, v. 5
  • Paulson, LC., 1999. Inductive Analysis of the Internet Protocol TLS. ACM Trans. Inf. Syst. Secur., v. 2
  • Paulson, LC., 1999. Inductive Analysis of the Internet Protocol TLS. ACM Trans. Inf. Syst. Secur., v. 2
    Doi: 10.1145/322510.322530
  • Paulson, LC., 1998. The Inductive Approach to Verifying Cryptographic Protocols. J. Comput. Secur., v. 6
  • Paulson, LC., 1998. The Inductive Approach to Verifying Cryptographic Protocols. J. Comput. Secur., v. 6
  • Paulson, LC., 1998. The Inductive Approach to Verifying Cryptographic Protocols. J. Comput. Secur., v. 6
  • Paulson, LC., 1997. Mechanizing coinduction and corecursion in higher-order logic J LOGIC COMPUT, v. 7
  • Paulson, L., 1997. Cobol in question COMMUNICATIONS OF THE ACM, v. 40
  • Paulson, LC., 1997. Mechanizing coinduction and corecursion in higher-order logic J LOGIC COMPUT, v. 7
  • Paulson, LC. and cabczewski, KG., 1996. Mechanizing Set Theory: Cardinal Arithmetic and the Axiom of Choice Journal of Automated Reasoning, v. 17
  • Paulson, LC. and cabczewski, KG., 1996. Mechanizing Set Theory: Cardinal Arithmetic and the Axiom of Choice Journal of Automated Reasoning, v. 17
  • Paulson, LC. and cabczewski, KG., 1996. Mechanizing Set Theory: Cardinal Arithmetic and the Axiom of Choice Journal of Automated Reasoning, v. 17
  • Paulson, LC. and Grabczewski, K., 1996. Mechanizing Set Theory. J. Autom. Reason., v. 17
    Doi: 10.1007/BF00283132
  • Paulson, LC. and cabczewski, KG., 1996. Mechanizing Set Theory: Cardinal Arithmetic and the Axiom of Choice Journal of Automated Reasoning, v. 17
  • Paulson, LC., 1995. A Concrete Final Coalgebra Theorem for ZF Set Theory. CoRR, v. abs/cs/9511103
  • Paulson, LC., 1995. A Concrete Final Coalgebra Theorem for ZF Set Theory. CoRR, v. abs/cs/9511103
  • PAULSON, LC., 1995. SET-THEORY FOR VERIFICATION .2. INDUCTION AND RECURSION J AUTOM REASONING, v. 15
  • Paulson, LC., 1995. Set Theory for Verification: II. Induction and Recursion Journal of Automated Reasoning, v. 15
  • Paulson, LC., 1995. Set Theory for Verification: II. Induction and Recursion Journal of Automated Reasoning, v. 15
  • Paulson, LC., 1995. Set Theory for Verification: II. Induction and Recursion Journal of Automated Reasoning, v. 15
  • Paulson, LC., 1993. Set Theory for Verification: I. From Foundations to Functions Journal of Automated Reasoning, v. 11
  • Paulson, LC., 1993. Set Theory for Verification: I. From Foundations to Functions Journal of Automated Reasoning, v. 11
  • PAULSON, LC., 1993. SET-THEORY FOR VERIFICATION .1. FROM FOUNDATIONS TO FUNCTIONS J AUTOM REASONING, v. 11
  • PAULSON, LC., 1993. SET-THEORY FOR VERIFICATION .1. FROM FOUNDATIONS TO FUNCTIONS J AUTOM REASONING, v. 11
  • PAULSON, LC., 1993. SET-THEORY FOR VERIFICATION .1. FROM FOUNDATIONS TO FUNCTIONS J AUTOM REASONING, v. 11
  • NIPKOW, T. and PAULSON, LC., 1992. ISABELLE-91 LECT NOTES ARTIF INT, v. 607
  • PAULSON, LC., 1990. A FORMULATION OF THE SIMPLE THEORY OF TYPES (FOR ISABELLE) LECT NOTES COMPUT SC, v. 417
  • PAULSON, LC., 1990. A FORMULATION OF THE SIMPLE THEORY OF TYPES (FOR ISABELLE) LECT NOTES COMPUT SC, v. 417
  • PAULSON, LC., 1990. A FORMULATION OF THE SIMPLE THEORY OF TYPES (FOR ISABELLE) LECT NOTES COMPUT SC, v. 417
  • PAULSON, L., COHEN, A. and GORDON, M., 1989. PROGRAM VERIFICATION - THE VERY IDEA COMMUNICATIONS OF THE ACM, v. 32
  • Paulson, LC., 1989. The Foundation of a Generic Theorem Prover. J. Autom. Reason., v. 5
    Doi: 10.1007/BF00248324
  • Paulson, LC., 1989. The Foundation of a Generic Theorem Prover Journal of Automated Reasoning, v. 5
  • Paulson, LC., 1989. The Foundation of a Generic Theorem Prover Journal of Automated Reasoning, v. 5
  • PAULSON, L., COHEN, A. and GORDON, M., 1989. PROGRAM VERIFICATION - THE VERY IDEA COMMUNICATIONS OF THE ACM, v. 32
  • Paulson, LC., 1989. The Foundation of a Generic Theorem Prover. J. Autom. Reason., v. 5
  • Paulson, LC., 1989. The Foundation of a Generic Theorem Prover. J. Autom. Reason., v. 5
  • PAULSON, LC., 1988. ISABELLE - THE NEXT 700 THEOREM PROVERS LECT NOTES COMPUT SC, v. 310
  • Paulson, LC., 1987. Logic and Computation
    Doi: http://doi.org/10.1017/cbo9780511526602
  • Paulson, LC., 1987. Logic and Computation
    Doi: http://doi.org/10.1017/cbo9780511526602
  • Paulson, LC., 1986. Natural Deduction as Higher-order Resolution Journal of Logic Programming, v. 3
  • PAULSON, LC., 1986. CONSTRUCTING RECURSION OPERATORS IN INTUITIONISTIC TYPE THEORY J SYMB COMPUT, v. 2
  • Paulson, LC., 1986. Natural Deduction as Higher-order Resolution Journal of Logic Programming, v. 3
  • Paulson, LC., 1986. Constructing Recursion Operators in Intuitionistic Type Theory. J. Symb. Comput., v. 2
  • Paulson, LC., 1986. Proving Termination of Normalization Functions for Conditional Experessions. J. Autom. Reason., v. 2
    Doi: 10.1007/BF00246023
  • Paulson, LC., 1986. Proving Termination of Normalization Functions for Conditional Expressions Journal of Automated Reasoning, v. 2
    Doi: http://doi.org/10.1007/BF00246023
  • Paulson, LC., 1986. Constructing Recursion Operators in Intuitionistic Type Theory. J. Symb. Comput., v. 2
  • Paulson, LC., 1986. Proving Termination of Normalization Functions for Conditional Expressions Journal of Automated Reasoning, v. 2
    Doi: http://doi.org/10.1007/BF00246023
  • Paulson, LC., 1986. Natural Deduction as Higher-order Resolution Journal of Logic Programming, v. 3
  • Paulson, LC., 1986. Constructing Recursion Operators in Intuitionistic Type Theory. J. Symb. Comput., v. 2
    Doi: 10.1016/S0747-7171(86)80002-5
  • PAULSON, LC., 1986. CONSTRUCTING RECURSION OPERATORS IN INTUITIONISTIC TYPE THEORY J SYMB COMPUT, v. 2
  • Paulson, LC., 1986. Proving Termination of Normalization Functions for Conditional Experessions. J. Autom. Reason., v. 2
  • Paulson, LC., 1985. Lessons learned from LCF: a Survey of Natural Deduction Proofs Computer Journal, v. 28
  • Paulson, LC., 1985. Lessons learned from LCF: a Survey of Natural Deduction Proofs Computer Journal, v. 28
  • Paulson, LC., 1985. Verifying the Unification Algorithm in LCF Science of Computer Programming, v. 5
  • Paulson, LC., 1985. Verifying the Unification Algorithm in LCF Science of Computer Programming, v. 5
  • Paulson, LC., 1983. A Higher-Order Implementation of Rewriting Science of Computer Programming, v. 3
  • Paulson, LC., 1983. A Higher-Order Implementation of Rewriting Science of Computer Programming, v. 3
  • Macfarlane, A., 1896. QUATERNIONS. Science, v. 3
    Doi: http://doi.org/10.1126/science.3.55.99
  • Macfarlane, A., 1896. QUATERNIONS. Science, v. 3
    Doi: http://doi.org/10.1126/science.3.55.99
  • Li, W., Passmore, G. and Paulson, LC., Deciding Univariate Polynomial Problems Using Untrusted Certificates in Isabelle/HOL Journal of Automated Reasoning,
    Doi: http://doi.org/10.1007/s10817-017-9424-6
  • Paulson, LC., Computational Logic: Its Origins and Applications Proceedings of the Royal Society A: Mathematical, Physical and Engineering Sciences,
  • Paulson, LC., A Formalised Theorem in the Partition Calculus
  • Li, W., Passmore, G. and Paulson, LC., Deciding Univariate Polynomial Problems Using Untrusted Certificates in Isabelle/HOL Journal of Automated Reasoning,
    Doi: http://doi.org/10.1007/s10817-017-9424-6
  • Huang, Z., England, M., Wilson, D., Davenport, JH. and Paulson, LC., Using Machine Learning to Improve Cylindrical Algebraic Decomposition Mathematics in Computer Science,
    Doi: http://doi.org/10.1007/s11786-019-00394-8
  • Słowik, A., Mangla, C., Jamnik, M., Holden, SB. and Paulson, LC., Bayesian Optimisation with Gaussian Processes for Premise Selection
  • Bordg, A., Paulson, L. and Li, W., Simple Type Theory is not too Simple: Grothendieck's Schemes without Dependent Types
  • Paulson, LC., Computational Logic: Its Origins and Applications Proceedings of the Royal Society A: Mathematical, Physical and Engineering Sciences,
  • Paulson, LC., Ackermann's Function in Iterative Form: A Proof Assistant Experiment
  • Koutsoukou-Argyraki, A., Li, W. and Paulson, LC., Irrationality and Transcendence Criteria for Infinite Series in Isabelle/HOL Experimental Mathematics,
  • Huang, Z., England, M., Wilson, D., Davenport, JH. and Paulson, LC., A comparison of three heuristics to choose the variable ordering for CAD ACM Communications in Computer Algebra 48:3 (issue 189), pp. 121-123, ACM, 2014,
    Doi: http://doi.org/10.1145/2733693.2733706
  • Džamonja, M., Koutsoukou-Argyraki, A. and Paulson, LC., Formalising Ordinal Partition Relations Using Isabelle/HOL Experimental Mathematics,
  • Paulson, LC., Formalising Mathematics In Simple Type Theory
  • Huang, Z., England, M., Wilson, D., Davenport, JH. and Paulson, LC., A comparison of three heuristics to choose the variable ordering for CAD ACM Communications in Computer Algebra 48:3 (issue 189), pp. 121-123, ACM, 2014,
    Doi: http://doi.org/10.1145/2733693.2733706
  • Huang, Z., England, M., Wilson, D., Davenport, JH. and Paulson, LC., Using Machine Learning to Improve Cylindrical Algebraic Decomposition Mathematics in Computer Science,
    Doi: http://doi.org/10.1007/s11786-019-00394-8
  • Słowik, A., Mangla, C., Jamnik, M., Holden, SB. and Paulson, LC., Bayesian Optimisation with Gaussian Processes for Premise Selection
  • Conference proceedings

  • Edmonds, C. and Paulson, LC., 2021. A Modular First Formalisation of Combinatorial Design Theory. CICM, v. 12833
  • 2020. Automated Reasoning
    Doi: http://doi.org/10.1007/978-3-030-51074-9
  • Slowik, A., Mangla, C., Jamnik, M., Holden, SB. and Paulson, LC., 2020. Bayesian Optimisation for Premise Selection in Automated Theorem Proving (Student Abstract). AAAI,
  • Huang, Z., England, M., Davenport, JH. and Paulson, LC., 2017. Using machine learning to decide when to precondition cylindrical algebraic decomposition with groebner bases Proceedings - 18th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2016,
    Doi: http://doi.org/10.1109/SYNASC.2016.020
  • Paulson, LC., 2017. Porting the HOL Light Analysis Library: Some Lessons (Invited Talk) PROCEEDINGS OF THE 6TH ACM SIGPLAN CONFERENCE ON CERTIFIED PROGRAMS AND PROOFS, CPP'17,
    Doi: http://doi.org/10.1145/3018610.3023366
  • Huang, Z., England, M., Davenport, JH. and Paulson, LC., 2017. Using machine learning to decide when to precondition cylindrical algebraic decomposition with groebner bases Proceedings - 18th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2016,
    Doi: http://doi.org/10.1109/SYNASC.2016.020
  • Paulson, LC., 2017. Porting the HOL Light Analysis Library: Some Lessons (Invited Talk) PROCEEDINGS OF THE 6TH ACM SIGPLAN CONFERENCE ON CERTIFIED PROGRAMS AND PROOFS, CPP'17,
    Doi: http://doi.org/10.1145/3018610.3023366
  • Li, W. and Paulson, LC., 2016. A modular, efficient formalisation of real algebraic numbers CPP 2016 - Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, co-located with POPL 2016,
    Doi: 10.1145/2854065.2854074
  • Huang, Z., England, M., Davenport, JH. and Paulson, LC., 2016. Using Machine Learning to Decide When to Precondition Cylindrical Algebraic Decomposition With Groebner Bases PROCEEDINGS OF 2016 18TH INTERNATIONAL SYMPOSIUM ON SYMBOLIC AND NUMERIC ALGORITHMS FOR SCIENTIFIC COMPUTING (SYNASC),
    Doi: http://doi.org/10.1109/SYNASC.2016.14
  • Huang, Z., England, M., Davenport, JH. and Paulson, LC., 2016. Using Machine Learning to Decide When to Precondition Cylindrical Algebraic Decomposition With Groebner Bases PROCEEDINGS OF 2016 18TH INTERNATIONAL SYMPOSIUM ON SYMBOLIC AND NUMERIC ALGORITHMS FOR SCIENTIFIC COMPUTING (SYNASC),
    Doi: http://doi.org/10.1109/SYNASC.2016.14
  • Li, W. and Paulson, LC., 2016. A modular, efficient formalisation of real algebraic numbers CPP 2016 - Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, co-located with POPL 2016,
    Doi: http://doi.org/10.1145/2854065.2854074
  • Huang, Z., England, M., Wilson, D., Davenport, JH. and Paulson, LC., 2015. A comparison of three heuristics to choose the variable ordering for cylindrical algebraic decomposition ACM Communications in Computer Algebra, v. 48
    Doi: http://doi.org/10.1145/2733693.2733706
  • Sultana, N., Benzmüller, C. and Paulson, LC., 2015. Proofs and reconstructions Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), v. 9322
    Doi: http://doi.org/10.1007/978-3-319-24246-0_16
  • Huang, Z., England, M., Wilson, D., Davenport, JH. and Paulson, LC., 2015. A comparison of three heuristics to choose the variable ordering for cylindrical algebraic decomposition ACM Communications in Computer Algebra, v. 48
    Doi: http://doi.org/10.1145/2733693.2733706
  • Sultana, N., Benzmüller, C. and Paulson, LC., 2015. Proofs and reconstructions Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), v. 9322
    Doi: 10.1007/978-3-319-24246-0_16
  • Paulson, LC., 2015. A formalisation of finite automata using hereditarily finite sets Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), v. 9195
    Doi: 10.1007/978-3-319-21401-6_15
  • Jackson, P., Sogokon, A., Bridge, J. and Paulson, L., 2014. Verifying hybrid systems involving transcendental functions Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), v. 8430 LNCS
    Doi: http://doi.org/10.1007/978-3-319-06200-6_14
  • Jackson, P., Sogokon, A., Bridge, J. and Paulson, L., 2014. Verifying hybrid systems involving transcendental functions Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), v. 8430 LNCS
    Doi: http://doi.org/10.1007/978-3-319-06200-6_14
  • Paulson, LC., 2013. MetiTarski's Menagerie of Cooperating Systems. FroCos, v. 8152
  • Paulson, LC., 2013. MetiTarski's Menagerie of Cooperating Systems. FroCos, v. 8152
  • Paulson, LC., 2012. MetiTarski: Past and Future. ITP, v. 7406
  • Paulson, LC., 2012. MetiTarski: Past and Future. ITP, v. 7406
  • Narayanan, R., Akbarpour, B., Zaki, MH., Tahar, S. and Paulson, LC., 2010. Formal verification of analog circuits in the presence of noise and process variation. DATE,
  • Narayanan, R., Akbarpour, B., Zaki, MH., Tahar, S. and Paulson, LC., 2010. Formal verification of analog circuits in the presence of noise and process variation. DATE,
  • Narayanan, R., Akbarpour, B., Zaki, MH., Tahar, S. and Paulson, LC., 2010. Formal verification of analog circuits in the presence of noise and process variation. DATE,
  • Narayanan, R., Akbarpour, B., Zaki, MH., Tahar, S. and Paulson, LC., 2010. Formal verification of analog circuits in the presence of noise and process variation. DATE,
  • 2010. Interactive Theorem Proving, First International Conference, ITP 2010, Edinburgh, UK, July 11-14, 2010. Proceedings ITP, v. 6172
  • Paulson, LC. and Blanchette, JC., 2010. Three years of experience with Sledgehammer, a Practical Link Between Automatic and Interactive Theorem Provers. IWIL@LPAR, v. 2
  • 2010. Interactive Theorem Proving, First International Conference, ITP 2010, Edinburgh, UK, July 11-14, 2010. Proceedings ITP, v. 6172
  • 2010. Interactive Theorem Proving, First International Conference, ITP 2010, Edinburgh, UK, July 11-14, 2010. Proceedings ITP, v. 6172
  • Paulson, LC. and Blanchette, JC., 2010. Three years of experience with Sledgehammer, a Practical Link Between Automatic and Interactive Theorem Provers. IWIL@LPAR, v. 2
  • Paulson, LC., 2010. Three Years of Experience with Sledgehammer, a Practical Link between Automatic and Interactive Theorem Provers. PAAR@IJCAR, v. 9
  • 2010. Interactive Theorem Proving, First International Conference, ITP 2010, Edinburgh, UK, July 11-14, 2010. Proceedings ITP, v. 6172
  • Paulson, LC., 2010. Three Years of Experience with Sledgehammer, a Practical Link between Automatic and Interactive Theorem Provers. PAAR@IJCAR, v. 9
  • Akbarpour, B. and Paulson, LC., 2009. Applications of MetiTarski in the Verification of Control and Hybrid Systems HYBRID SYSTEMS: COMPUTATION AND CONTROL, v. 5469
  • Akbarpour, B. and Paulson, LC., 2009. Applications of MetiTarski in the Verification of Control and Hybrid Systems Hybrid Systems: Computation and Control,
  • Denman, W., Akbarpour, B., Tahar, S., Zaki, M. and Paulson, LC., 2009. Formal Verification of Analog Designs using MetiTarski Formal Methods in Computer Aided Design,
    Doi: http://doi.org/10.1109/FMCAD.2009.5351136
  • Akbarpour, B. and Paulson, LC., 2009. Applications of MetiTarski in the Verification of Control and Hybrid Systems Hybrid Systems: Computation and Control,
  • Benzmüller, C. and Paulson, LC., 2009. Quantified Multimodal Logics in Simple Type Theory CoRR, v. abs/0905.2435
  • Denman, W., Akbarpour, B., Tahar, S., Zaki, M. and Paulson, LC., 2009. Formal Verification of Analog Designs using MetiTarski Formal Methods in Computer Aided Design,
    Doi: http://doi.org/10.1109/FMCAD.2009.5351136
  • Benzmüller, C. and Paulson, LC., 2009. Quantified Multimodal Logics in Simple Type Theory CoRR, v. abs/0905.2435
  • Benzmüller, C. and Paulson, LC., 2009. Quantified Multimodal Logics in Simple Type Theory CoRR, v. abs/0905.2435
  • Benzmüller, C. and Paulson, LC., 2009. Quantified Multimodal Logics in Simple Type Theory CoRR, v. abs/0905.2435
  • Akbarpour, B. and Paulson, LC., 2009. Applications of MetiTarski in the Verification of Control and Hybrid Systems. HSCC, v. 5469
  • Akbarpour, B. and Paulson, LC., 2009. Applications of MetiTarski in the Verification of Control and Hybrid Systems. HSCC, v. 5469
  • Akbarpour, B. and Paulson, LC., 2009. Applications of MetiTarski in the Verification of Control and Hybrid Systems. HSCC, v. 5469
  • Akbarpour, B. and Paulson, LC., 2009. Applications of MetiTarski in the Verification of Control and Hybrid Systems. HSCC, v. 5469
  • Akbarpour, B. and Paulson, LC., 2009. Applications of MetiTarski in the Verification of Control and Hybrid Systems HYBRID SYSTEMS: COMPUTATION AND CONTROL, v. 5469
  • Paulson, LC., 2008. The relative consistency of the axiom of choice - Mechanized using Isabelle/ZF LOGIC AND THEORY OF ALGORITHMS, v. 5028
  • Wenzel, M., Paulson, LC. and Nipkow, T., 2008. The Isabelle Framework Theorem Proving in Higher Order Logics: TPHOLs 2008,
    Doi: http://doi.org/10.1007/978-3-540-71067-7_7
  • Benzmüller, C., Paulson, LC., Theiss, F. and Fietzke, A., 2008. LEO-II - A Cooperative Automatic Theorem Prover for Higher-Order Logic Automated Reasoning — 4th International Joint Conference, IJCAR 2008,
    Doi: http://doi.org/10.1007/978-3-540-71070-7_14
  • Wenzel, M., Paulson, LC. and Nipkow, T., 2008. The Isabelle Framework Theorem Proving in Higher Order Logics: TPHOLs 2008,
    Doi: http://doi.org/10.1007/978-3-540-71067-7_7
  • Benzmüller, C., Paulson, LC., Theiss, F. and Fietzke, A., 2008. LEO-II - A Cooperative Automatic Theorem Prover for Higher-Order Logic Automated Reasoning — 4th International Joint Conference, IJCAR 2008,
    Doi: http://doi.org/10.1007/978-3-540-71070-7_14
  • Meng, J., Paulson, LC. and Klein, G., 2007. A Termination Checker for Isabelle Hoare Logic 4th International Verification Workshop - VERIFY’07, v. 259
  • Meng, J., Paulson, LC. and Klein, G., 2007. A Termination Checker for Isabelle Hoare Logic 4th International Verification Workshop - VERIFY’07, v. 259
  • Akbarpour, B. and Paulson, L., 2007. Extending a Resolution Prover for Inequalities on Elementary Functions Logic for Programming, Artificial Intelligence, and Reasoning,
    Doi: http://doi.org/10.1007/978-3-540-75560-9_6
  • Akbarpour, B. and Paulson, L., 2007. Extending a Resolution Prover for Inequalities on Elementary Functions Logic for Programming, Artificial Intelligence, and Reasoning,
    Doi: http://doi.org/10.1007/978-3-540-75560-9_6
  • Wenzel, M. and Paulson, LC., 2006. Isabelle/Isar.
  • Wenzel, M. and Paulson, LC., 2006. Isabelle/Isar.
  • Akbarpour, B. and Paulson, LC., 2006. Towards Automatic Proofs of Inequalities Involving Elementary Functions PDPAR: Pragmatics of Decision Procedures in Automated Reasoning,
  • Akbarpour, B. and Paulson, LC., 2006. Towards Automatic Proofs of Inequalities Involving Elementary Functions PDPAR: Pragmatics of Decision Procedures in Automated Reasoning,
  • 2006. FLoC’06 Workshop on Empirically Successful Computerized Reasoning
  • 2006. FLoC’06 Workshop on Empirically Successful Computerized Reasoning
  • Wenzel, M. and Paulson, LC., 2006. Isabelle/Isar.
  • Wenzel, M. and Paulson, LC., 2006. Isabelle/Isar.
  • Nipkow, T. and Paulson, LC., 2005. Proof Pearl: Defining Functions Over Finite Sets Theorem Proving in Higher Order Logics: TPHOLs 2005,
    Doi: http://doi.org/10.1007/11541868_25
  • Nipkow, T. and Paulson, LC., 2005. Proof Pearl: Defining Functions Over Finite Sets Theorem Proving in Higher Order Logics: TPHOLs 2005,
    Doi: http://doi.org/10.1007/11541868_25
  • Bella, G., Longo, C. and Paulson, LC., 2005. Is the verification problem for cryptographic protocols solved? SECURITY PROTOCOLS, v. 3364
  • Nipkow, T. and Paulson, LC., 2005. Proof pearl: Defining functions over finite sets THEOREM PROVING IN HIGHER ORDER LOGICS, PROCEEDINGS, v. 3603
  • Nipkow, T. and Paulson, LC., 2005. Proof pearl: Defining functions over finite sets THEOREM PROVING IN HIGHER ORDER LOGICS, PROCEEDINGS, v. 3603
  • Nipkow, T. and Paulson, LC., 2005. Proof pearl: Defining functions over finite sets THEOREM PROVING IN HIGHER ORDER LOGICS, PROCEEDINGS, v. 3603
  • Bella, G., Longo, C. and Paulson, LC., 2005. Is the verification problem for cryptographic protocols solved? SECURITY PROTOCOLS, v. 3364
  • Bella, G. and Paulson, LC., 2004. Analyzing delegation properties SECURITY PROTOCOLS, v. 2845
  • Bella, G. and Paulson, LC., 2004. Analyzing delegation properties SECURITY PROTOCOLS, v. 2845
  • Bella, G. and Paulson, LC., 2004. Analyzing delegation properties SECURITY PROTOCOLS, v. 2845
  • Meng, J. and Paulson, LC., 2004. Experiments On Supporting Interactive Proof Using Resolution Automated Reasoning — Second International Joint Conference, IJCAR 2004,
    Doi: http://doi.org/10.1007/b98691
  • Meng, J. and Paulson, LC., 2004. Experiments On Supporting Interactive Proof Using Resolution Automated Reasoning — Second International Joint Conference, IJCAR 2004,
    Doi: http://doi.org/10.1007/b98691
  • Meng, J. and Paulson, LC., 2004. Experiments on supporting interactive proof using resolution AUTOMATED REASONING, PROCEEDINGS, v. 3097
  • Paulson, LC., 2004. The descent of BAN COMPUTER SYSTEMS: THEORY, TECHNOLOGY AND APPLICATIONS,
  • Meng, J. and Paulson, LC., 2004. Experiments On Supporting Interactive Proof Using Resolution Automated Reasoning — Second International Joint Conference, IJCAR 2004,
    Doi: http://doi.org/10.1007/b98691
  • Meng, J. and Paulson, LC., 2004. Experiments On Supporting Interactive Proof Using Resolution Automated Reasoning — Second International Joint Conference, IJCAR 2004,
    Doi: http://doi.org/10.1007/b98691
  • Bella, G., Longo, C. and Paulson, LC., 2003. Verifying Second-Level Security Protocols Theorem Proving in Higher Order Logics: TPHOLs 2003,
  • Bella, G., Longo, C. and Paulson, LC., 2003. Verifying Second-Level Security Protocols Theorem Proving in Higher Order Logics: TPHOLs 2003,
  • Paulson, LC., 2003. Verifying the SET protocol: Overview FORMAL ASPECTS OF SECURITY, v. 2629
  • Bella, G., Longo, C. and Paulson, LC., 2003. Verifying Second-Level Security Protocols Theorem Proving in Higher Order Logics: TPHOLs 2003,
  • Paulson, LC., 2003. Verifying the SET protocol: Overview FORMAL ASPECTS OF SECURITY, v. 2629
  • Bella, G., Paulson, LC. and Massacci, F., 2002. The verification of an industrial payment protocol: the SET purchase phase. CCS,
  • Bella, G., Paulson, LC. and Massacci, F., 2002. The verification of an industrial payment protocol: the SET purchase phase. CCS,
  • Bella, G. and Paulson, LC., 2002. A proof of non-repudiation SECURITY PROTOCOLS, v. 2467
  • Ehmety, SO. and Paulson, LC., 2002. Program Composition in Isabelle/UNITY Workshop on Formal Methods for Parallel Programming: Theory and Applications; text on CD-ROM,
  • Paulson, LC., 2002. The Reflection Theorem: A Study in Meta-theoretic Reasoning. CADE, v. 2392
  • Ehmety, SO. and Paulson, LC., 2002. Program Composition in Isabelle/UNITY Workshop on Formal Methods for Parallel Programming: Theory and Applications; text on CD-ROM,
  • Ehmety, SO. and Paulson, LC., 2002. Program Composition in Isabelle/UNITY Workshop on Formal Methods for Parallel Programming: Theory and Applications; text on CD-ROM,
  • Paulson, L., 2002. A proof of non-repudiation - (Transcript of discussion) SECURITY PROTOCOLS, v. 2467
  • Bella, G., Paulson, LC. and Massacci, F., 2002. The verification of an industrial payment protocol: the SET purchase phase. CCS,
  • Christianson, B., Aura, T., Wheeler, D., Harbison, W., Gligor, V., Paulson, L., Blaze, M. and Ioannidis, J., 2002. Concluding discussion - When does confidentiality harm security? SECURITY PROTOCOLS, v. 2467
  • Paulson, LC., 2002. The Reflection Theorem: A Study in Meta-theoretic Reasoning. CADE, v. 2392
  • Bella, G. and Paulson, LC., 2002. A proof of non-repudiation SECURITY PROTOCOLS, v. 2467
  • Ehmety, SO. and Paulson, LC., 2002. Program Composition in Isabelle/UNITY Workshop on Formal Methods for Parallel Programming: Theory and Applications; text on CD-ROM,
  • Paulson, L., 2002. A proof of non-repudiation - (Transcript of discussion) SECURITY PROTOCOLS, v. 2467
  • Bella, G. and Paulson, LC., 2001. Mechanical Proofs about a Non-repudiation Protocol. TPHOLs, v. 2152
  • Paulson, LC., 2001. SET Cardholder Registration: The Secrecy Proofs. IJCAR, v. 2083
  • Bella, G. and Paulson, LC., 2001. Mechanical Proofs about a Non-repudiation Protocol. TPHOLs, v. 2152
  • Bella, G., Massacci, F., Paulson, LC. and Tramontano, P., 2001. Making sense of specifications: The formalization of SET (Extended abstract) Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), v. 2133
    Doi: http://doi.org/10.1007/3-540-44810-1_11
  • Bella, G., Massacci, F., Paulson, LC. and Tramontano, P., 2001. Making sense of specifications: The formalization of SET (Extended abstract) Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), v. 2133
    Doi: http://doi.org/10.1007/3-540-44810-1_11
  • Paulson, LC., 2001. SET Cardholder Registration: The Secrecy Proofs. IJCAR, v. 2083
  • Paulson, LC., 2001. SET Cardholder Registration: The Secrecy Proofs. IJCAR, v. 2083
  • Paulson, LC., 2001. SET Cardholder Registration: The Secrecy Proofs. IJCAR, v. 2083
  • Paulson, LC., 2000. Relations between secrets: The Yahalom protocol SECURITY PROTOCOLS, v. 1796
  • Bella, G., Massacci, F., Paulson, LC. and Tramontano, P., 2000. Formal verification of Cardholder Registration in SET COMPUTER SECURITY - ESORICS 2000, PROCEEDINGS, v. 1895
  • Paulson, LC., 2000. The Yahalom protocol SECURITY PROTOCOLS, v. 1796
  • Bella, G., Massacci, F., Paulson, LC. and Tramontano, P., 2000. Making Sense of Specifications: The Formalization of SET. Security Protocols Workshop, v. 2133
  • Paulson, LC., 2000. Making Sense of Specifications: The Formalization of SET (Transcript of Discussion). Security Protocols Workshop, v. 2133
  • Paulson, LC., 2000. Making Sense of Specifications: The Formalization of SET (Transcript of Discussion). Security Protocols Workshop, v. 2133
  • Paulson, LC., 2000. Making Sense of Specifications: The Formalization of SET (Transcript of Discussion). Security Protocols Workshop, v. 2133
  • Bella, G., Massacci, F., Paulson, LC. and Tramontano, P., 2000. Formal verification of Cardholder Registration in SET COMPUTER SECURITY - ESORICS 2000, PROCEEDINGS, v. 1895
  • Bella, G., Massacci, F., Paulson, LC. and Tramontano, P., 2000. Formal Verification of Cardholder Registration in SET Computer Security — ESORICS 2000,
  • Paulson, LC., 2000. Relations between secrets: The yahalom protocol extended abstract Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), v. 1796
    Doi: http://doi.org/10.1007/10720107_10
  • Paulson, LC., 2000. Relations between secrets: The yahalom protocol extended abstract Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), v. 1796
    Doi: http://doi.org/10.1007/10720107_10
  • Bella, G., Massacci, F., Paulson, LC. and Tramontano, P., 2000. Formal Verification of Cardholder Registration in SET Computer Security — ESORICS 2000,
  • Bella, G., Massacci, F., Paulson, LC. and Tramontano, P., 2000. Formal Verification of Cardholder Registration in SET Computer Security — ESORICS 2000,
  • Paulson, LC., 2000. The Yahalom protocol SECURITY PROTOCOLS, v. 1796
  • Bella, G., Massacci, F., Paulson, LC. and Tramontano, P., 2000. Formal Verification of Cardholder Registration in SET Computer Security — ESORICS 2000,
  • Bella, G., Massacci, F., Paulson, LC. and Tramontano, P., 2000. Making Sense of Specifications: The Formalization of SET. Security Protocols Workshop, v. 2133
  • Paulson, LC., 2000. Making Sense of Specifications: The Formalization of SET (Transcript of Discussion). Security Protocols Workshop, v. 2133
  • Paulson, LC., 1999. Proving Security Protocols Correct. LICS,
    Doi: http://doi.org/10.1109/LICS.1999.782632
  • Kammüller, F., Wenzel, M. and Paulson, LC., 1999. Locales: A Sectioning Concept for Isabelle Theorem Proving in Higher Order Logics: TPHOLs ’99,
  • Kammüller, F., Wenzel, M. and Paulson, LC., 1999. Locales: A Sectioning Concept for Isabelle Theorem Proving in Higher Order Logics: TPHOLs ’99,
  • Fleuriot, J. and Paulson, LC., 1999. Proving Newton’s Propositio Kepleriana Using Geometry and Nonstandard Analysis in Isabelle Workshop on Automated Deduction in Geometry, Second International Workshop, ADG’98,
  • Kammüller, F., Wenzel, M. and Paulson, LC., 1999. Locales: A Sectioning Concept for Isabelle Theorem Proving in Higher Order Logics: TPHOLs ’99,
  • Fleuriot, J. and Paulson, LC., 1999. Proving Newton’s Propositio Kepleriana Using Geometry and Nonstandard Analysis in Isabelle Workshop on Automated Deduction in Geometry, Second International Workshop, ADG’98,
  • Paulson, LC., 1999. Proving Security Protocols Correct. LICS,
    Doi: http://doi.org/10.1109/LICS.1999.782632
  • Paulson, LC., 1999. Proving Security Protocols Correct. LICS,
    Doi: http://doi.org/10.1109/LICS.1999.782632
  • Paulson, LC., 1999. Proving Security Protocols Correct. LICS,
    Doi: http://doi.org/10.1109/LICS.1999.782632
  • Kammüller, F., Wenzel, M. and Paulson, LC., 1999. Locales: A Sectioning Concept for Isabelle Theorem Proving in Higher Order Logics: TPHOLs ’99,
  • Paulson, LC., 1998. A Generic Tableau Prover and its Integration with Isabelle (Extended Abstract) CADE-15 Workshop on Integration of Deduction Systems,
  • Paulson, LC., 1998. Inductive Analysis of the Internet Protocol TLS (Transcript of Discussion). Security Protocols Workshop, v. 1550
  • Bella, G. and Paulson, LC., 1998. Kerberos Version IV: Inductive Analysis of the Secrecy Goals Computer Security — ESORICS 98,
  • Ballarin, C. and Paulson, LC., 1998. Reasoning about coding theory: The benefits we get from computer algebra Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), v. 1476
  • Bella, G. and Paulson, LC., 1998. Mechanising BAN Kerberos by the Inductive Method Computer Aided Verification: 10th International Conference, CAV ’98,
  • Ballarin, C. and Paulson, LC., 1998. Reasoning About Coding Theory: The Benefits We Get from Computer Algebra. AISC, v. 1476
  • Paulson, LC., 1998. A Generic Tableau Prover and its Integration with Isabelle (Extended Abstract) CADE-15 Workshop on Integration of Deduction Systems,
  • Fleuriot, J. and Paulson, LC., 1998. A Combination of Nonstandard Analysis and Geometry Theorem Proving, with Application to Newton’s Principia Automated Deduction — CADE-15 International Conference,
  • Bella, G. and Paulson, LC., 1998. Kerberos Version IV: Inductive Analysis of the Secrecy Goals Computer Security — ESORICS 98,
  • Ballarin, C. and Paulson, LC., 1998. Reasoning About Coding Theory: The Benefits We Get from Computer Algebra. AISC, v. 1476
  • Ballarin, C. and Paulson, LC., 1998. Reasoning About Coding Theory: The Benefits We Get from Computer Algebra. AISC, v. 1476
  • Paulson, L., 1998. Inductive analysis of the internet protocol TLS Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), v. 1550
    Doi: http://doi.org/10.1007/3-540-49135-X_2
  • Bella, G. and Paulson, LC., 1998. Kerberos Version IV: Inductive Analysis of the Secrecy Goals Computer Security — ESORICS 98,
  • Ballarin, C. and Paulson, LC., 1998. Reasoning About Coding Theory: The Benefits We Get from Computer Algebra. AISC, v. 1476
  • Bella, G. and Paulson, LC., 1998. Kerberos Version IV: Inductive Analysis of the Secrecy Goals Computer Security — ESORICS 98,
  • Bella, G. and Paulson, LC., 1998. Mechanising BAN Kerberos by the Inductive Method Computer Aided Verification: 10th International Conference, CAV ’98,
  • Paulson, LC., 1998. Inductive Analysis of the Internet Protocol TLS (Position Paper). Security Protocols Workshop, v. 1550
  • Bella, G. and Paulson, LC., 1998. Mechanising BAN Kerberos by the Inductive Method Computer Aided Verification: 10th International Conference, CAV ’98,
  • Paulson, LC., 1998. Inductive Analysis of the Internet Protocol TLS (Position Paper). Security Protocols Workshop, v. 1550
  • Fleuriot, J. and Paulson, LC., 1998. A Combination of Nonstandard Analysis and Geometry Theorem Proving, with Application to Newton’s Principia Automated Deduction — CADE-15 International Conference,
  • Paulson, LC., 1998. Inductive Analysis of the Internet Protocol TLS (Position Paper). Security Protocols Workshop, v. 1550
  • Fleuriot, J. and Paulson, LC., 1998. A Combination of Nonstandard Analysis and Geometry Theorem Proving, with Application to Newton’s Principia Automated Deduction — CADE-15 International Conference,
  • Paulson, LC., 1998. Inductive Analysis of the Internet Protocol TLS (Transcript of Discussion). Security Protocols Workshop, v. 1550
  • Fleuriot, J. and Paulson, LC., 1998. A Combination of Nonstandard Analysis and Geometry Theorem Proving, with Application to Newton’s Principia Automated Deduction — CADE-15 International Conference,
  • Paulson, LC., 1998. Inductive Analysis of the Internet Protocol TLS (Transcript of Discussion). Security Protocols Workshop, v. 1550
  • Paulson, LC., 1998. Inductive Analysis of the Internet Protocol TLS (Transcript of Discussion). Security Protocols Workshop, v. 1550
  • Paulson, L., 1998. Inductive analysis of the internet protocol TLS Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), v. 1550
    Doi: http://doi.org/10.1007/3-540-49135-X_2
  • Ballarin, C. and Paulson, LC., 1998. Reasoning about coding theory: The benefits we get from computer algebra Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), v. 1476
  • Paulson, LC., 1998. Inductive Analysis of the Internet Protocol TLS (Position Paper). Security Protocols Workshop, v. 1550
  • Bella, G. and Paulson, LC., 1997. Using Isabelle to Prove Properties of the Kerberos Authentication System Workshop on Design and Formal Verification of Security Protocols,
  • Bella, G. and Paulson, LC., 1997. Using Isabelle to Prove Properties of the Kerberos Authentication System Workshop on Design and Formal Verification of Security Protocols,
  • Bella, G. and Paulson, LC., 1997. Using Isabelle to Prove Properties of the Kerberos Authentication System Workshop on Design and Formal Verification of Security Protocols,
  • Paulson, LC., 1997. Mechanizing Coinduction and Corecursion in Higher-Order Logic. J. Log. Comput., v. 7
  • Paulson, LC., 1997. Proving Properties of Security Protocols by Induction 10th Computer Security Foundations Workshop,
  • Paulson, LC., 1997. Mechanizing Coinduction and Corecursion in Higher-Order Logic. J. Log. Comput., v. 7
  • Paulson, LC., 1997. Proving Properties of Security Protocols by Induction 10th Computer Security Foundations Workshop,
  • Paulson, LC., 1997. Proving Properties of Security Protocols by Induction 10th Computer Security Foundations Workshop,
  • Paulson, LC., 1997. Mechanizing Coinduction and Corecursion in Higher-Order Logic. J. Log. Comput., v. 7
    Doi: 10.1093/logcom/7.2.175
  • Paulson, LC., 1997. Mechanized Proofs for a Recursive Authentication Protocol 10th Computer Security Foundations Workshop,
  • Paulson, LC., 1997. Mechanized Proofs for a Recursive Authentication Protocol 10th Computer Security Foundations Workshop,
  • Paulson, LC., 1997. Proving Properties of Security Protocols by Induction 10th Computer Security Foundations Workshop,
  • Paulson, LC., 1997. Mechanized Proofs for a Recursive Authentication Protocol 10th Computer Security Foundations Workshop,
  • Paulson, LC., 1997. Mechanized Proofs for a Recursive Authentication Protocol 10th Computer Security Foundations Workshop,
  • Bella, G. and Paulson, LC., 1997. Using Isabelle to Prove Properties of the Kerberos Authentication System Workshop on Design and Formal Verification of Security Protocols,
  • 1995. First Isabelle Users Workshop
  • 1995. First Isabelle Users Workshop
  • 1995. First Isabelle Users Workshop
  • Paulson, LC., 1994. A Concrete Final Coalgebra Theorem for ZF Set Theory. TYPES, v. 996
  • Paulson, LC., 1994. A Fixedpoint Approach to Implementing (Co)Inductive Definitions Automated Deduction — CADE-12,
  • Paulson, LC., 1994. A Concrete Final Coalgebra Theorem for ZF Set Theory. TYPES, v. 996
  • Paulson, LC., 1994. A Fixedpoint Approach to Implementing (Co)Inductive Definitions Automated Deduction — CADE-12,
  • Paulson, LC., 1993. A Formulation of the Simple Theory of Types (for Isabelle) CoRR, v. cs.LO/9301107
  • Paulson, LC., 1993. A Formulation of the Simple Theory of Types (for Isabelle) CoRR, v. cs.LO/9301107
  • Paulson, LC., 1993. A Formulation of the Simple Theory of Types (for Isabelle) CoRR, v. cs.LO/9301107
  • Paulson, LC., 1993. A Formulation of the Simple Theory of Types (for Isabelle) CoRR, v. cs.LO/9301107
  • NIPKOW, T. and PAULSON, LC., 1992. ISABELLE-91 AUTOMATED DEDUCTION - CADE-11, v. 607
  • Nipkow, T. and Paulson, LC., 1992. Isabelle-91 (system abstract) Automated Deduction — CADE-11,
  • Nipkow, T. and Paulson, LC., 1992. Isabelle-91 (system abstract) Automated Deduction — CADE-11,
  • Paulson, LC. and Smith, AW., 1991. Logic Programming, Functional Programming, and Inductive Definitions Extensions of Logic Programming,
  • Paulson, LC. and Smith, AW., 1991. Logic Programming, Functional Programming, and Inductive Definitions Extensions of Logic Programming,
  • Paulson, LC., 1990. A Formulation of the Simple Theory of Types (for Isabelle) COLOG-88: International Conference on Computer Logic,
  • Paulson, LC., 1990. A Formulation of the Simple Theory of Types (for Isabelle) COLOG-88: International Conference on Computer Logic,
  • Paulson, LC., 1990. A Formulation of the Simple Theory of Types (for Isabelle) COLOG-88: International Conference on Computer Logic,
  • Paulson, LC. and Smith, AW., 1989. Logic Programming, Functional Programming, and Inductive Definitions. ELP, v. 475
  • Paulson, LC. and Smith, AW., 1989. Logic Programming, Functional Programming, and Inductive Definitions. ELP, v. 475
  • Paulson, LC. and Smith, AW., 1989. Logic Programming, Functional Programming, and Inductive Definitions. ELP, v. 475
  • Paulson, LC., 1988. Isabelle: The Next Seven Hundred Theorem Provers. CADE, v. 310
  • Paulson, LC., 1988. Isabelle: The Next Seven Hundred Theorem Provers. CADE, v. 310
  • Paulson, LC., 1988. Isabelle: The Next Seven Hundred Theorem Provers. CADE, v. 310
  • Paulson, LC., 1988. Isabelle: The Next Seven Hundred Theorem Provers. CADE, v. 310
  • Paulson, LC., 1987. NEXT SEVEN HUNDRED THEOREM PROVERS. IEE Colloquium (Digest),
  • Paulson, LC., 1987. NEXT SEVEN HUNDRED THEOREM PROVERS. IEE Colloquium (Digest),
  • Paulson, LC., 1986. Natural Deduction as Higher-Order Resolution. J. Log. Program., v. 3
  • Paulson, LC., 1986. Natural Deduction as Higher-Order Resolution. J. Log. Program., v. 3
  • Paulson, LC., 1986. Natural Deduction as Higher-Order Resolution. J. Log. Program., v. 3
    Doi: 10.1016/0743-1066(86)90015-4
  • Paulson, LC., 1985. Verifying the Unification Algorithm in LCF. Sci. Comput. Program., v. 5
  • Paulson, LC., 1985. Verifying the Unification Algorithm in LCF. Sci. Comput. Program., v. 5
    Doi: 10.1016/0167-6423(85)90009-7
  • Paulson, LC., 1984. Deriving Structural Induction in LCF. Semantics of Data Types, v. 173
  • Paulson, LC., 1984. Deriving Structural Induction in LCF. Semantics of Data Types, v. 173
  • Paulson, LC., 1983. Compiler Generation from Denotational Semantics. Method and tools for compiler construction,
  • Paulson, LC., 1983. Compiler Generation from Denotational Semantics. Method and tools for compiler construction,
  • Paulson, LC., 1983. Compiler Generation from Denotational Semantics. Method and tools for compiler construction,
  • Paulson, LC., 1983. A Higher-Order Implementation of Rewriting. Sci. Comput. Program., v. 3
  • Paulson, LC., 1983. A Higher-Order Implementation of Rewriting. Sci. Comput. Program., v. 3
  • Paulson, LC., 1983. A Higher-Order Implementation of Rewriting. Sci. Comput. Program., v. 3
    Doi: 10.1016/0167-6423(83)90008-4
  • Paulson, LC., 1982. A Semantics-Directed Compiler Generator. POPL,
  • Paulson, LC., 1982. A Semantics-Directed Compiler Generator. POPL,
  • Paulson, L., 1982. A Semantics-Directed Compiler Generator Ninth Annual ACM Symposium on Principles of Programming Languages,
  • Paulson, LC., 1982. A Semantics-Directed Compiler Generator. POPL,
  • Paulson, L., 1982. A Semantics-Directed Compiler Generator Ninth Annual ACM Symposium on Principles of Programming Languages,
  • Paulson, LC., 1982. A Semantics-Directed Compiler Generator. POPL,
  • Słowik, A., Mangla, C., Jamnik, M., Holden, S. and Paulson, L., Bayesian Optimisation for Heuristic Configuration in Automated Theorem Proving
    Doi: 10.29007/q91g
  • Li, W., Yu, L., Wu, Y. and Paulson, L., International Conference on Learning Representations
  • Li, W. and Paulson, L., Counting Polynomial Roots]{Counting Polynomial Roots in Isabelle/HOL: A Formal Proof of the Budan-Fourier Theorem
    Doi: http://doi.org/10.1145/3293880.3294092
  • Li, W. and Paulson, LC., 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,
    Doi: http://doi.org/10.1145/3293880.3294092
  • Paulson, LC. and Susanto, KW., Source-Level Proof Reconstruction for Interactive Theorem Proving
  • Slowik, A., Mangla, C., Jamnik, M., Holden, S. and Paulson, L., Bayesian Optimisation for Premise Selection in Automated Theorem Proving (Student Abstract) Proceedings of the AAAI Conference on Artificial Intelligence,
  • Paulson, LC. and Susanto, KW., Source-Level Proof Reconstruction for Interactive Theorem Proving
  • de Vilhena, PE. and Paulson, L., Algebraically Closed Fields in Isabelle/HOL Automated Reasoning—10th International Joint Conference, IJCAR 2020,
    Doi: http://doi.org/10.1007/978-3-030-51054-1_12
  • Meng, J. and Paulson, LC., Translating Higher-Order Problems to First-Order Clauses
  • Meng, J. and Paulson, LC., Lightweight Relevance Filtering for Machine-Generated Resolution Problems
  • Meng, J. and Paulson, LC., Translating Higher-Order Problems to First-Order Clauses
  • Mangla, C., Paulson, L. and Holden, S., Bayesian Optimisation of Solver Parameters in CBMC
  • Meng, J. and Paulson, LC., Lightweight Relevance Filtering for Machine-Generated Resolution Problems
  • Li, W. and Paulson, LC., 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,
    Doi: http://doi.org/10.1145/3293880.3294092
  • Edmonds, C. and Paulson, L., A Modular First Formalisation of Combinatorial Design Theory Intelligent Computer Mathematics 14th International Conference, CICM 2021,
  • Slowik, A., Mangla, C., Jamnik, M., Holden, S. and Paulson, L., Bayesian Optimisation for Premise Selection in Automated Theorem Proving (Student Abstract) Proceedings of the AAAI Conference on Artificial Intelligence,
  • Book chapters

  • Passmore, G., Paulson, L. and de Moura, L., 2012. Real Algebraic Strategies for MetiTarski Proofs
    Doi: http://doi.org/10.1007/978-3-642-31374-5_24
  • Paulson, LC., 2010. Functional Programming in ML.
  • Paulson, LC., 2010. Functional Programming in ML.
  • Wenzel, M., Paulson, LC. and Nipkow, T., 2008. The Isabelle Framework
    Doi: http://doi.org/10.1007/978-3-540-71067-7_7
  • Wenzel, M., Paulson, LC. and Nipkow, T., 2008. The Isabelle Framework
    Doi: http://doi.org/10.1007/978-3-540-71067-7_7
  • Paulson, LC., 2001. Making Sense of Specifications: The Formalization of SET
    Doi: http://doi.org/10.1007/3-540-44810-1_12
  • Paulson, LC., 2000. A fixedpoint approach to (co)inductive and (co)datatype definitions.
  • Paulson, LC., 2000. A fixedpoint approach to (co)inductive and (co)datatype definitions.
  • Paulson, LC., 2000. A fixedpoint approach to (co)inductive and (co)datatype definitions.
  • Paulson, LC., 2000. A fixedpoint approach to (co)inductive and (co)datatype definitions.
  • Paulson, LC., 1997. Tool Support for Logics of Programs
  • Paulson, LC., 1997. Generic Automatic Proof Tools
  • Paulson, LC., 1997. Generic Automatic Proof Tools
  • Paulson, LC., 1997. Generic Automatic Proof Tools
  • Paulson, LC., 1997. Tool Support for Logics of Programs
  • Paulson, LC., 1992. Designing a Theorem Prover
  • Paulson, LC., 1992. Designing a Theorem Prover
  • Paulson, LC., 1990. Isabelle: The Next 700 Theorem Provers
  • Abdulaziz, M. and Paulson, LC., An Isabelle/HOL Formalisation of Green’s Theorem
    Doi: http://doi.org/10.1007/978-3-319-43144-4_1
  • Abdulaziz, M. and Paulson, LC., An Isabelle/HOL Formalisation of Green’s Theorem
    Doi: http://doi.org/10.1007/978-3-319-43144-4_1
  • Books

  • 2010. Interactive Theorem Proving
    Doi: http://doi.org/10.1007/978-3-642-14052-5
  • 2010. Interactive Theorem Proving
    Doi: http://doi.org/10.1007/978-3-642-14052-5
  • Kaufmann, M. and Paulson, L., 2010. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics): Preface
  • Kaufmann, M. and Paulson, L., 2010. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics): Preface
  • Paulson, LC., 1996. ML for the Working Programmer
  • Paulson, LC., 1996. ML for the Working Programmer
  • Paulson, LC., 1994. Isabelle: A Generic Theorem Prover
  • Paulson, LC., 1994. Isabelle: A Generic Theorem Prover
  • Paulson, LC., 1994. Isabelle: A Generic Theorem Prover
  • Paulson, LC., 1991. ML for the Working Programmer
  • Paulson, LC., 1991. ML for the Working Programmer
  • Paulson, LC., 1987. Logic and Computation: Interactive proof with Cambridge LCF
  • Paulson, LC., 1987. Logic and Computation: Interactive proof with Cambridge LCF
  • Reports

  • Paulson, LC., 1997. Mechanized Proofs of Security Protocols: Needham-Schroeder with Public Keys
  • Paulson, LC., 1997. Mechanized Proofs of Security Protocols: Needham-Schroeder with Public Keys
  • Paulson, LC., 1997. Mechanized Proofs of Security Protocols: Needham-Schroeder with Public Keys
  • Paulson, LC., 1997. Mechanized Proofs of Security Protocols: Needham-Schroeder with Public Keys
  • Paulson, LC., 1996. A Simple Formalization and Proof for the Mutilated Chess Board
  • Paulson, LC., 1996. A Simple Formalization and Proof for the Mutilated Chess Board
  • Paulson, LC., 1996. A Simple Formalization and Proof for the Mutilated Chess Board
  • Paulson, LC., 1996. A Simple Formalization and Proof for the Mutilated Chess Board
  • Paulson, LC., 1993. Introduction to Isabelle
  • Paulson, LC., 1993. Introduction to Isabelle
  • Paulson, LC., 1993. The Isabelle Reference Manual
  • Paulson, LC., 1993. The Isabelle Reference Manual
  • Paulson, LC., 1993. The Isabelle Reference Manual
  • Paulson, LC., 1993. Isabelle’s Object-Logics
  • Paulson, LC., 1993. Isabelle’s Object-Logics
  • Paulson, LC., 1993. A Fixedpoint Approach to Implementing (Co)Inductive Definitions
  • Paulson, LC., 1993. Isabelle’s Object-Logics
  • Paulson, LC., 1993. A Fixedpoint Approach to Implementing (Co)Inductive Definitions
  • Paulson, LC., 1993. A Fixedpoint Approach to Implementing (Co)Inductive Definitions
  • Paulson, LC., 1992. Set Theory as a Computational Logic: I. From Foundations to Functions
  • Paulson, LC., 1992. Set Theory as a Computational Logic: I. From Foundations to Functions
  • Paulson, LC. and Nipkow, T., 1990. Isabelle Tutorial and User’s Manual
  • Paulson, LC. and Nipkow, T., 1990. Isabelle Tutorial and User’s Manual
  • Paulson, LC., 1988. A preliminary user’s manual for Isabelle
  • Paulson, LC., 1988. A preliminary user’s manual for Isabelle
  • Theses / dissertations

  • Paulson, LC., 1981. A Compiler Generator for Semantic Grammars
  • Paulson, LC., 1981. A Compiler Generator for Semantic Grammars
  • Internet publications

  • Paulson, LC., Home Page
  • Paulson, LC., Home Page
  • Paulson, LC., Home Page
  • Paulson, LC., Home Page
  • Contact Details

    Room: 
    FE18
    Office phone: 
    (01223) 3-34623
    Email: 

    lp15@cam.ac.uk