Book chapters
Paulson, LC., 2023. Large-Scale Formal Proof for the Working Mathematician—Lessons Learnt from the ALEXANDRIA Project
Doi: 10.1007/978-3-031-42753-4_1
Mangla, C., Holden, SB. and Paulson, LC., 2022. Bayesian Ranking for Strategy Scheduling in Automated Theorem Provers
Doi: 10.1007/978-3-031-10769-6_33
Paulson, LC., 2022. Wetzel: Formalisation of an Undecidable Problem Linked to the Continuum Hypothesis
Doi: 10.1007/978-3-031-16681-5_6
Paulson, LC., 2010. Functional Programming in ML.
Paulson, LC., 2010. Functional Programming in ML.
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. Generic Automatic Proof Tools
Paulson, LC., 1997. Tool Support for Logics of Programs
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., 1992. Designing a Theorem Prover
Paulson, LC., 1992. Designing a Theorem Prover
Paulson, LC., 1990. Isabelle: The Next 700 Theorem Provers
Journal articles
Bayer, J., Benzmüller, C., Buzzard, K., David, M., Lamport, L., Matiyasevich, Y., Paulson, L., Schleicher, D., Stock, B. and Zelmanov, E., 2022. Mathematical Proof Between Generations
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
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., 2020. Ordinal Partitions. Arch. Formal Proofs, v. 2020
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. Zermelo Fraenkel Set Theory in Higher-Order Logic. 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
Paulson, LC., 2019. Fourier Series. Arch. Formal Proofs, v. 2019
Słowik, A., Mangla, C., Jamnik, M., Holden, SB. and Paulson, LC., 2019. Bayesian Optimisation with Gaussian Processes for Premise Selection
Paulson, LC., 2019. Zermelo Fraenkel Set Theory in Higher-Order Logic. Arch. Formal Proofs, v. 2019
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
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
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: 10.1007/s10817-017-9424-6
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
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. 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
Eberl, M. and Paulson, LC., 2018. The Prime Number Theorem. Arch. Formal Proofs, v. 2018
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
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
Hibon, Q. and Paulson, LC., 2016. Source Coding Theorem. Arch. Formal Proofs, v. 2016
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
Paulson, LC., 2016. The Cartan Fixed Point Theorems. Arch. Formal Proofs, v. 2016
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., 2015. Finite Automata in Hereditarily Finite Set Theory. Arch. Formal Proofs, v. 2015
Paulson, LC., 2015. Abolish Software Warranty Disclaimers COMMUNICATIONS OF THE ACM, v. 58
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
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., 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. Provenance of British Computing COMMUNICATIONS OF THE ACM, v. 57
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
Huang, Z., England, M., Wilson, D., Davenport, JH. and Paulson, LC., 2014. 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,
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
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
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
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
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
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
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
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
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
Sultana, N., Blanchette, JC. and Paulson, LC., 2013. LEO-II and Satallax on the Sledgehammer test bench Journal of Applied Logic, v. 11
Doi: 10.1016/j.jal.2012.12.002
Paulson, LC., 2013. What we want from computer science Communications of the ACM, v. 56
Doi: 10.1145/2483852.2483856
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
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., 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
Romanos, R. and Paulson, LC., 2012. Proving the Impossibility of Trisecting an Angle and Doubling the Cube. Arch. Formal Proofs, v. 2012
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
Paulson, LC., 2009. Refocus Fragmented CS Conference Culture COMMUNICATIONS OF THE ACM, v. 52
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,
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
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
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
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
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
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
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. 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. 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. 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
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
Paulson, LC., 2000. Mechanizing UNITY in Isabelle. ACM Trans. Comput. Log., v. 1
Fleuriot, JD. and Paulson, LC., 2000. Mechanizing Nonstandard Real Analysis LMS Journal of Computation and Mathematics, v. 3
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
Paulson, LC., 2000. Mechanizing UNITY in Isabelle. ACM Trans. Comput. Log., v. 1
Doi: 10.1145/343369.343370
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
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. Final coalgebras as greatest fixed points in ZF set theory. Math. Struct. Comput. Sci., v. 9
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
Paulson, LC., 1999. Final coalgebras as greatest fixed points in ZF set theory. Math. Struct. Comput. Sci., v. 9
Lamport, L. and Paulson, LC., 1999. Should Your Specification Language Be Typed? ACM Transactions on Programming Languages and Systems, v. 21
Ballarin, C. and Paulson, LC., 1999. A Pragmatic Approach to Extending Provers by Computer Algebra - with Applications to Coding Theory. Fundam. Informaticae, v. 39
Lamport, L. and Paulson, LC., 1999. Should Your Specification Language Be Typed? ACM Transactions on Programming Languages and Systems, v. 21
Ballarin, C. and Paulson, LC., 1999. A Pragmatic Approach to Extending Provers by Computer Algebra - with Applications to Coding Theory. Fundam. Informaticae, v. 39
Lamport, L. and Paulson, LC., 1999. Should Your Specification Language Be Typed? ACM Transactions on Programming Languages and Systems, v. 21
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. 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
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
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. 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
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
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, 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. 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. 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., 1995. Set Theory for Verification: II. Induction and Recursion Journal of Automated Reasoning, v. 15
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. 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., 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
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
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, 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, 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, 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 Journal of Automated Reasoning, 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., 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. Natural Deduction as Higher-order Resolution Journal of Logic Programming, v. 3
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. Proving Termination of Normalization Functions for Conditional Expressions Journal of Automated Reasoning, v. 2
Doi: http://doi.org/10.1007/BF00246023
Paulson, LC., 1986. Proving Termination of Normalization Functions for Conditional Experessions. J. Autom. Reason., v. 2
PAULSON, LC., 1986. CONSTRUCTING RECURSION OPERATORS IN INTUITIONISTIC TYPE THEORY J SYMB COMPUT, v. 2
Paulson, LC., 1986. Constructing Recursion Operators in Intuitionistic Type Theory. J. Symb. Comput., v. 2
Paulson, LC., 1986. Constructing Recursion Operators in Intuitionistic Type Theory. J. Symb. Comput., v. 2
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., 1985. Lessons learned from LCF: a Survey of Natural Deduction Proofs Computer Journal, v. 28
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
Słowik, A., Mangla, C., Jamnik, M., Holden, SB. and Paulson, LC., Bayesian Optimisation with Gaussian Processes for Premise Selection
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
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
Paulson, LC., A Formalised Theorem in the Partition Calculus Annals of Pure and Applied Logic,
Paulson, LC., Ackermann's Function in Iterative Form: A Proof Assistant Experiment Bulletin of Symbolic Logic,
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
Coward, S., Paulson, L., Drane, T. and Morini, E., Formal Verification of Transcendental Fixed and Floating Point Algorithms using an Automatic Theorem Prover Formal Aspects of Computing: applicable formal methods,
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
Bordg, A., Paulson, L. and Li, W., Simple Type Theory is not too Simple: Grothendieck’s Schemes Without Dependent Types Experimental Mathematics, v. 31
Doi: 10.1080/10586458.2022.2062073
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
Koutsoukou-Argyraki, A., Li, W. and Paulson, LC., Irrationality and Transcendence Criteria for Infinite Series in
Isabelle/HOL Experimental Mathematics,
Paulson, LC., Computational Logic: Its Origins and Applications Proceedings of the Royal Society A: Mathematical, Physical and Engineering Sciences,
Džamonja, M., Koutsoukou-Argyraki, A. and Paulson, LC., Formalising Ordinal Partition Relations Using Isabelle/HOL Experimental Mathematics,
Edmonds, C., Koutsoukou-Argyraki, A. and Paulson, LC., Formalising Szemerédi's Regularity Lemma and Roth's Theorem on Arithmetic Progressions in Isabelle/HOL Journal of Automated Reasoning,
Doi: 10.1007/s10817-022-09650-2
Paulson, LC., Computational Logic: Its Origins and Applications Proceedings of the Royal Society A: Mathematical, Physical and Engineering Sciences,
Conference proceedings
Edmonds, C. and Paulson, LC., 2022. Formalising Fisher's Inequality: Formal Linear Algebraic Proof Techniques in Combinatorics Leibniz International Proceedings in Informatics, LIPIcs, v. 237
Doi: http://doi.org/10.4230/LIPIcs.ITP.2022.11
Mangla, C., Holden, S. and Paulson, L., 2022. Bayesian Ranking for Strategy Scheduling in Automated Theorem Provers IJCAR 2022: Automated Reasoning,
Doi: 10.1007/978-3-031-10769-6_33
Edmonds, C. and Paulson, L., 2022. Formalising Fisher’s Inequality: Formal Linear Algebraic Proof Techniques in Combinatorics LIPIcs : Leibniz International Proceedings in Informatics,
Doi: 10.4230/LIPIcs.ITP.2022.11
Edmonds, C. and Paulson, LC., 2021. A Modular First Formalisation of Combinatorial Design Theory. CICM, v. 12833
Slowik, A., Mangla, C., Jamnik, M., Holden, SB. and Paulson, LC., 2020. Bayesian Optimisation for Premise Selection in Automated Theorem Proving (Student Abstract). Proceedings of the AAAI Conference on Artificial Intelligence, 34(10), v. 34
Doi: 10.1609/aaai.v34i10.7232
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
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
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
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., 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
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
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
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., 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. 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
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,
Akbarpour, B. and Paulson, LC., 2009. Applications of MetiTarski in the Verification of Control and Hybrid Systems. HSCC, v. 5469
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. 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
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
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 HYBRID SYSTEMS: COMPUTATION AND CONTROL, v. 5469
Benzmüller, C. and Paulson, LC., 2009. Quantified Multimodal Logics in Simple Type Theory CoRR, v. abs/0905.2435
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
Paulson, LC., 2008. The relative consistency of the axiom of choice - Mechanized using Isabelle/ZF LOGIC AND THEORY OF ALGORITHMS, v. 5028
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
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
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, 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
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,
Wenzel, M. and Paulson, LC., 2006. Isabelle/Isar.
Wenzel, M. and Paulson, LC., 2006. Isabelle/Isar.
2006. FLoC’06 Workshop on Empirically Successful Computerized Reasoning
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, 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., 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: 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, 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. 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, 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
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. and Paulson, LC., 2004. Analyzing delegation properties SECURITY PROTOCOLS, v. 2845
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,
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., 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,
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,
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,
Bella, G. and Paulson, LC., 2002. A proof of non-repudiation SECURITY PROTOCOLS, v. 2467
Bella, G. and Paulson, LC., 2002. A proof of non-repudiation SECURITY PROTOCOLS, v. 2467
Paulson, LC., 2002. The Reflection Theorem: A Study in Meta-theoretic Reasoning. CADE, v. 2392
Paulson, L., 2002. A proof of non-repudiation - (Transcript of discussion) SECURITY PROTOCOLS, v. 2467
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, L., 2002. A proof of non-repudiation - (Transcript of discussion) SECURITY PROTOCOLS, v. 2467
Paulson, LC., 2002. The Reflection Theorem: A Study in Meta-theoretic Reasoning. CADE, v. 2392
Bella, G., Paulson, LC. and Massacci, F., 2002. The verification of an industrial payment protocol: the SET purchase phase. CCS,
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
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
Paulson, LC., 2001. SET Cardholder Registration: The Secrecy Proofs. IJCAR, v. 2083
Paulson, LC., 2000. Making Sense of Specifications: The Formalization of SET (Transcript of Discussion). Security Protocols Workshop, v. 2133
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,
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. 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
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
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,
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
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. 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
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,
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,
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,
Paulson, LC., 1998. Inductive Analysis of the Internet Protocol TLS (Position Paper). Security Protocols Workshop, v. 1550
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 (Position Paper). Security Protocols Workshop, v. 1550
Bella, G. and Paulson, LC., 1998. Kerberos Version IV: Inductive Analysis of the Secrecy Goals Computer Security — ESORICS 98,
Paulson, LC., 1998. Inductive Analysis of the Internet Protocol TLS (Position Paper). Security Protocols Workshop, v. 1550
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
Bella, G. and Paulson, LC., 1998. Kerberos Version IV: Inductive Analysis of the Secrecy Goals Computer Security — ESORICS 98,
Paulson, LC., 1998. Inductive Analysis of the Internet Protocol TLS (Transcript of Discussion). Security Protocols Workshop, v. 1550
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,
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
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 (Transcript of Discussion). 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,
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
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
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. A Generic Tableau Prover and its Integration with Isabelle (Extended Abstract) CADE-15 Workshop on Integration of Deduction Systems,
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. Mechanising BAN Kerberos by the Inductive Method Computer Aided Verification: 10th International Conference, CAV ’98,
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., 1997. Mechanizing Coinduction and Corecursion in Higher-Order Logic. J. Log. Comput., v. 7
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
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
Doi: 10.1093/logcom/7.2.175
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. 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. Proving Properties of Security Protocols by Induction 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,
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. 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 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 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 (system abstract) Automated Deduction — CADE-11,
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,
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., 1985. Verifying the Unification Algorithm in LCF. Sci. Comput. Program., v. 5
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. 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. Compiler Generation from Denotational Semantics. Method and tools for compiler construction,
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, LC., 1982. A Semantics-Directed Compiler Generator. POPL,
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. and Susanto, KW., Source-Level Proof Reconstruction for Interactive Theorem Proving
Edmonds, C. and Paulson, L., A Modular First Formalisation of Combinatorial Design Theory Intelligent Computer Mathematics 14th International Conference, CICM 2021,
Mangla, C., Paulson, L. and Holden, S., Bayesian Optimisation of Solver Parameters in CBMC
Słowik, A., Mangla, C., Jamnik, M., Holden, S. and Paulson, L., Bayesian Optimisation for Heuristic Configuration in Automated Theorem Proving EPiC Series in Computing,
Doi: 10.29007/q91g
Meng, J. and Paulson, LC., Translating Higher-Order Problems to First-Order Clauses
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
Meng, J. and Paulson, LC., Lightweight Relevance Filtering for Machine-Generated Resolution Problems
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,
Li, W., Yu, L., Wu, Y. and Paulson, L., International Conference on Learning Representations
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
Meng, J. and Paulson, LC., Translating Higher-Order Problems to First-Order Clauses
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, L., Wetzel: Formalisation of an Undecidable Problem Linked to the Continuum Hypothesis
Meng, J. and Paulson, LC., Lightweight Relevance Filtering for Machine-Generated Resolution Problems
Software
Paulson, LC., 2016. Isabelle-86 - source code from the interactive theorem prover Isabelle upon its original release in 1986
Doi: http://doi.org/10.17863/CAM.9039
Gordon, MJC. and Paulson, LC., HOL88 proof assistant
Books
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. 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. A Fixedpoint Approach to Implementing (Co)Inductive Definitions
Paulson, LC., 1993. Introduction to Isabelle
Paulson, LC., 1993. The Isabelle Reference Manual
Paulson, LC., 1993. Isabelle’s Object-Logics
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
Datasets
Paulson, LC., Research data supporting "A semantics-directed compiler generator"
Internet publications