Lawrence C. Paulson

Nik Sultana, Jasmin Christian Blanchette, Lawrence C. Paulson: LEO-II and Satallax on the Sledgehammer test bench. J. Applied Logic 11(1): 91-102 (2013)

James P. Bridge, Lawrence C. Paulson: Case Splitting in an Automatic Theorem Prover for Real-Valued Special Functions. J. Autom. Reasoning 50(1): 99-117 (2013)

Jasmin Christian Blanchette, Sascha Böhme, Lawrence C. Paulson: Extending Sledgehammer with SMT Solvers. J. Autom. Reasoning 51(1): 109-128 (2013)

Christoph Benzmüller, Lawrence C. Paulson: Quantified Multimodal Logics in Simple Type Theory. Logica Universalis 7(1): 7-20 (2013)

Jean Everson Martina, Lawrence C. Paulson: Verifying multicast-based security protocols using the inductive method. SAC 2013: 1824-1829

Ralph Romanos, Lawrence C. Paulson: Proving the Impossibility of Trisecting an Angle and Doubling the Cube. Archive of Formal Proofs 2012 (2012)

Grant Olney Passmore, Lawrence C. Paulson, Leonardo Mendonça de Moura: Real Algebraic Strategies for MetiTarski Proofs. AISC/MKM/Calculemus 2012: 358-370

Lawrence C. Paulson: MetiTarski: Past and Future. ITP 2012: 1-10

Jasmin Christian Blanchette, Sascha Böhme, Lawrence C. Paulson: Extending Sledgehammer with SMT Solvers. CADE 2011: 116-130

Christoph Benzmüller, Lawrence C. Paulson: Multimodal and intuitionistic logics in simple type theory. Logic Journal of the IGPL 18(6): 881-892 (2010)

Behzad Akbarpour, Lawrence C. Paulson: MetiTarski: An Automatic Theorem Prover for Real-Valued Special Functions. J. Autom. Reasoning 44(3): 175-205 (2010)

Rajeev Narayanan, Behzad Akbarpour, Mohamed H. Zaki, Sofiène Tahar, Lawrence C. Paulson: Formal verification of analog circuits in the presence of noise and process variation. DATE 2010: 1309-1312

Lawrence C. Paulson: Functional Programming in ML. Encyclopedia of Software Engineering 2010: 333-346

Matt Kaufmann, Lawrence C. Paulson (Eds.): Interactive Theorem Proving, First International Conference, ITP 2010, Edinburgh, UK, July 11-14, 2010. Proceedings. Lecture Notes in Computer Science 6172, Springer 2010, isbn 978-3-642-14051-8

Jia Meng, Lawrence C. Paulson: Lightweight relevance filtering for machine-generated resolution problems. J. Applied Logic 7(1): 41-57 (2009)

William Denman, Behzad Akbarpour, Sofiène Tahar, Mohamed H. Zaki, Lawrence C. Paulson: Formal verification of analog designs using MetiTarski. FMCAD 2009: 93-100

Behzad Akbarpour, Lawrence C. Paulson: Applications of MetiTarski in the Verification of Control and Hybrid Systems. HSCC 2009: 1-15

Christoph Benzmüller, Lawrence C. Paulson: Quantified Multimodal Logics in Simple Type Theory. CoRR abs/0905.2435 (2009)

Tobias Nipkow, Lawrence C. Paulson: Fun With Tilings. Archive of Formal Proofs 2008 (2008)

Jia Meng, Lawrence C. Paulson: Translating Higher-Order Clauses to First-Order Clauses. J. Autom. Reasoning 40(1): 35-60 (2008)

Behzad Akbarpour, Lawrence C. Paulson: MetiTarski: An Automatic Prover for the Elementary Functions. AISC/MKM/Calculemus 2008: 217-231

Christoph Benzmüller, Lawrence C. Paulson, Frank Theiss, Arnaud Fietzke: LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description). IJCAR 2008: 162-170

Lawrence C. Paulson: The Relative Consistency of the Axiom of Choice - Mechanized Using Isabelle/ZF. CiE 2008: 486-490

Makarius Wenzel, Lawrence C. Paulson, Tobias Nipkow: The Isabelle Framework. TPHOLs 2008: 33-38

Bernhard Beckert, Lawrence C. Paulson: Preface. J. Autom. Reasoning 38(1-3): 1-2 (2007)

Jia Meng, Lawrence C. Paulson, Gerwin Klein: A Termination Checker for Isabelle Hoare Logic. VERIFY 2007

