The SCEAS System
Navigation Menu
Introduction
Collection Based
Clustering
Ranking
Paper Based
Journals
Conferences
DB Status
Statistics
Search

Search the dblp DataBase

Title:
Author:
Lawrence C. Paulson: [Publications] [Author Rank by year] [Co-authors] [Prefers] [Cites] [Cited by]

Publications of Author

  1. Lawrence C. Paulson
    The Foundation of a Generic Theorem Prover. [Citation Graph (1, 0)][DBLP]
    J. Autom. Reasoning, 1989, v:5, n:3, pp:363-397 [Journal]
  2. Lawrence C. Paulson
    Compiler Generation from Denotational Semantics. [Citation Graph (0, 0)][DBLP]
    Method and tools for compiler construction, 1983, pp:219-252 [Conf]
  3. Jacques D. Fleuriot, Lawrence C. Paulson
    Proving Newton's Propositio Kepleriana Using Geometry and Nonstandard Analysis in Isabelle. [Citation Graph (0, 0)][DBLP]
    Automated Deduction in Geometry, 1998, pp:47-66 [Conf]
  4. Clemens Ballarin, Lawrence C. Paulson
    Reasoning About Coding Theory: The Benefits We Get from Computer Algebra. [Citation Graph (0, 0)][DBLP]
    AISC, 1998, pp:55-66 [Conf]
  5. Jacques D. Fleuriot, Lawrence C. Paulson
    A Combination of Nonstandard Analysis and Geometry Theorem Proving, with Application to Newton's Principia. [Citation Graph (0, 0)][DBLP]
    CADE, 1998, pp:3-16 [Conf]
  6. Jia Meng, Lawrence C. Paulson
    Experiments on Supporting Interactive Proof Using Resolution. [Citation Graph (0, 0)][DBLP]
    IJCAR, 2004, pp:372-384 [Conf]
  7. Tobias Nipkow, Lawrence C. Paulson
    Isabelle-91. [Citation Graph (0, 0)][DBLP]
    CADE, 1992, pp:673-676 [Conf]
  8. Lawrence C. Paulson
    SET Cardholder Registration: The Secrecy Proofs. [Citation Graph (0, 0)][DBLP]
    IJCAR, 2001, pp:5-12 [Conf]
  9. Lawrence C. Paulson
    The Reflection Theorem: A Study in Meta-theoretic Reasoning. [Citation Graph (0, 0)][DBLP]
    CADE, 2002, pp:377-391 [Conf]
  10. Lawrence C. Paulson
    Isabelle: The Next Seven Hundred Theorem Provers. [Citation Graph (0, 0)][DBLP]
    CADE, 1988, pp:772-773 [Conf]
  11. Lawrence C. Paulson
    A Fixedpoint Approach to Implementing (Co)Inductive Definitions. [Citation Graph (0, 0)][DBLP]
    CADE, 1994, pp:148-161 [Conf]
  12. Giampaolo Bella, Lawrence C. Paulson
    Mechanising BAN Kerberos by the Inductive Method. [Citation Graph (0, 0)][DBLP]
    CAV, 1998, pp:416-427 [Conf]
  13. Giampaolo Bella, Lawrence C. Paulson, Fabio Massacci
    The verification of an industrial payment protocol: the SET purchase phase. [Citation Graph (0, 0)][DBLP]
    ACM Conference on Computer and Communications Security, 2002, pp:12-20 [Conf]
  14. Lawrence C. Paulson
    A formulation of the simple theory of types (for Isabelle). [Citation Graph (0, 0)][DBLP]
    Conference on Computer Logic, 1988, pp:246-274 [Conf]
  15. Lawrence C. Paulson
    Proving Properties of Security Protocols by Induction. [Citation Graph (0, 0)][DBLP]
    CSFW, 1997, pp:70-83 [Conf]
  16. Lawrence C. Paulson
    Mechanized proofs for a recursive authentication protocol. [Citation Graph (0, 0)][DBLP]
    CSFW, 1997, pp:84-95 [Conf]
  17. Lawrence C. Paulson, Andrew W. Smith
    Logic Programming, Functional Programming, and Inductive Definitions. [Citation Graph (0, 0)][DBLP]
    ELP, 1989, pp:283-309 [Conf]
  18. Giampaolo Bella, Fabio Massacci, Lawrence C. Paulson, Piero Tramontano
    Formal Verification of Cardholder Registration in SET. [Citation Graph (0, 0)][DBLP]
    ESORICS, 2000, pp:159-174 [Conf]
  19. Giampaolo Bella, Lawrence C. Paulson
    Kerberos Version 4: Inductive Analysis of the Secrecy Goals. [Citation Graph (0, 0)][DBLP]
    ESORICS, 1998, pp:361-375 [Conf]
  20. Lawrence C. Paulson
    Verifying the SET Protocol: Overview. [Citation Graph (0, 0)][DBLP]
    FASec, 2002, pp:4-14 [Conf]
  21. Sidi O. Ehmety, Lawrence C. Paulson
    Program Composition in Isabelle/UNITY. [Citation Graph (0, 0)][DBLP]
    IPDPS, 2002, pp:- [Conf]
  22. Lawrence C. Paulson
    Proving Security Protocols Correct. [Citation Graph (0, 0)][DBLP]
    LICS, 1999, pp:370-383 [Conf]
  23. Lawrence C. Paulson
    A Semantics-Directed Compiler Generator. [Citation Graph (0, 0)][DBLP]
    POPL, 1982, pp:224-233 [Conf]
  24. Lawrence C. Paulson
    Deriving Structural Induction in LCF. [Citation Graph (0, 0)][DBLP]
    Semantics of Data Types, 1984, pp:197-214 [Conf]
  25. Giampaolo Bella, Cristiano Longo, Lawrence C. Paulson
    Is the Verification Problem for Cryptographic Protocols Solved?. [Citation Graph (0, 0)][DBLP]
    Security Protocols Workshop, 2003, pp:183-189 [Conf]
  26. Giampaolo Bella, Fabio Massacci, Lawrence C. Paulson, Piero Tramontano
    Making Sense of Specifications: The Formalization of SET. [Citation Graph (0, 0)][DBLP]
    Security Protocols Workshop, 2000, pp:74-81 [Conf]
  27. Giampaolo Bella, Lawrence C. Paulson
    A Proof of Non-repudiation. [Citation Graph (0, 0)][DBLP]
    Security Protocols Workshop, 2001, pp:119-125 [Conf]
  28. Giampaolo Bella, Lawrence C. Paulson
    Analyzing Delegation Properties. [Citation Graph (0, 0)][DBLP]
    Security Protocols Workshop, 2002, pp:120-127 [Conf]
  29. Lawrence C. Paulson
    Making Sense of Specifications: The Formalization of SET (Transcript of Discussion). [Citation Graph (0, 0)][DBLP]
    Security Protocols Workshop, 2000, pp:82-86 [Conf]
  30. Lawrence C. Paulson
    A Proof of Non-repudiation (Transcript of Discussion). [Citation Graph (0, 0)][DBLP]
    Security Protocols Workshop, 2001, pp:126-133 [Conf]
  31. Lawrence C. Paulson
    Inductive Analysis of the Internet Protocol TLS (Position Paper). [Citation Graph (0, 0)][DBLP]
    Security Protocols Workshop, 1998, pp:1-12 [Conf]
  32. Lawrence C. Paulson
    Inductive Analysis of the Internet Protocol TLS (Transcript of Discussion). [Citation Graph (0, 0)][DBLP]
    Security Protocols Workshop, 1998, pp:13-23 [Conf]
  33. Lawrence C. Paulson
    Relatios Between Secrets: The Yahalom Protocol. [Citation Graph (0, 0)][DBLP]
    Security Protocols Workshop, 1999, pp:73-84 [Conf]
  34. Giampaolo Bella, Lawrence C. Paulson
    Mechanical Proofs about a Non-repudiation Protocol. [Citation Graph (0, 0)][DBLP]
    TPHOLs, 2001, pp:91-104 [Conf]
  35. Giampaolo Bella, Cristiano Longo, Lawrence C. Paulson
    Verifying Second-Level Security Protocols. [Citation Graph (0, 0)][DBLP]
    TPHOLs, 2003, pp:352-366 [Conf]
  36. Florian Kammüller, Markus Wenzel, Lawrence C. Paulson
    Locales - A Sectioning Concept for Isabelle. [Citation Graph (0, 0)][DBLP]
    TPHOLs, 1999, pp:149-166 [Conf]
  37. Tobias Nipkow, Lawrence C. Paulson
    Proof Pearl: Defining Functions over Finite Sets. [Citation Graph (0, 0)][DBLP]
    TPHOLs, 2005, pp:385-396 [Conf]
  38. Markus Wenzel, Larry Paulson
    Isabelle/Isar. [Citation Graph (0, 0)][DBLP]
    The Seventeen Provers of the World, 2006, pp:41-49 [Conf]
  39. Lawrence C. Paulson
    A Concrete Final Coalgebra Theorem for ZF Set Theory. [Citation Graph (0, 0)][DBLP]
    TYPES, 1994, pp:120-139 [Conf]
  40. Lawrence C. Paulson
    Lessons Learned from LCF: A Survey of Natural Deduction Proofs. [Citation Graph (0, 0)][DBLP]
    Comput. J., 1985, v:28, n:5, pp:474-479 [Journal]
  41. Lawrence C. Paulson
    Verifying the Unification Algorithm in LCF [Citation Graph (0, 0)][DBLP]
    CoRR, 1993, v:0, n:, pp:- [Journal]
  42. Lawrence C. Paulson
    Constructing Recursion Operators in Intuitionistic Type Theory [Citation Graph (0, 0)][DBLP]
    CoRR, 1993, v:0, n:, pp:- [Journal]
  43. Lawrence C. Paulson
    Proving Termination of Normalization Functions for Conditional Expressions [Citation Graph (0, 0)][DBLP]
    CoRR, 1993, v:0, n:, pp:- [Journal]
  44. Lawrence C. Paulson
    Natural Deduction as Higher-Order Resolution [Citation Graph (0, 0)][DBLP]
    CoRR, 1993, v:0, n:, pp:- [Journal]
  45. Lawrence C. Paulson
    The Foundation of a Generic Theorem Prover [Citation Graph (0, 0)][DBLP]
    CoRR, 1993, v:0, n:, pp:- [Journal]
  46. Lawrence C. Paulson
    Isabelle: The Next 700 Theorem Provers [Citation Graph (0, 0)][DBLP]
    CoRR, 1993, v:0, n:, pp:- [Journal]
  47. Lawrence C. Paulson
    A Formulation of the Simple Theory of Types (for Isabelle) [Citation Graph (0, 0)][DBLP]
    CoRR, 1993, v:0, n:, pp:- [Journal]
  48. Lawrence C. Paulson
    A Higher-Order Implementation of Rewriting [Citation Graph (0, 0)][DBLP]
    CoRR, 1993, v:0, n:, pp:- [Journal]
  49. Lawrence C. Paulson, Andrew W. Smith
    Logic Programming, Functional Programming, and Inductive Definitions [Citation Graph (0, 0)][DBLP]
    CoRR, 1993, v:0, n:, pp:- [Journal]
  50. Lawrence C. Paulson
    Designing a Theorem Prover [Citation Graph (0, 0)][DBLP]
    CoRR, 1993, v:0, n:, pp:- [Journal]
  51. Lawrence C. Paulson
    Set Theory for Verification: I. From Foundations to Functions [Citation Graph (0, 0)][DBLP]
    CoRR, 1993, v:0, n:, pp:- [Journal]
  52. Lawrence C. Paulson, Krzysztof Grabczewski
    Mechanizing Set Theory: Cardinal Arithmetic and the Axiom of Choice. [Citation Graph (0, 0)][DBLP]
    CoRR, 1996, v:0, n:, pp:- [Journal]
  53. Lawrence C. Paulson
    Mechanizing Coinduction and Corecursion in Higher-order Logic [Citation Graph (0, 0)][DBLP]
    CoRR, 1997, v:0, n:, pp:- [Journal]
  54. Lawrence C. Paulson
    Generic Automatic Proof Tools [Citation Graph (0, 0)][DBLP]
    CoRR, 1997, v:0, n:, pp:- [Journal]
  55. Sidi O. Ehmety, Lawrence C. Paulson
    Mechanizing compositional reasoning for concurrent systems: some lessons. [Citation Graph (0, 0)][DBLP]
    Formal Asp. Comput., 2005, v:17, n:1, pp:58-68 [Journal]
  56. Clemens Ballarin, Lawrence C. Paulson
    A Pragmatic Approach to Extending Provers by Computer Algebra - with Applications to Coding Theory. [Citation Graph (0, 0)][DBLP]
    Fundam. Inform., 1999, v:39, n:1-2, pp:1-20 [Journal]
  57. Jia Meng, Claire Quigley, Lawrence C. Paulson
    Automation for interactive proof: First prototype. [Citation Graph (0, 0)][DBLP]
    Inf. Comput., 2006, v:204, n:10, pp:1575-1596 [Journal]
  58. Jia Meng, Claire Quigley, Lawrence C. Paulson
    Erratum to "Automation for interactive proof: First prototype" [Inform. and Comput. 204(2006) 1575-1596]. [Citation Graph (0, 0)][DBLP]
    Inf. Comput., 2006, v:204, n:12, pp:1852- [Journal]
  59. Lawrence C. Paulson
    A Simple Formalization and Proof for the Mutilated Chess Board. [Citation Graph (0, 0)][DBLP]
    Logic Journal of the IGPL, 2001, v:9, n:3, pp:- [Journal]
  60. Giampaolo Bella, Fabio Massacci, Lawrence C. Paulson
    An overview of the verification of SET. [Citation Graph (0, 0)][DBLP]
    Int. J. Inf. Sec., 2005, v:4, n:1-2, pp:17-28 [Journal]
  61. Florian Kammüller, Lawrence C. Paulson
    A Formal Proof of Sylow's Theorem. [Citation Graph (0, 0)][DBLP]
    J. Autom. Reasoning, 1999, v:23, n:3-4, pp:235-264 [Journal]
  62. Lawrence C. Paulson
    Organizing Numerical Theories Using Axiomatic Type Classes. [Citation Graph (0, 0)][DBLP]
    J. Autom. Reasoning, 2004, v:33, n:1, pp:29-49 [Journal]
  63. Lawrence C. Paulson
    Proving Termination of Normalization Functions for Conditional Experessions. [Citation Graph (0, 0)][DBLP]
    J. Autom. Reasoning, 1986, v:2, n:1, pp:63-74 [Journal]
  64. Lawrence C. Paulson
    Set Theory for Verification: I. From Foundations to Functions. [Citation Graph (0, 0)][DBLP]
    J. Autom. Reasoning, 1993, v:11, n:3, pp:353-389 [Journal]
  65. Lawrence C. Paulson
    Set Theory for Verification. II: Induction and Recursion. [Citation Graph (0, 0)][DBLP]
    J. Autom. Reasoning, 1995, v:15, n:2, pp:167-215 [Journal]
  66. Lawrence C. Paulson, Krzysztof Grabczewski
    Mechanizing Set Theory. [Citation Graph (0, 0)][DBLP]
    J. Autom. Reasoning, 1996, v:17, n:3, pp:291-323 [Journal]
  67. Giampaolo Bella, Fabio Massacci, Lawrence C. Paulson
    Verifying the SET Purchase Protocols. [Citation Graph (0, 0)][DBLP]
    J. Autom. Reasoning, 2006, v:36, n:1-2, pp:5-37 [Journal]
  68. Lawrence C. Paulson
    Relations Between Secrets: Two Formal Analyses of the Yahalom Protocol. [Citation Graph (0, 0)][DBLP]
    Journal of Computer Security, 2001, v:9, n:3, pp:197-216 [Journal]
  69. Lawrence C. Paulson
    The Inductive Approach to Verifying Cryptographic Protocols. [Citation Graph (0, 0)][DBLP]
    Journal of Computer Security, 1998, v:6, n:1-2, pp:85-128 [Journal]
  70. Lawrence C. Paulson
    Natural Deduction as Higher-Order Resolution. [Citation Graph (0, 0)][DBLP]
    J. Log. Program., 1986, v:3, n:3, pp:237-258 [Journal]
  71. Lawrence C. Paulson
    Constructing Recursion Operators in Intuitionistic Type Theory. [Citation Graph (0, 0)][DBLP]
    J. Symb. Comput., 1986, v:2, n:4, pp:325-355 [Journal]
  72. Lawrence C. Paulson
    A Generic Tableau Prover and its Integration with Isabelle. [Citation Graph (0, 0)][DBLP]
    J. UCS, 1999, v:5, n:3, pp:73-87 [Journal]
  73. Lawrence C. Paulson
    Mechanizing Coinduction and Corecursion in Higher-Order Logic. [Citation Graph (0, 0)][DBLP]
    J. Log. Comput., 1997, v:7, n:2, pp:175-204 [Journal]
  74. Lawrence C. Paulson
    Final coalgebras as greatest fixed points in ZF set theory. [Citation Graph (0, 0)][DBLP]
    Mathematical Structures in Computer Science, 1999, v:9, n:5, pp:545-567 [Journal]
  75. Lawrence C. Paulson
    A Higher-Order Implementation of Rewriting. [Citation Graph (0, 0)][DBLP]
    Sci. Comput. Program., 1983, v:3, n:2, pp:119-149 [Journal]
  76. Lawrence C. Paulson
    Verifying the Unification Algorithm in LCF. [Citation Graph (0, 0)][DBLP]
    Sci. Comput. Program., 1985, v:5, n:2, pp:143-169 [Journal]
  77. Lawrence C. Paulson
    Inductive Analysis of the Internet Protocol TLS. [Citation Graph (0, 0)][DBLP]
    ACM Trans. Inf. Syst. Secur., 1999, v:2, n:3, pp:332-351 [Journal]
  78. Giampaolo Bella, Lawrence C. Paulson
    Accountability protocols: Formalized and verified. [Citation Graph (0, 0)][DBLP]
    ACM Trans. Inf. Syst. Secur., 2006, v:9, n:2, pp:138-161 [Journal]
  79. Lawrence C. Paulson
    Mechanizing UNITY in Isabelle. [Citation Graph (0, 0)][DBLP]
    ACM Trans. Comput. Log., 2000, v:1, n:1, pp:3-32 [Journal]
  80. Lawrence C. Paulson
    Defining functions on equivalence classes. [Citation Graph (0, 0)][DBLP]
    ACM Trans. Comput. Log., 2006, v:7, n:4, pp:658-675 [Journal]
  81. Leslie Lamport, Lawrence C. Paulson
    Should your specification language be typed. [Citation Graph (0, 0)][DBLP]
    ACM Trans. Program. Lang. Syst., 1999, v:21, n:3, pp:502-526 [Journal]
  82. Lawrence C. Paulson
    Mechanizing a theory of program composition for UNITY. [Citation Graph (0, 0)][DBLP]
    ACM Trans. Program. Lang. Syst., 2001, v:23, n:5, pp:626-656 [Journal]
  83. Behzad Akbarpour, Lawrence C. Paulson
    Extending a Resolution Prover for Inequalities on Elementary Functions. [Citation Graph (0, 0)][DBLP]
    LPAR, 2007, pp:47-61 [Conf]
  84. Lawrence C. Paulson, Kong Woei Susanto
    Source-Level Proof Reconstruction for Interactive Theorem Proving. [Citation Graph (0, 0)][DBLP]
    TPHOLs, 2007, pp:232-245 [Conf]
  85. Bernhard Beckert, Lawrence C. Paulson
    Preface. [Citation Graph (0, 0)][DBLP]
    J. Autom. Reasoning, 2007, v:38, n:1-3, pp:1-2 [Journal]

  86. MetiTarski: An Automatic Prover for the Elementary Functions. [Citation Graph (, )][DBLP]


  87. A fixedpoint approach to (co)inductive and (co)datatype definitions. [Citation Graph (, )][DBLP]


  88. A Termination Checker for Isabelle Hoare Logic. [Citation Graph (, )][DBLP]


  89. LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description). [Citation Graph (, )][DBLP]


  90. The Relative Consistency of the Axiom of Choice - Mechanized Using Isabelle/ZF. [Citation Graph (, )][DBLP]


  91. Formal verification of analog circuits in the presence of noise and process variation. [Citation Graph (, )][DBLP]


  92. Formal verification of analog designs using MetiTarski. [Citation Graph (, )][DBLP]


  93. Applications of MetiTarski in the Verification of Control and Hybrid Systems. [Citation Graph (, )][DBLP]


  94. The Isabelle Framework. [Citation Graph (, )][DBLP]


  95. Quantified Multimodal Logics in Simple Type Theory [Citation Graph (, )][DBLP]


Search in 0.005secs, Finished in 0.462secs
NOTICE1
System may not be available sometimes or not working properly, since it is still in development with continuous upgrades
NOTICE2
The rankings that are presented on this page should NOT be considered as formal since the citation info is incomplete in DBLP
 
Introduction Collection Based Clustering Ranking Paper Based Journals Conferences DB Status Statistics Search
System created by asidirop@csd.auth.gr [http://users.auth.gr/~asidirop/] © 2002
for Data Engineering Laboratory, Department of Informatics, Aristotle University © 2002