Lawrence C. Paulson

233 papers A* 6A 15B 13C 5Misc 3Journal 145Unranked 38

Year	Rank	Type	Title / Venue / Authors
2025	J	`jnl`	Compactness Theorem for First-Order Logic. Arch. Formal Proofs Sophie Tourret, Lawrence C. Paulson
2025	J	`jnl`	Complex Lattices, Elliptic Functions, and the Modular Group. Arch. Formal Proofs Manuel Eberl, Anthony Bordg, Wenda Li, Lawrence C. Paulson
2025	J	`jnl`	Dedekind Sums. Arch. Formal Proofs Manuel Eberl, Anthony Bordg, Lawrence C. Paulson, Wenda Li
2025	J	`jnl`	Farey Sequences and Ford Circles. Arch. Formal Proofs Lawrence C. Paulson
2025	B	`conf`	Formalising New Mathematics in Isabelle: Diagonal Ramsey. ITP Lawrence C. Paulson
2025	J	`jnl`	Formalising New Mathematics in Isabelle: Diagonal Ramsey. CoRR Lawrence C. Paulson
2025	J	`jnl`	Transitive Union-Closed Families. Arch. Formal Proofs Angeliki Koutsoukou-Argyraki, Lawrence C. Paulson
2024	J	`jnl`	A formalised theorem in the partition calculus. Ann. Pure Appl. Log. Lawrence C. Paulson
2024	J	`jnl`	An Exponential Improvement for Diagonal Ramsey. Arch. Formal Proofs Lawrence C. Paulson
2024	B	`conf`	Formal Probabilistic Methods for Combinatorial Structures using the Lovász Local Lemma. CPP Chelsea Edmonds, Lawrence C. Paulson
2024	B	`conf`	Formalising Half of a Graduate Textbook on Number Theory (Short Paper). ITP Manuel Eberl, Anthony Bordg, Lawrence C. Paulson, Wenda Li
2024	J	`jnl`	Ramsey Number Bounds. Arch. Formal Proofs Lawrence C. Paulson
2023	J	`jnl`	Euler's Polyhedron Formula. Arch. Formal Proofs Lawrence C. Paulson
2023	J	`jnl`	Formal Probabilistic Methods for Combinatorial Structures in Isabelle/HOL. CoRR Chelsea Edmonds, Lawrence C. Paulson
2023	J	`jnl`	Formalising Szemerédi's Regularity Lemma and Roth's Theorem on Arithmetic Progressions in Isabelle/HOL. J. Autom. Reason. Chelsea Edmonds, Angeliki Koutsoukou-Argyraki, Lawrence C. Paulson
2023	J	`jnl`	Hypergraph Colouring Bounds. Arch. Formal Proofs Chelsea Edmonds, Lawrence C. Paulson
2023	J	`jnl`	Knuth-Morris-Pratt String Search. Arch. Formal Proofs Lawrence C. Paulson
2023	C	`conf`	Large-Scale Formal Proof for the Working Mathematician - Lessons Learnt from the ALEXANDRIA Project. CICM Lawrence C. Paulson
2022	J	`jnl`	Ackermann's Function Is Not Primitive Recursive. Arch. Formal Proofs Lawrence C. Paulson
2022	A	`conf`	Bayesian Ranking for Strategy Scheduling in Automated Theorem Provers. IJCAR Chaitanya Mangla, Sean B. Holden, Lawrence C. Paulson
2022	J	`jnl`	Constructing the Reals as Dedekind Cuts of Rationals. Arch. Formal Proofs Jacques D. Fleuriot, Lawrence C. Paulson
2022	J	`jnl`	Fisher's Inequality: Linear Algebraic Proof Techniques for Combinatorics. Arch. Formal Proofs Chelsea Edmonds, Lawrence C. Paulson
2022	J	`jnl`	Formal Verification of Transcendental Fixed- and Floating-point Algorithms using an Automatic Theorem Prover. Formal Aspects Comput. Samuel Coward, Lawrence C. Paulson, Theo Drane, Emiliano Morini
2022	B	`conf`	Formalising Fisher's Inequality: Formal Linear Algebraic Proof Techniques in Combinatorics. ITP Chelsea Edmonds, Lawrence C. Paulson
2022	J	`jnl`	Formalising Fisher's Inequality: Formal Linear Algebraic Proof Techniques in Combinatorics. CoRR Chelsea Edmonds, Lawrence C. Paulson
2022	J	`jnl`	Formalising Szemerédi's Regularity Lemma and Roth's Theorem on Arithmetic Progressions in Isabelle/HOL. CoRR Chelsea Edmonds, Angeliki Koutsoukou-Argyraki, Lawrence C. Paulson
2022	J	`jnl`	Formalizing Ordinal Partition Relations Using Isabelle/HOL. Exp. Math. Mirna Dzamonja, Angeliki Koutsoukou-Argyraki, Lawrence C. Paulson
2022	J	`jnl`	Irrational numbers from THE BOOK. Arch. Formal Proofs Lawrence C. Paulson
2022	J	`jnl`	Irrationality and Transcendence Criteria for Infinite Series in Isabelle/HOL. Exp. Math. Angeliki Koutsoukou-Argyraki, Wenda Li, Lawrence C. Paulson
2022	J	`jnl`	Khovanskii's Theorem. Arch. Formal Proofs Angeliki Koutsoukou-Argyraki, Lawrence C. Paulson
2022	J	`jnl`	Mathematical Proof Between Generations. CoRR Jonas Bayer, Christoph Benzmüller, Kevin Buzzard, Marco David, Leslie Lamport, Yuri V. Matiyasevich, Lawrence C. Paulson, Dierk Schleicher, Benedikt Stock, Efim I. Zelmanov
2022	J	`jnl`	Simple Type Theory is not too Simple: Grothendieck's Schemes Without Dependent Types. Exp. Math. Anthony Bordg, Lawrence C. Paulson, Wenda Li
2022	J	`jnl`	The Plünnecke-Ruzsa Inequality. Arch. Formal Proofs Angeliki Koutsoukou-Argyraki, Lawrence C. Paulson
2022	J	`jnl`	Wetzel's Problem and the Continuum Hypothesis. Arch. Formal Proofs Lawrence C. Paulson
2022	C	`conf`	Wetzel: Formalisation of an Undecidable Problem Linked to the Continuum Hypothesis. CICM Lawrence C. Paulson
2022	J	`jnl`	Wetzel: Formalisation of an Undecidable Problem Linked to the Continuum Hypothesis. CoRR Lawrence C. Paulson
2022	J	`jnl`	Young's Inequality for Increasing Functions. Arch. Formal Proofs Lawrence C. Paulson
2021	J	`jnl`	A Mechanised Proof of Gödel's Incompleteness Theorems using Nominal Isabelle. CoRR Lawrence C. Paulson
2021	C	`conf`	A Modular First Formalisation of Combinatorial Design Theory. CICM Chelsea Edmonds, Lawrence C. Paulson
2021	J	`jnl`	A Modular First Formalisation of Combinatorial Design Theory. CoRR Chelsea Edmonds, Lawrence C. Paulson
2021	J	`jnl`	Ackermann's Function in Iterative Form: A Proof Assistant Experiment. CoRR Lawrence C. Paulson
2021	J	`jnl`	Ackermann's function in iterative Form: a Proof Assistant Experiment. Bull. Symb. Log. Lawrence C. Paulson
2021	J	`jnl`	Combinatorial Design Theory. Arch. Formal Proofs Chelsea Edmonds, Lawrence C. Paulson
2021	J	`jnl`	Grothendieck's Schemes in Algebraic Geometry. Arch. Formal Proofs Anthony Bordg, Lawrence C. Paulson, Wenda Li
2021	J	`jnl`	Irrationality and Transcendence Criteria for Infinite Series in Isabelle/HOL. CoRR Angeliki Koutsoukou-Argyraki, Wenda Li, Lawrence C. Paulson
2021	A*	`conf`	IsarStep: a Benchmark for High-level Mathematical Reasoning. ICLR Wenda Li, Lei Yu, Yuhuai Wu, Lawrence C. Paulson
2021	J	`jnl`	Roth's Theorem on Arithmetic Progressions. Arch. Formal Proofs Chelsea Edmonds, Angeliki Koutsoukou-Argyraki, Lawrence C. Paulson
2021	J	`jnl`	Simple Type Theory is not too Simple: Grothendieck's Schemes without Dependent Types. CoRR Anthony Bordg, Lawrence C. Paulson, Wenda Li
2021	J	`jnl`	Szemerédi's Regularity Lemma. Arch. Formal Proofs Chelsea Edmonds, Angeliki Koutsoukou-Argyraki, Lawrence C. Paulson
2021	J	`jnl`	The Inductive Approach to Verifying Cryptographic Protocols. CoRR Lawrence C. Paulson
2021	J	`jnl`	The Relative Consistency of the Axiom of Choice Mechanized Using Isabelle/ZF. CoRR Lawrence C. Paulson
2020	—	`conf`	Algebraically Closed Fields in Isabelle/HOL. IJCAR (2) Paulo Emílio de Vilhena, Lawrence C. Paulson
2020	A*	`conf`	Bayesian Optimisation for Premise Selection in Automated Theorem Proving (Student Abstract). AAAI Agnieszka Slowik, Chaitanya Mangla, Mateja Jamnik, Sean B. Holden, Lawrence C. Paulson
2020	—	`conf`	Bayesian Optimisation of Solver Parameters in CBMC. SMT Chaitanya Mangla, Sean B. Holden, Lawrence C. Paulson
2020	J	`jnl`	Evaluating Winding Numbers and Counting Complex Roots Through Cauchy Indices in Isabelle/HOL. J. Autom. Reason. Wenda Li, Lawrence C. Paulson
2020	J	`jnl`	Modelling High-Level Mathematical Reasoning in Mechanised Declarative Proofs. CoRR Wenda Li, Lei Yu, Yuhuai Wu, Lawrence C. Paulson
2020	J	`jnl`	Ordinal Partitions. Arch. Formal Proofs Lawrence C. Paulson
2020	J	`jnl`	The Nash-Williams Partition Theorem. Arch. Formal Proofs Lawrence C. Paulson
2019	J	`jnl`	An Isabelle/HOL Formalisation of Green's Theorem. J. Autom. Reason. Mohammad Abdulaziz, Lawrence C. Paulson
2019	—	`conf`	Bayesian Optimisation for Heuristic Configuration in Automated Theorem Proving. Vampire Agnieszka Slowik, Chaitanya Mangla, Mateja Jamnik, Sean B. Holden, Lawrence C. Paulson
2019	J	`jnl`	Bayesian Optimisation with Gaussian Processes for Premise Selection. CoRR Agnieszka Slowik, Chaitanya Mangla, Mateja Jamnik, Sean B. Holden, Lawrence C. Paulson
2019	B	`conf`	Counting polynomial roots in isabelle/hol: a formal proof of the budan-fourier theorem. CPP Wenda Li, Lawrence C. Paulson
2019	J	`jnl`	Deciding Univariate Polynomial Problems Using Untrusted Certificates in Isabelle/HOL. J. Autom. Reason. Wenda Li, Grant Olney Passmore, Lawrence C. Paulson
2019	J	`jnl`	Defining Functions on Equivalence Classes. CoRR Lawrence C. Paulson
2019	J	`jnl`	Fourier Series. Arch. Formal Proofs Lawrence C. Paulson
2019	J	`jnl`	From LCF to Isabelle/HOL. CoRR Lawrence C. Paulson, Tobias Nipkow, Makarius Wenzel
2019	J	`jnl`	From LCF to Isabelle/HOL. Formal Aspects Comput. Lawrence C. Paulson, Tobias Nipkow, Makarius Wenzel
2019	J	`jnl`	Inductive Analysis of the Internet Protocol TLS. CoRR Lawrence C. Paulson
2019	J	`jnl`	Using Machine Learning to Improve Cylindrical Algebraic Decomposition. Math. Comput. Sci. Zongyan Huang, Matthew England, David J. Wilson, James P. Bridge, James H. Davenport, Lawrence C. Paulson
2019	J	`jnl`	Zermelo Fraenkel Set Theory in Higher-Order Logic. Arch. Formal Proofs Lawrence C. Paulson
2018	J	`jnl`	An Isabelle/HOL formalisation of Green's Theorem. Arch. Formal Proofs Mohammad Abdulaziz, Lawrence C. Paulson
2018	J	`jnl`	Counting Polynomial Roots in Isabelle/HOL: A Formal Proof of the Budan-Fourier Theorem. CoRR Wenda Li, Lawrence C. Paulson
2018	J	`jnl`	Evaluating Winding Numbers and Counting Complex Roots through Cauchy Indices in Isabelle/HOL. CoRR Wenda Li, Lawrence C. Paulson
2018	J	`jnl`	Formalising Mathematics In Simple Type Theory. CoRR Lawrence C. Paulson
2018	J	`jnl`	Introduction to Milestones in Interactive Theorem Proving. J. Autom. Reason. Jeremy Avigad, Jasmin Christian Blanchette, Gerwin Klein, Lawrence C. Paulson, Andrei Popescu, Gregor Snelting
2018	J	`jnl`	Michael John Caldwell Gordon (FRS 1994), 28 February 1948 - 22 August 2017. CoRR Lawrence C. Paulson
2018	J	`jnl`	Quaternions. Arch. Formal Proofs Lawrence C. Paulson
2018	J	`jnl`	The Prime Number Theorem. Arch. Formal Proofs Manuel Eberl, Lawrence C. Paulson
2018	J	`jnl`	Using Machine Learning to Improve Cylindrical Algebraic Decomposition. CoRR Zongyan Huang, Matthew England, David J. Wilson, James H. Davenport, Lawrence C. Paulson
2017	J	`jnl`	Computational Logic: Its Origins and Applications. CoRR Lawrence C. Paulson
2017	B	`conf`	Porting the HOL light analysis library: some lessons (invited talk). CPP Lawrence C. Paulson
2016	B	`conf`	A Formal Proof of Cauchy's Residue Theorem. ITP Wenda Li, Lawrence C. Paulson
2016	B	`conf`	A modular, efficient formalisation of real algebraic numbers. CPP Wenda Li, Lawrence C. Paulson
2016	B	`conf`	An Isabelle/HOL Formalisation of Green's Theorem. ITP Mohammad Abdulaziz, Lawrence C. Paulson
2016	J	`jnl`	Hammering towards QED. J. Formaliz. Reason. Jasmin Christian Blanchette, Cezary Kaliszyk, Lawrence C. Paulson, Josef Urban
2016	J	`jnl`	Source Coding Theorem. Arch. Formal Proofs Quentin Hibon, Lawrence C. Paulson
2016	J	`jnl`	The Cartan Fixed Point Theorems. Arch. Formal Proofs Lawrence C. Paulson
2016	J	`jnl`	Using Machine Learning to Decide When to Precondition Cylindrical Algebraic Decomposition With Groebner Bases. CoRR Zongyan Huang, Matthew England, James H. Davenport, Lawrence C. Paulson
2016	Misc	`conf`	Using Machine Learning to Decide When to Precondition Cylindrical Algebraic Decomposition with Groebner Bases. SYNASC Zongyan Huang, Matthew England, James H. Davenport, Lawrence C. Paulson
2015	J	`jnl`	A Complete Decision Procedure for Univariate Polynomial Problems in Isabelle/HOL. CoRR Wenda Li, Grant Olney Passmore, Lawrence C. Paulson
2015	A	`conf`	A Formalisation of Finite Automata Using Hereditarily Finite Sets. CADE Lawrence C. Paulson
2015	J	`jnl`	A Formalisation of Finite Automata using Hereditarily Finite Sets. CoRR Lawrence C. Paulson
2015	J	`jnl`	A Mechanised Proof of Gödel's Incompleteness Theorems Using Nominal Isabelle. J. Autom. Reason. Lawrence C. Paulson
2015	J	`jnl`	Finite Automata in Hereditarily Finite Set Theory. Arch. Formal Proofs Lawrence C. Paulson
2015	—	`conf`	Proofs and Reconstructions. FroCos Nik Sultana, Christoph Benzmüller, Lawrence C. Paulson
2015	J	`jnl`	The Higher-Order Prover Leo-II. J. Autom. Reason. Christoph Benzmüller, Nik Sultana, Lawrence C. Paulson, Frank Theiss
2015	J	`jnl`	Verifying multicast-based security protocols using the inductive method. Int. J. Inf. Sec. Jean Everson Martina, Lawrence C. Paulson
2014	J	`jnl`	A Comparison of Three Heuristics to Choose the Variable Ordering for Cylindrical Algebraic Decomposition. ACM Commun. Comput. Algebra Zongyan Huang, Matthew England, David J. Wilson, James H. Davenport, Lawrence C. Paulson
2014	J	`jnl`	A Machine-Assisted Proof of Gödel's Incompleteness theorems for the Theory of Hereditarily Finite Sets. Rev. Symb. Log. Lawrence C. Paulson
2014	J	`jnl`	A comparison of three heuristics to choose the variable ordering for CAD. CoRR Zongyan Huang, Matthew England, David J. Wilson, James H. Davenport, Lawrence C. Paulson
2014	C	`conf`	Applying Machine Learning to the Problem of Choosing a Heuristic to Select the Variable Ordering for Cylindrical Algebraic Decomposition. CICM Zongyan Huang, Matthew England, David J. Wilson, James H. Davenport, Lawrence C. Paulson, James P. Bridge
2014	J	`jnl`	Applying machine learning to the problem of choosing a heuristic to select the variable ordering for cylindrical algebraic decomposition. CoRR Zongyan Huang, Matthew England, David J. Wilson, James H. Davenport, Lawrence C. Paulson, James P. Bridge
2014	—	`conf`	Automated theorem proving for special functions: the next phase. SNC Lawrence C. Paulson
2014	J	`jnl`	Machine Learning for First-Order Theorem Proving - Learning to Select a Good Heuristic. J. Autom. Reason. James P. Bridge, Sean B. Holden, Lawrence C. Paulson
2014	J	`jnl`	Real-Valued Special Functions: Upper and Lower Bounds. Arch. Formal Proofs Lawrence C. Paulson
2014	—	`conf`	Verifying Hybrid Systems Involving Transcendental Functions. NASA Formal Methods Paul B. Jackson, Andrew Sogokon, James P. Bridge, Lawrence C. Paulson
2013	J	`jnl`	Case Splitting in an Automatic Theorem Prover for Real-Valued Special Functions. J. Autom. Reason. James P. Bridge, Lawrence C. Paulson
2013	J	`jnl`	Extending Sledgehammer with SMT Solvers. J. Autom. Reason. Jasmin Christian Blanchette, Sascha Böhme, Lawrence C. Paulson
2013	J	`jnl`	Gödel's Incompleteness Theorems. Arch. Formal Proofs Lawrence C. Paulson
2013	J	`jnl`	LEO-II and Satallax on the Sledgehammer test bench. J. Appl. Log. Nik Sultana, Jasmin Christian Blanchette, Lawrence C. Paulson
2013	—	`conf`	MetiTarski's Menagerie of Cooperating Systems. FroCos Lawrence C. Paulson
2013	J	`jnl`	Quantified Multimodal Logics in Simple Type Theory. Logica Universalis Christoph Benzmüller, Lawrence C. Paulson
2013	J	`jnl`	The Hereditarily Finite Sets. Arch. Formal Proofs Lawrence C. Paulson
2013	Misc	`conf`	Verifying multicast-based security protocols using the inductive method. SAC Jean Everson Martina, Lawrence C. Paulson
2012	B	`conf`	MetiTarski: Past and Future. ITP Lawrence C. Paulson
2012	J	`jnl`	Proving the Impossibility of Trisecting an Angle and Doubling the Cube. Arch. Formal Proofs Ralph Romanos, Lawrence C. Paulson
2012	—	`conf`	Real Algebraic Strategies for MetiTarski Proofs. AISC/MKM/Calculemus Grant Olney Passmore, Lawrence C. Paulson, Leonardo Mendonça de Moura
2011	A	`conf`	Extending Sledgehammer with SMT Solvers. CADE Jasmin Christian Blanchette, Sascha Böhme, Lawrence C. Paulson
2010	A	`conf`	Formal verification of analog circuits in the presence of noise and process variation. DATE Rajeev Narayanan, Behzad Akbarpour, Mohamed H. Zaki, Sofiène Tahar, Lawrence C. Paulson
2010	—	`ch.`	Functional Programming in ML. Encyclopedia of Software Engineering Lawrence C. Paulson
2010	B	`ed.`	Interactive Theorem Proving, First International Conference, ITP 2010, Edinburgh, UK, July 11-14, 2010. Proceedings ITP Matt Kaufmann, Lawrence C. Paulson
2010	J	`jnl`	MetiTarski: An Automatic Theorem Prover for Real-Valued Special Functions. J. Autom. Reason. Behzad Akbarpour, Lawrence C. Paulson
2010	J	`jnl`	Multimodal and intuitionistic logics in simple type theory. Log. J. IGPL Christoph Benzmüller, Lawrence C. Paulson
2010	—	`conf`	Three Years of Experience with Sledgehammer, a Practical Link between Automatic and Interactive Theorem Provers. PAAR@IJCAR Lawrence C. Paulson
2010	—	`conf`	Three years of experience with Sledgehammer, a Practical Link Between Automatic and Interactive Theorem Provers. IWIL@LPAR Lawrence C. Paulson, Jasmin Christian Blanchette
2009	—	`conf`	Applications of MetiTarski in the Verification of Control and Hybrid Systems. HSCC Behzad Akbarpour, Lawrence C. Paulson
2009	B	`conf`	Formal verification of analog designs using MetiTarski. FMCAD William Denman, Behzad Akbarpour, Sofiène Tahar, Mohamed H. Zaki, Lawrence C. Paulson
2009	J	`jnl`	Lightweight relevance filtering for machine-generated resolution problems. J. Appl. Log. Jia Meng, Lawrence C. Paulson
2009	J	`jnl`	Quantified Multimodal Logics in Simple Type Theory CoRR Christoph Benzmüller, Lawrence C. Paulson
2008	J	`jnl`	Fun With Tilings. Arch. Formal Proofs Tobias Nipkow, Lawrence C. Paulson
2008	A	`conf`	LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description). IJCAR Christoph Benzmüller, Lawrence C. Paulson, Frank Theiss, Arnaud Fietzke
2008	—	`conf`	MetiTarski: An Automatic Prover for the Elementary Functions. AISC/MKM/Calculemus Behzad Akbarpour, Lawrence C. Paulson
2008	—	`conf`	The Isabelle Framework. TPHOLs Makarius Wenzel, Lawrence C. Paulson, Tobias Nipkow
2008	C	`conf`	The Relative Consistency of the Axiom of Choice - Mechanized Using Isabelle/ZF. CiE Lawrence C. Paulson
2008	J	`jnl`	Translating Higher-Order Clauses to First-Order Clauses. J. Autom. Reason. Jia Meng, Lawrence C. Paulson
2007	—	`conf`	A Termination Checker for Isabelle Hoare Logic. VERIFY Jia Meng, Lawrence C. Paulson, Gerwin Klein
2007	B	`conf`	Extending a Resolution Prover for Inequalities on Elementary Functions. LPAR Behzad Akbarpour, Lawrence C. Paulson
2007	J	`jnl`	Preface. J. Autom. Reason. Bernhard Beckert, Lawrence C. Paulson
2007	—	`conf`	Source-Level Proof Reconstruction for Interactive Theorem Proving. TPHOLs Lawrence C. Paulson, Kong Woei Susanto
2006	J	`jnl`	Accountability protocols: Formalized and verified. ACM Trans. Inf. Syst. Secur. Giampaolo Bella, Lawrence C. Paulson
2006	J	`jnl`	Automation for interactive proof: First prototype. Inf. Comput. Jia Meng, Claire Quigley, Lawrence C. Paulson
2006	J	`jnl`	Defining functions on equivalence classes. ACM Trans. Comput. Log. Lawrence C. Paulson
2006	J	`jnl`	Erratum to "Automation for interactive proof: First prototype" [Inform. and Comput. 204(2006) 1575-1596]. Inf. Comput. Jia Meng, Claire Quigley, Lawrence C. Paulson
2006	—	`ch.`	Isabelle/Isar. The Seventeen Provers of the World Markus Wenzel, Lawrence C. Paulson
2006	J	`jnl`	Verifying the SET Purchase Protocols. J. Autom. Reason. Giampaolo Bella, Fabio Massacci, Lawrence C. Paulson
2005	J	`jnl`	An overview of the verification of SET. Int. J. Inf. Sec. Giampaolo Bella, Fabio Massacci, Lawrence C. Paulson
2005	J	`jnl`	Mechanizing compositional reasoning for concurrent systems: some lessons. Formal Aspects Comput. Sidi O. Ehmety, Lawrence C. Paulson
2005	—	`conf`	Proof Pearl: Defining Functions over Finite Sets. TPHOLs Tobias Nipkow, Lawrence C. Paulson
2004	A	`conf`	Experiments on Supporting Interactive Proof Using Resolution. IJCAR Jia Meng, Lawrence C. Paulson
2004	J	`jnl`	Organizing Numerical Theories Using Axiomatic Type Classes. J. Autom. Reason. Lawrence C. Paulson
2003	—	`conf`	Is the Verification Problem for Cryptographic Protocols Solved?. Security Protocols Workshop Giampaolo Bella, Cristiano Longo, Lawrence C. Paulson
2003	J	`jnl`	The Relative Consistency of the Axiom of Choice Mechanized Using Isabelle⁄zf. LMS J. Comput. Math. Lawrence C. Paulson
2003	—	`conf`	Verifying Second-Level Security Protocols. TPHOLs Giampaolo Bella, Cristiano Longo, Lawrence C. Paulson
2003	J	`jnl`	Verifying the SET registration protocols. IEEE J. Sel. Areas Commun. Giampaolo Bella, Fabio Massacci, Lawrence C. Paulson
2002	—	`conf`	Analyzing Delegation Properties. Security Protocols Workshop Giampaolo Bella, Lawrence C. Paulson
2002	—	`book`	Isabelle/HOL - A Proof Assistant for Higher-Order Logic Tobias Nipkow, Lawrence C. Paulson, Markus Wenzel
2002	A	`conf`	Program Composition in Isabelle/UNITY. IPDPS Sidi O. Ehmety, Lawrence C. Paulson
2002	A	`conf`	The Reflection Theorem: A Study in Meta-theoretic Reasoning. CADE Lawrence C. Paulson
2002	A*	`conf`	The verification of an industrial payment protocol: the SET purchase phase. CCS Giampaolo Bella, Lawrence C. Paulson, Fabio Massacci
2002	—	`conf`	Verifying the SET Protocol: Overview. FASec Lawrence C. Paulson
2001	—	`conf`	A Proof of Non-repudiation (Transcript of Discussion). Security Protocols Workshop Lawrence C. Paulson
2001	—	`conf`	A Proof of Non-repudiation. Security Protocols Workshop Giampaolo Bella, Lawrence C. Paulson
2001	J	`jnl`	A Simple Formalization and Proof for the Mutilated Chess Board. Log. J. IGPL Lawrence C. Paulson
2001	—	`conf`	Mechanical Proofs about a Non-repudiation Protocol. TPHOLs Giampaolo Bella, Lawrence C. Paulson
2001	J	`jnl`	Mechanizing a theory of program composition for UNITY. ACM Trans. Program. Lang. Syst. Lawrence C. Paulson
2001	J	`jnl`	Relations Between Secrets: Two Formal Analyses of the Yahalom Protocol. J. Comput. Secur. Lawrence C. Paulson
2001	A	`conf`	SET Cardholder Registration: The Secrecy Proofs. IJCAR Lawrence C. Paulson
2000	—	`conf`	A fixedpoint approach to (co)inductive and (co)datatype definitions. Proof, Language, and Interaction Lawrence C. Paulson
2000	A	`conf`	Formal Verification of Cardholder Registration in SET. ESORICS Giampaolo Bella, Fabio Massacci, Lawrence C. Paulson, Piero Tramontano
2000	—	`conf`	Making Sense of Specifications: The Formalization of SET (Transcript of Discussion). Security Protocols Workshop Lawrence C. Paulson
2000	—	`conf`	Making Sense of Specifications: The Formalization of SET. Security Protocols Workshop Giampaolo Bella, Fabio Massacci, Lawrence C. Paulson, Piero Tramontano
2000	J	`jnl`	Mechanizing Nonstandard Real Analysis. LMS J. Comput. Math. Jacques D. Fleuriot, Lawrence C. Paulson
2000	J	`jnl`	Mechanizing UNITY in Isabelle. ACM Trans. Comput. Log. Lawrence C. Paulson
1999	J	`jnl`	A Formal Proof of Sylow's Theorem. J. Autom. Reason. Florian Kammüller, Lawrence C. Paulson
1999	J	`jnl`	A Generic Tableau Prover and its Integration with Isabelle. J. Univers. Comput. Sci. Lawrence C. Paulson
1999	J	`jnl`	A Pragmatic Approach to Extending Provers by Computer Algebra - with Applications to Coding Theory. Fundam. Informaticae Clemens Ballarin, Lawrence C. Paulson
1999	J	`jnl`	Final coalgebras as greatest fixed points in ZF set theory. Math. Struct. Comput. Sci. Lawrence C. Paulson
1999	J	`jnl`	Inductive Analysis of the Internet Protocol TLS. ACM Trans. Inf. Syst. Secur. Lawrence C. Paulson
1999	—	`conf`	Locales - A Sectioning Concept for Isabelle. TPHOLs Florian Kammüller, Markus Wenzel, Lawrence C. Paulson
1999	A*	`conf`	Proving Security Protocols Correct. LICS Lawrence C. Paulson
1999	—	`conf`	Relatios Between Secrets: The Yahalom Protocol. Security Protocols Workshop Lawrence C. Paulson
1999	J	`jnl`	Should your specification language be typed. ACM Trans. Program. Lang. Syst. Leslie Lamport, Lawrence C. Paulson
1998	A	`conf`	A Combination of Nonstandard Analysis and Geometry Theorem Proving, with Application to Newton's Principia. CADE Jacques D. Fleuriot, Lawrence C. Paulson
1998	—	`conf`	Inductive Analysis of the Internet Protocol TLS (Position Paper). Security Protocols Workshop Lawrence C. Paulson
1998	—	`conf`	Inductive Analysis of the Internet Protocol TLS (Transcript of Discussion). Security Protocols Workshop Lawrence C. Paulson
1998	A	`conf`	Kerberos Version 4: Inductive Analysis of the Secrecy Goals. ESORICS Giampaolo Bella, Lawrence C. Paulson
1998	A*	`conf`	Mechanising BAN Kerberos by the Inductive Method. CAV Giampaolo Bella, Lawrence C. Paulson
1998	—	`conf`	Proving Newton's Propositio Kepleriana Using Geometry and Nonstandard Analysis in Isabelle. Automated Deduction in Geometry Jacques D. Fleuriot, Lawrence C. Paulson
1998	Misc	`conf`	Reasoning About Coding Theory: The Benefits We Get from Computer Algebra. AISC Clemens Ballarin, Lawrence C. Paulson
1998	J	`jnl`	The Inductive Approach to Verifying Cryptographic Protocols. J. Comput. Secur. Lawrence C. Paulson
1997	J	`jnl`	Generic Automatic Proof Tools CoRR Lawrence C. Paulson
1997	—	`conf`	Mechanized proofs for a recursive authentication protocol. CSFW Lawrence C. Paulson
1997	J	`jnl`	Mechanizing Coinduction and Corecursion in Higher-Order Logic. J. Log. Comput. Lawrence C. Paulson
1997	J	`jnl`	Mechanizing Coinduction and Corecursion in Higher-order Logic CoRR Lawrence C. Paulson
1997	—	`conf`	Proving Properties of Security Protocols by Induction. CSFW Lawrence C. Paulson
1996	—	`book`	ML for the working programmer (2. ed.). Lawrence C. Paulson
1996	J	`jnl`	Mechanizing Set Theory. J. Autom. Reason. Lawrence C. Paulson, Krzysztof Grabczewski
1996	J	`jnl`	Mechanizing Set Theory: Cardinal Arithmetic and the Axiom of Choice. CoRR Lawrence C. Paulson, Krzysztof Grabczewski
1995	J	`jnl`	A Concrete Final Coalgebra Theorem for ZF Set Theory. CoRR Lawrence C. Paulson
1995	J	`jnl`	Set Theory for Verification. II: Induction and Recursion. J. Autom. Reason. Lawrence C. Paulson
1995	J	`jnl`	Set Theory for Verification: II. Induction and Recursion. CoRR Lawrence C. Paulson
1994	—	`conf`	A Concrete Final Coalgebra Theorem for ZF Set Theory. TYPES Lawrence C. Paulson
1994	A	`conf`	A Fixedpoint Approach to Implementing (Co)Inductive Definitions. CADE Lawrence C. Paulson
1994	—	`book`	Isabelle - A Generic Theorem Prover (with a contribution by T. Nipkow) Lawrence C. Paulson
1993	J	`jnl`	A Formulation of the Simple Theory of Types (for Isabelle) CoRR Lawrence C. Paulson
1993	J	`jnl`	A Higher-Order Implementation of Rewriting CoRR Lawrence C. Paulson
1993	J	`jnl`	Constructing Recursion Operators in Intuitionistic Type Theory CoRR Lawrence C. Paulson
1993	J	`jnl`	Designing a Theorem Prover CoRR Lawrence C. Paulson
1993	J	`jnl`	Isabelle: The Next 700 Theorem Provers CoRR Lawrence C. Paulson
1993	J	`jnl`	Logic Programming, Functional Programming, and Inductive Definitions CoRR Lawrence C. Paulson, Andrew W. Smith
1993	J	`jnl`	Natural Deduction as Higher-Order Resolution CoRR Lawrence C. Paulson
1993	J	`jnl`	Proving Termination of Normalization Functions for Conditional Expressions CoRR Lawrence C. Paulson
1993	J	`jnl`	Set Theory for Verification: I. From Foundations to Functions CoRR Lawrence C. Paulson
1993	J	`jnl`	Set Theory for Verification: I. From Foundations to Functions. J. Autom. Reason. Lawrence C. Paulson
1993	J	`jnl`	The Foundation of a Generic Theorem Prover CoRR Lawrence C. Paulson
1993	J	`jnl`	Verifying the Unification Algorithm in LCF CoRR Lawrence C. Paulson
1992	A	`conf`	Isabelle-91. CADE Tobias Nipkow, Lawrence C. Paulson
1991	—	`book`	ML for the working programmer. Lawrence C. Paulson
1989	—	`conf`	Logic Programming, Functional Programming, and Inductive Definitions. ELP Lawrence C. Paulson, Andrew W. Smith
1989	J	`jnl`	The Foundation of a Generic Theorem Prover. J. Autom. Reason. Lawrence C. Paulson
1988	—	`conf`	A formulation of the simple theory of types (for Isabelle). Conference on Computer Logic Lawrence C. Paulson
1988	A	`conf`	Isabelle: The Next Seven Hundred Theorem Provers. CADE Lawrence C. Paulson
1987	—	`book`	Logic and computation - interactive proof with Cambridge LCF. Lawrence C. Paulson
1986	J	`jnl`	Constructing Recursion Operators in Intuitionistic Type Theory. J. Symb. Comput. Lawrence C. Paulson
1986	J	`jnl`	Natural Deduction as Higher-Order Resolution. J. Log. Program. Lawrence C. Paulson
1986	J	`jnl`	Proving Termination of Normalization Functions for Conditional Experessions. J. Autom. Reason. Lawrence C. Paulson
1985	J	`jnl`	Lessons Learned from LCF: A Survey of Natural Deduction Proofs. Comput. J. Lawrence C. Paulson
1985	J	`jnl`	Verifying the Unification Algorithm in LCF. Sci. Comput. Program. Lawrence C. Paulson
1984	—	`conf`	Deriving Structural Induction in LCF. Semantics of Data Types Lawrence C. Paulson
1983	J	`jnl`	A Higher-Order Implementation of Rewriting. Sci. Comput. Program. Lawrence C. Paulson
1983	—	`conf`	Compiler Generation from Denotational Semantics. Method and tools for compiler construction Lawrence C. Paulson
1982	A*	`conf`	A Semantics-Directed Compiler Generator. POPL Lawrence C. Paulson
1981	—	`—`	A compiler generator for semantic grammars. Lawrence C. Paulson