Behzad Akbarpour, Lawrence C. Paulson: Extending a Resolution Prover for Inequalities on Elementary Functions. LPAR 2007: 47-61

Lawrence C. Paulson, Kong Woei Susanto: Source-Level Proof Reconstruction for Interactive Theorem Proving. TPHOLs 2007: 232-245

Jia Meng, Claire Quigley, Lawrence C. Paulson: Automation for interactive proof: First prototype. Inf. Comput. 204(10): 1575-1596 (2006)

Jia Meng, Claire Quigley, Lawrence C. Paulson: Erratum to "Automation for interactive proof: First prototype" [Inform. and Comput. 204(2006) 1575-1596]. Inf. Comput. 204(12): 1852 (2006)

Giampaolo Bella, Fabio Massacci, Lawrence C. Paulson: Verifying the SET Purchase Protocols. J. Autom. Reasoning 36(1-2): 5-37 (2006)

Giampaolo Bella, Lawrence C. Paulson: Accountability protocols: Formalized and verified. ACM Trans. Inf. Syst. Secur. 9(2): 138-161 (2006)

Lawrence C. Paulson: Defining functions on equivalence classes. ACM Trans. Comput. Log. 7(4): 658-675 (2006)

Markus Wenzel, Lawrence C. Paulson: Isabelle/Isar. The Seventeen Provers of the World 2006: 41-49

Sidi O. Ehmety, Lawrence C. Paulson: Mechanizing compositional reasoning for concurrent systems: some lessons. Formal Asp. Comput. 17(1): 58-68 (2005)

Giampaolo Bella, Fabio Massacci, Lawrence C. Paulson: An overview of the verification of SET. Int. J. Inf. Sec. 4(1-2): 17-28 (2005)

Tobias Nipkow, Lawrence C. Paulson: Proof Pearl: Defining Functions over Finite Sets. TPHOLs 2005: 385-396

Lawrence C. Paulson: Organizing Numerical Theories Using Axiomatic Type Classes. J. Autom. Reasoning 33(1): 29-49 (2004)

Jia Meng, Lawrence C. Paulson: Experiments on Supporting Interactive Proof Using Resolution. IJCAR 2004: 372-384

Giampaolo Bella, Fabio Massacci, Lawrence C. Paulson: Verifying the SET registration protocols. IEEE Journal on Selected Areas in Communications 21(1): 77-87 (2003)

Giampaolo Bella, Cristiano Longo, Lawrence C. Paulson: Is the Verification Problem for Cryptographic Protocols Solved?. Security Protocols Workshop 2003: 183-189

Giampaolo Bella, Cristiano Longo, Lawrence C. Paulson: Verifying Second-Level Security Protocols. TPHOLs 2003: 352-366

Tobias Nipkow, Lawrence C. Paulson, Markus Wenzel: Isabelle/HOL - A Proof Assistant for Higher-Order Logic. Lecture Notes in Computer Science 2283, Springer 2002, isbn 3-540-43376-7

Lawrence C. Paulson: The Reflection Theorem: A Study in Meta-theoretic Reasoning. CADE 2002: 377-391

Giampaolo Bella, Lawrence C. Paulson, Fabio Massacci: The verification of an industrial payment protocol: the SET purchase phase. ACM Conference on Computer and Communications Security 2002: 12-20

Lawrence C. Paulson: Verifying the SET Protocol: Overview. FASec 2002: 4-14

Sidi O. Ehmety, Lawrence C. Paulson: Program Composition in Isabelle/UNITY. IPDPS 2002

Giampaolo Bella, Lawrence C. Paulson: Analyzing Delegation Properties. Security Protocols Workshop 2002: 120-127

Lawrence C. Paulson: A Simple Formalization and Proof for the Mutilated Chess Board. Logic Journal of the IGPL 9(3): 475-485 (2001)

Lawrence C. Paulson: Relations Between Secrets: Two Formal Analyses of the Yahalom Protocol. Journal of Computer Security 9(3): 197-216 (2001)

Lawrence C. Paulson: Mechanizing a theory of program composition for UNITY. ACM Trans. Program. Lang. Syst. 23(5): 626-656 (2001)

Lawrence C. Paulson: SET Cardholder Registration: The Secrecy Proofs. IJCAR 2001: 5-12

Giampaolo Bella, Lawrence C. Paulson: A Proof of Non-repudiation. Security Protocols Workshop 2001: 119-125

Lawrence C. Paulson: A Proof of Non-repudiation (Transcript of Discussion). Security Protocols Workshop 2001: 126-133

