 | 2009 |
|---|
| 98 |       | William Denman,
Behzad Akbarpour,
Sofiène Tahar,
Mohamed H. Zaki,
Lawrence C. Paulson:
Formal verification of analog designs using MetiTarski.
FMCAD 2009: 93-100 |
| 97 | | Behzad Akbarpour,
Lawrence C. Paulson:
Applications of MetiTarski in the Verification of Control and Hybrid Systems.
HSCC 2009: 1-15 |
| 96 | | Christoph Benzmüller,
Lawrence C. Paulson:
Quantified Multimodal Logics in Simple Type Theory
CoRR abs/0905.2435: (2009) |
| 95 | | Jia Meng,
Lawrence C. Paulson:
Lightweight relevance filtering for machine-generated resolution problems.
J. Applied Logic 7(1): 41-57 (2009) |
| 2008 |
|---|
| 94 | | Behzad Akbarpour,
Lawrence C. Paulson:
MetiTarski: An Automatic Prover for the Elementary Functions.
AISC/MKM/Calculemus 2008: 217-231 |
| 93 | | Lawrence C. Paulson:
The Relative Consistency of the Axiom of Choice - Mechanized Using Isabelle/ZF.
CiE 2008: 486-490 |
| 92 | | 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 |
| 91 | | Makarius Wenzel,
Lawrence C. Paulson,
Tobias Nipkow:
The Isabelle Framework.
TPHOLs 2008: 33-38 |
| 90 | | Jia Meng,
Lawrence C. Paulson:
Translating Higher-Order Clauses to First-Order Clauses.
J. Autom. Reasoning 40(1): 35-60 (2008) |
| 2007 |
|---|
| 89 | | Behzad Akbarpour,
Lawrence C. Paulson:
Extending a Resolution Prover for Inequalities on Elementary Functions.
LPAR 2007: 47-61 |
| 88 | | Lawrence C. Paulson,
Kong Woei Susanto:
Source-Level Proof Reconstruction for Interactive Theorem Proving.
TPHOLs 2007: 232-245 |
| 87 | | Jia Meng,
Lawrence C. Paulson,
Gerwin Klein:
A Termination Checker for Isabelle Hoare Logic.
VERIFY 2007 |
| 86 | | Bernhard Beckert,
Lawrence C. Paulson:
Preface.
J. Autom. Reasoning 38(1-3): 1-2 (2007) |
| 2006 |
|---|
| 85 | | Markus Wenzel,
Lawrence C. Paulson:
Isabelle/Isar.
The Seventeen Provers of the World 2006: 41-49 |
| 84 | | Lawrence C. Paulson:
Defining functions on equivalence classes.
ACM Trans. Comput. Log. 7(4): 658-675 (2006) |
| 83 | | Giampaolo Bella,
Lawrence C. Paulson:
Accountability protocols: Formalized and verified.
ACM Trans. Inf. Syst. Secur. 9(2): 138-161 (2006) |
| 82 | | Jia Meng,
Claire Quigley,
Lawrence C. Paulson:
Automation for interactive proof: First prototype.
Inf. Comput. 204(10): 1575-1596 (2006) |
| 81 | | 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) |
| 80 | | Giampaolo Bella,
Fabio Massacci,
Lawrence C. Paulson:
Verifying the SET Purchase Protocols.
J. Autom. Reasoning 36(1-2): 5-37 (2006) |
| 2005 |
|---|
| 79 | | Tobias Nipkow,
Lawrence C. Paulson:
Proof Pearl: Defining Functions over Finite Sets.
TPHOLs 2005: 385-396 |
| 78 | | Sidi O. Ehmety,
Lawrence C. Paulson:
Mechanizing compositional reasoning for concurrent systems: some lessons.
Formal Asp. Comput. 17(1): 58-68 (2005) |
| 77 | | Giampaolo Bella,
Fabio Massacci,
Lawrence C. Paulson:
An overview of the verification of SET.
Int. J. Inf. Sec. 4(1-2): 17-28 (2005) |
| 2004 |
|---|
| 76 | | Jia Meng,
Lawrence C. Paulson:
Experiments on Supporting Interactive Proof Using Resolution.
IJCAR 2004: 372-384 |
| 75 | | Lawrence C. Paulson:
Organizing Numerical Theories Using Axiomatic Type Classes.
J. Autom. Reasoning 33(1): 29-49 (2004) |
| 2003 |
|---|
| 74 | | Giampaolo Bella,
Cristiano Longo,
Lawrence C. Paulson:
Is the Verification Problem for Cryptographic Protocols Solved?.
Security Protocols Workshop 2003: 183-189 |
| 73 | | Giampaolo Bella,
Cristiano Longo,
Lawrence C. Paulson:
Verifying Second-Level Security Protocols.
TPHOLs 2003: 352-366 |
| 2002 |
|---|
| 72 |  | Tobias Nipkow,
Lawrence C. Paulson,
Markus Wenzel:
Isabelle/HOL - A Proof Assistant for Higher-Order Logic
Springer 2002 |
| 71 | | 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 |
| 70 | | Lawrence C. Paulson:
The Reflection Theorem: A Study in Meta-theoretic Reasoning.
CADE 2002: 377-391 |
| 69 | | Lawrence C. Paulson:
Verifying the SET Protocol: Overview.
FASec 2002: 4-14 |
| 68 | | Sidi O. Ehmety,
Lawrence C. Paulson:
Program Composition in Isabelle/UNITY.
IPDPS 2002 |
| 67 | | Giampaolo Bella,
Lawrence C. Paulson:
Analyzing Delegation Properties.
Security Protocols Workshop 2002: 120-127 |
| 2001 |
|---|
| 66 | | Lawrence C. Paulson:
SET Cardholder Registration: The Secrecy Proofs.
IJCAR 2001: 5-12 |
| 65 | | Giampaolo Bella,
Lawrence C. Paulson:
A Proof of Non-repudiation.
Security Protocols Workshop 2001: 119-125 |
| 64 | | Lawrence C. Paulson:
A Proof of Non-repudiation (Transcript of Discussion).
Security Protocols Workshop 2001: 126-133 |
| 63 | | Giampaolo Bella,
Lawrence C. Paulson:
Mechanical Proofs about a Non-repudiation Protocol.
TPHOLs 2001: 91-104 |
| 62 | | Lawrence C. Paulson:
Mechanizing a theory of program composition for UNITY.
ACM Trans. Program. Lang. Syst. 23(5): 626-656 (2001) |
| 61 | | Lawrence C. Paulson:
Relations Between Secrets: Two Formal Analyses of the Yahalom Protocol.
Journal of Computer Security 9(3): 197-216 (2001) |
| 60 | | Lawrence C. Paulson:
A Simple Formalization and Proof for the Mutilated Chess Board.
Logic Journal of the IGPL 9(3): (2001) |
| 2000 |
|---|
| 59 | | Giampaolo Bella,
Fabio Massacci,
Lawrence C. Paulson,
Piero Tramontano:
Formal Verification of Cardholder Registration in SET.
ESORICS 2000: 159-174 |
| 58 | | Lawrence C. Paulson:
A fixedpoint approach to (co)inductive and (co)datatype definitions.
Proof, Language, and Interaction 2000: 187-212 |
| 57 | | Giampaolo Bella,
Fabio Massacci,
Lawrence C. Paulson,
Piero Tramontano:
Making Sense of Specifications: The Formalization of SET.
Security Protocols Workshop 2000: 74-81 |
| 56 | | Lawrence C. Paulson:
Making Sense of Specifications: The Formalization of SET (Transcript of Discussion).
Security Protocols Workshop 2000: 82-86 |
| 55 | | Lawrence C. Paulson:
Mechanizing UNITY in Isabelle.
ACM Trans. Comput. Log. 1(1): 3-32 (2000) |
| 1999 |
|---|
| 54 | | Lawrence C. Paulson:
Proving Security Protocols Correct.
LICS 1999: 370-383 |
| 53 | | Lawrence C. Paulson:
Relatios Between Secrets: The Yahalom Protocol.
Security Protocols Workshop 1999: 73-84 |
| 52 | | Florian Kammüller,
Markus Wenzel,
Lawrence C. Paulson:
Locales - A Sectioning Concept for Isabelle.
TPHOLs 1999: 149-166 |
| 51 | | Lawrence C. Paulson:
Inductive Analysis of the Internet Protocol TLS.
ACM Trans. Inf. Syst. Secur. 2(3): 332-351 (1999) |
| 50 | | Leslie Lamport,
Lawrence C. Paulson:
Should your specification language be typed.
ACM Trans. Program. Lang. Syst. 21(3): 502-526 (1999) |
| 49 | | 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) |
| 48 | | Florian Kammüller,
Lawrence C. Paulson:
A Formal Proof of Sylow's Theorem.
J. Autom. Reasoning 23(3-4): 235-264 (1999) |
| 47 | | Lawrence C. Paulson:
A Generic Tableau Prover and its Integration with Isabelle.
J. UCS 5(3): 73-87 (1999) |
| 46 | | Lawrence C. Paulson:
Final coalgebras as greatest fixed points in ZF set theory.
Mathematical Structures in Computer Science 9(5): 545-567 (1999) |
| 1998 |
|---|
| 45 | | Clemens Ballarin,
Lawrence C. Paulson:
Reasoning About Coding Theory: The Benefits We Get from Computer Algebra.
AISC 1998: 55-66 |
| 44 | | 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 |
| 43 | | 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 |
| 42 | | Giampaolo Bella,
Lawrence C. Paulson:
Mechanising BAN Kerberos by the Inductive Method.
CAV 1998: 416-427 |
| 41 | | Giampaolo Bella,
Lawrence C. Paulson:
Kerberos Version 4: Inductive Analysis of the Secrecy Goals.
ESORICS 1998: 361-375 |
| 40 | | Lawrence C. Paulson:
Inductive Analysis of the Internet Protocol TLS (Position Paper).
Security Protocols Workshop 1998: 1-12 |
| 39 | | Lawrence C. Paulson:
Inductive Analysis of the Internet Protocol TLS (Transcript of Discussion).
Security Protocols Workshop 1998: 13-23 |
| 38 | | Lawrence C. Paulson:
The Inductive Approach to Verifying Cryptographic Protocols.
Journal of Computer Security 6(1-2): 85-128 (1998) |
| 1997 |
|---|
| 37 | | Lawrence C. Paulson:
Proving Properties of Security Protocols by Induction.
CSFW 1997: 70-83 |
| 36 | | Lawrence C. Paulson:
Mechanized proofs for a recursive authentication protocol.
CSFW 1997: 84-95 |
| 35 | | Lawrence C. Paulson:
Mechanizing Coinduction and Corecursion in Higher-order Logic
CoRR cs.LO/9711105: (1997) |
| 34 | | Lawrence C. Paulson:
Generic Automatic Proof Tools
CoRR cs.LO/9711106: (1997) |
| 33 | | Lawrence C. Paulson:
Mechanizing Coinduction and Corecursion in Higher-Order Logic.
J. Log. Comput. 7(2): 175-204 (1997) |
| 1996 |
|---|
| 32 | | Lawrence C. Paulson,
Krzysztof Grabczewski:
Mechanizing Set Theory: Cardinal Arithmetic and the Axiom of Choice.
CoRR cs.LO/9612104: (1996) |
| 31 | | Lawrence C. Paulson,
Krzysztof Grabczewski:
Mechanizing Set Theory.
J. Autom. Reasoning 17(3): 291-323 (1996) |
| 1995 |
|---|
| 30 | | Lawrence C. Paulson:
Set Theory for Verification. II: Induction and Recursion.
J. Autom. Reasoning 15(2): 167-215 (1995) |
| 1994 |
|---|
| 29 | | Lawrence C. Paulson:
Isabelle - A Generic Theorem Prover (with a contribution by T. Nipkow)
Springer 1994 |
| 28 | | Lawrence C. Paulson:
A Fixedpoint Approach to Implementing (Co)Inductive Definitions.
CADE 1994: 148-161 |
| 27 | | Lawrence C. Paulson:
A Concrete Final Coalgebra Theorem for ZF Set Theory.
TYPES 1994: 120-139 |
| 1993 |
|---|
| 26 | | Lawrence C. Paulson:
Verifying the Unification Algorithm in LCF
CoRR cs.LO/9301101: (1993) |
| 25 | | Lawrence C. Paulson:
Constructing Recursion Operators in Intuitionistic Type Theory
CoRR cs.LO/9301102: (1993) |
| 24 | | Lawrence C. Paulson:
Proving Termination of Normalization Functions for Conditional Expressions
CoRR cs.LO/9301103: (1993) |
| 23 | | Lawrence C. Paulson:
Natural Deduction as Higher-Order Resolution
CoRR cs.LO/9301104: (1993) |
| 22 | | Lawrence C. Paulson:
The Foundation of a Generic Theorem Prover
CoRR cs.LO/9301105: (1993) |
| 21 | | Lawrence C. Paulson:
Isabelle: The Next 700 Theorem Provers
CoRR cs.LO/9301106: (1993) |
| 20 | | Lawrence C. Paulson:
A Formulation of the Simple Theory of Types (for Isabelle)
CoRR cs.LO/9301107: (1993) |
| 19 | | Lawrence C. Paulson:
A Higher-Order Implementation of Rewriting
CoRR cs.LO/9301108: (1993) |
| 18 | | Lawrence C. Paulson,
Andrew W. Smith:
Logic Programming, Functional Programming, and Inductive Definitions
CoRR cs.LO/9301109: (1993) |
| 17 | | Lawrence C. Paulson:
Designing a Theorem Prover
CoRR cs.LO/9301110: (1993) |
| 16 | | Lawrence C. Paulson:
Set Theory for Verification: I. From Foundations to Functions
CoRR cs.LO/9311103: (1993) |
| 15 | | Lawrence C. Paulson:
Set Theory for Verification: I. From Foundations to Functions.
J. Autom. Reasoning 11(3): 353-389 (1993) |
| 1992 |
|---|
| 14 | | Tobias Nipkow,
Lawrence C. Paulson:
Isabelle-91.
CADE 1992: 673-676 |
| 1989 |
|---|
| 13 | | Lawrence C. Paulson,
Andrew W. Smith:
Logic Programming, Functional Programming, and Inductive Definitions.
ELP 1989: 283-309 |
| 12 | | Lawrence C. Paulson:
The Foundation of a Generic Theorem Prover.
J. Autom. Reasoning 5(3): 363-397 (1989) |
| 1988 |
|---|
| 11 | | Lawrence C. Paulson:
Isabelle: The Next Seven Hundred Theorem Provers.
CADE 1988: 772-773 |
| 10 | | Lawrence C. Paulson:
A formulation of the simple theory of types (for Isabelle).
Conference on Computer Logic 1988: 246-274 |
| 1986 |
|---|
| 9 | | Lawrence C. Paulson:
Proving Termination of Normalization Functions for Conditional Experessions.
J. Autom. Reasoning 2(1): 63-74 (1986) |
| 8 | | Lawrence C. Paulson:
Natural Deduction as Higher-Order Resolution.
J. Log. Program. 3(3): 237-258 (1986) |
| 7 | | Lawrence C. Paulson:
Constructing Recursion Operators in Intuitionistic Type Theory.
J. Symb. Comput. 2(4): 325-355 (1986) |
| 1985 |
|---|
| 6 | | Lawrence C. Paulson:
Lessons Learned from LCF: A Survey of Natural Deduction Proofs.
Comput. J. 28(5): 474-479 (1985) |
| 5 | | Lawrence C. Paulson:
Verifying the Unification Algorithm in LCF.
Sci. Comput. Program. 5(2): 143-169 (1985) |
| 1984 |
|---|
| 4 | | Lawrence C. Paulson:
Deriving Structural Induction in LCF.
Semantics of Data Types 1984: 197-214 |
| 1983 |
|---|
| 3 | | Lawrence C. Paulson:
Compiler Generation from Denotational Semantics.
Method and tools for compiler construction 1983: 219-252 |
| 2 | | Lawrence C. Paulson:
A Higher-Order Implementation of Rewriting.
Sci. Comput. Program. 3(2): 119-149 (1983) |
| 1982 |
|---|
| 1 | | Lawrence C. Paulson:
A Semantics-Directed Compiler Generator.
POPL 1982: 224-233 |