Giampaolo Bella, Lawrence C. Paulson: Mechanical Proofs about a Non-repudiation Protocol. TPHOLs 2001: 91-104

Lawrence C. Paulson: Mechanizing UNITY in Isabelle. ACM Trans. Comput. Log. 1(1): 3-32 (2000)

Lawrence C. Paulson: A fixedpoint approach to (co)inductive and (co)datatype definitions. Proof, Language, and Interaction 2000: 187-212

Giampaolo Bella, Fabio Massacci, Lawrence C. Paulson, Piero Tramontano: Formal Verification of Cardholder Registration in SET. ESORICS 2000: 159-174

Giampaolo Bella, Fabio Massacci, Lawrence C. Paulson, Piero Tramontano: Making Sense of Specifications: The Formalization of SET. Security Protocols Workshop 2000: 74-81

Lawrence C. Paulson: Making Sense of Specifications: The Formalization of SET (Transcript of Discussion). Security Protocols Workshop 2000: 82-86

Clemens Ballarin, Lawrence C. Paulson: A Pragmatic Approach to Extending Provers by Computer Algebra - with Applications to Coding Theory. Fundam. Inform. 39(1-2): 1-20 (1999)

Florian Kammüller, Lawrence C. Paulson: A Formal Proof of Sylow's Theorem. J. Autom. Reasoning 23(3-4): 235-264 (1999)

Lawrence C. Paulson: A Generic Tableau Prover and its Integration with Isabelle. J. UCS 5(3): 73-87 (1999)

Lawrence C. Paulson: Final coalgebras as greatest fixed points in ZF set theory. Mathematical Structures in Computer Science 9(5): 545-567 (1999)

Lawrence C. Paulson: Inductive Analysis of the Internet Protocol TLS. ACM Trans. Inf. Syst. Secur. 2(3): 332-351 (1999)

Leslie Lamport, Lawrence C. Paulson: Should your specification language be typed. ACM Trans. Program. Lang. Syst. 21(3): 502-526 (1999)

Lawrence C. Paulson: Proving Security Protocols Correct. LICS 1999: 370-381

Lawrence C. Paulson: Relatios Between Secrets: The Yahalom Protocol. Security Protocols Workshop 1999: 73-84

Florian Kammüller, Markus Wenzel, Lawrence C. Paulson: Locales - A Sectioning Concept for Isabelle. TPHOLs 1999: 149-166

Lawrence C. Paulson: The Inductive Approach to Verifying Cryptographic Protocols. Journal of Computer Security 6(1-2): 85-128 (1998)

Jacques D. Fleuriot, Lawrence C. Paulson: Proving Newton's Propositio Kepleriana Using Geometry and Nonstandard Analysis in Isabelle. Automated Deduction in Geometry 1998: 47-66

Clemens Ballarin, Lawrence C. Paulson: Reasoning About Coding Theory: The Benefits We Get from Computer Algebra. AISC 1998: 55-66

Jacques D. Fleuriot, Lawrence C. Paulson: A Combination of Nonstandard Analysis and Geometry Theorem Proving, with Application to Newton's Principia. CADE 1998: 3-16

Giampaolo Bella, Lawrence C. Paulson: Mechanising BAN Kerberos by the Inductive Method. CAV 1998: 416-427

Giampaolo Bella, Lawrence C. Paulson: Kerberos Version 4: Inductive Analysis of the Secrecy Goals. ESORICS 1998: 361-375

Lawrence C. Paulson: Inductive Analysis of the Internet Protocol TLS (Position Paper). Security Protocols Workshop 1998: 1-12

Lawrence C. Paulson: Inductive Analysis of the Internet Protocol TLS (Transcript of Discussion). Security Protocols Workshop 1998: 13-23

Lawrence C. Paulson: Mechanizing Coinduction and Corecursion in Higher-Order Logic. J. Log. Comput. 7(2): 175-204 (1997)

Lawrence C. Paulson: Proving Properties of Security Protocols by Induction. CSFW 1997: 70-83

Lawrence C. Paulson: Mechanized proofs for a recursive authentication protocol. CSFW 1997: 84-95

Lawrence C. Paulson: Mechanizing Coinduction and Corecursion in Higher-order Logic. CoRR cs.LO/9711105 (1997)

Lawrence C. Paulson: Generic Automatic Proof Tools. CoRR cs.LO/9711106 (1997)

Lawrence C. Paulson: ML for the working programmer (2. ed.). Cambridge University Press 1996, isbn 978-0-521-57050-3, pp. I-XVIII, 1-476

Lawrence C. Paulson, Krzysztof Grabczewski: Mechanizing Set Theory. J. Autom. Reasoning 17(3): 291-323 (1996)

Lawrence C. Paulson, Krzysztof Grabczewski: Mechanizing Set Theory: Cardinal Arithmetic and the Axiom of Choice. . CoRR cs.LO/9612104 (1996)

Lawrence C. Paulson: Set Theory for Verification. II: Induction and Recursion. J. Autom. Reasoning 15(2): 167-215 (1995)

Lawrence C. Paulson: Isabelle - A Generic Theorem Prover (with a contribution by T. Nipkow). Lecture Notes in Computer Science 828, Springer 1994, isbn 3-540-58244-4

Lawrence C. Paulson: A Fixedpoint Approach to Implementing (Co)Inductive Definitions. CADE 1994: 148-161

Lawrence C. Paulson: A Concrete Final Coalgebra Theorem for ZF Set Theory. TYPES 1994: 120-139

Lawrence C. Paulson: Set Theory for Verification: I. From Foundations to Functions. J. Autom. Reasoning 11(3): 353-389 (1993)

Lawrence C. Paulson: Verifying the Unification Algorithm in LCF. CoRR cs.LO/9301101 (1993)

Lawrence C. Paulson: Constructing Recursion Operators in Intuitionistic Type Theory. CoRR cs.LO/9301102 (1993)

Lawrence C. Paulson: Proving Termination of Normalization Functions for Conditional Expressions. CoRR cs.LO/9301103 (1993)

Lawrence C. Paulson: Natural Deduction as Higher-Order Resolution. CoRR cs.LO/9301104 (1993)

Lawrence C. Paulson: The Foundation of a Generic Theorem Prover. CoRR cs.LO/9301105 (1993)

Lawrence C. Paulson: Isabelle: The Next 700 Theorem Provers. CoRR cs.LO/9301106 (1993)

Lawrence C. Paulson: A Formulation of the Simple Theory of Types (for Isabelle). CoRR cs.LO/9301107 (1993)

Lawrence C. Paulson: A Higher-Order Implementation of Rewriting. CoRR cs.LO/9301108 (1993)

Lawrence C. Paulson, Andrew W. Smith: Logic Programming, Functional Programming, and Inductive Definitions. CoRR cs.LO/9301109 (1993)

Lawrence C. Paulson: Designing a Theorem Prover. CoRR cs.LO/9301110 (1993)

Lawrence C. Paulson: Set Theory for Verification: I. From Foundations to Functions. CoRR cs.LO/9311103 (1993)

Tobias Nipkow, Lawrence C. Paulson: Isabelle-91. CADE 1992: 673-676

Lawrence C. Paulson: ML for the working programmer. Cambridge University Press 1991, isbn 978-0-521-39022-4, pp. I-X, 1-429

Lawrence C. Paulson: The Foundation of a Generic Theorem Prover. J. Autom. Reasoning 5(3): 363-397 (1989)

Lawrence C. Paulson, Andrew W. Smith: Logic Programming, Functional Programming, and Inductive Definitions. ELP 1989: 283-309

Lawrence C. Paulson: Isabelle: The Next Seven Hundred Theorem Provers. CADE 1988: 772-773

Lawrence C. Paulson: A formulation of the simple theory of types (for Isabelle). Conference on Computer Logic 1988: 246-274

Lawrence C. Paulson: Proving Termination of Normalization Functions for Conditional Experessions. J. Autom. Reasoning 2(1): 63-74 (1986)

Lawrence C. Paulson: Natural Deduction as Higher-Order Resolution. J. Log. Program. 3(3): 237-258 (1986)

Lawrence C. Paulson: Constructing Recursion Operators in Intuitionistic Type Theory. J. Symb. Comput. 2(4): 325-355 (1986)

Lawrence C. Paulson: Lessons Learned from LCF: A Survey of Natural Deduction Proofs. Comput. J. 28(5): 474-479 (1985)

Lawrence C. Paulson: Verifying the Unification Algorithm in LCF. Sci. Comput. Program. 5(2): 143-169 (1985)

Lawrence C. Paulson: Deriving Structural Induction in LCF. Semantics of Data Types 1984: 197-214

Lawrence C. Paulson: A Higher-Order Implementation of Rewriting. Sci. Comput. Program. 3(2): 119-149 (1983)

Lawrence C. Paulson: Compiler Generation from Denotational Semantics. Method and tools for compiler construction 1983: 219-252

Lawrence C. Paulson: A Semantics-Directed Compiler Generator. POPL 1982: 224-233