| Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
| 1 | Jasmin Christian Blanchette, Sascha Böhme, Lawrence C. Paulson |
Extending Sledgehammer with SMT Solvers.  |
CADE  |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Christoph Benzmüller, Lawrence C. Paulson |
Multimodal and intuitionistic logics in simple type theory. |
Logic Journal of the IGPL |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Behzad Akbarpour, Lawrence C. Paulson |
MetiTarski: An Automatic Theorem Prover for Real-Valued Special Functions. |
J. Autom. Reasoning |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Lawrence C. Paulson |
Functional Programming in ML. |
Encyclopedia of Software Engineering |
2010 |
DBLP BibTeX RDF |
|
| 1 | Matt Kaufmann, Lawrence C. Paulson (eds.) |
Interactive Theorem Proving, First International Conference, ITP 2010, Edinburgh, UK, July 11-14, 2010. Proceedings |
ITP |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | 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 |
DBLP BibTeX RDF |
|
| 1 | Jia Meng, Lawrence C. Paulson |
Lightweight relevance filtering for machine-generated resolution problems. |
J. Applied Logic |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Christoph Benzmüller, Lawrence C. Paulson |
Quantified Multimodal Logics in Simple Type Theory |
CoRR |
2009 |
DBLP BibTeX RDF |
|
| 1 | William Denman, Behzad Akbarpour, Sofiène Tahar, Mohamed H. Zaki, Lawrence C. Paulson |
Formal verification of analog designs using MetiTarski. |
FMCAD |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Behzad Akbarpour, Lawrence C. Paulson |
Applications of MetiTarski in the Verification of Control and Hybrid Systems. |
HSCC |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Tobias Nipkow, Lawrence C. Paulson |
Fun With Tilings. |
Archive of Formal Proofs |
2008 |
DBLP BibTeX RDF |
|
| 1 | Jia Meng, Lawrence C. Paulson |
Translating Higher-Order Clauses to First-Order Clauses. |
J. Autom. Reasoning |
2008 |
DBLP DOI BibTeX RDF |
Interactive theorem provers, Clause translation, First-order logic, Higher-order logic |
| 1 | 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 |
DBLP DOI BibTeX RDF |
|
| 1 | Makarius Wenzel, Lawrence C. Paulson, Tobias Nipkow |
The Isabelle Framework. |
TPHOLs |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Behzad Akbarpour, Lawrence C. Paulson |
MetiTarski: An Automatic Prover for the Elementary Functions. |
AISC/MKM/Calculemus |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Lawrence C. Paulson |
The Relative Consistency of the Axiom of Choice - Mechanized Using Isabelle/ZF. |
CiE |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Bernhard Beckert, Lawrence C. Paulson |
Preface. |
J. Autom. Reasoning |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Jia Meng, Lawrence C. Paulson, Gerwin Klein |
A Termination Checker for Isabelle Hoare Logic. |
VERIFY |
2007 |
DBLP BibTeX RDF |
|
| 1 | Behzad Akbarpour, Lawrence C. Paulson |
Extending a Resolution Prover for Inequalities on Elementary Functions. |
LPAR |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Lawrence C. Paulson, Kong Woei Susanto |
Source-Level Proof Reconstruction for Interactive Theorem Proving. |
TPHOLs |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Jia Meng, Claire Quigley, Lawrence C. Paulson |
Erratum to "Automation for interactive proof: First prototype" [Inform. and Comput. 204(2006) 1575-1596]. |
Inf. Comput. |
2006 |
DBLP DOI BibTeX RDF |
|
| 1 | Jia Meng, Claire Quigley, Lawrence C. Paulson |
Automation for interactive proof: First prototype. |
Inf. Comput. |
2006 |
DBLP DOI BibTeX RDF |
|
| 1 | Giampaolo Bella, Fabio Massacci, Lawrence C. Paulson |
Verifying the SET Purchase Protocols. |
J. Autom. Reasoning |
2006 |
DBLP DOI BibTeX RDF |
deductive verification, electronic commerce, security protocols, Isabelle, inductive definitions |
| 1 | Giampaolo Bella, Lawrence C. Paulson |
Accountability protocols: Formalized and verified. |
ACM Trans. Inf. Syst. Secur. |
2006 |
DBLP DOI BibTeX RDF |
inductive method, proof tools, Isabelle, Nonrepudiation, certified email |
| 1 | Lawrence C. Paulson |
Defining functions on equivalence classes. |
ACM Trans. Comput. Log. |
2006 |
DBLP DOI BibTeX RDF |
theorem proving, Equivalence classes, quotients |
| 1 | Markus Wenzel, Lawrence C. Paulson |
Isabelle/Isar. |
The Seventeen Provers of the World |
2006 |
DBLP DOI BibTeX RDF |
|
| 1 | Giampaolo Bella, Fabio Massacci, Lawrence C. Paulson |
An overview of the verification of SET. |
Int. J. Inf. Sec. |
2005 |
DBLP DOI BibTeX RDF |
Secure Electronic Transactions (SET), Formal verification, Computer security, Network protocols, Automated reasoning |
| 1 | Sidi O. Ehmety, Lawrence C. Paulson |
Mechanizing compositional reasoning for concurrent systems: some lessons. |
Formal Asp. Comput. |
2005 |
DBLP DOI BibTeX RDF |
Existential properties, Universal properties, Guarantees assertions, UNITY, Isabelle, Compositional reasoning |
| 1 | Tobias Nipkow, Lawrence C. Paulson |
Proof Pearl: Defining Functions over Finite Sets. |
TPHOLs |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Lawrence C. Paulson |
Organizing Numerical Theories Using Axiomatic Type Classes. |
J. Autom. Reasoning |
2004 |
DBLP DOI BibTeX RDF |
axiomatic type classes, polymorphism, arithmetic, overloading, Isabelle |
| 1 | Jia Meng, Lawrence C. Paulson |
Experiments on Supporting Interactive Proof Using Resolution. |
IJCAR |
2004 |
DBLP DOI BibTeX RDF |
|
| 1 | Giampaolo Bella, Fabio Massacci, Lawrence C. Paulson |
Verifying the SET registration protocols. |
IEEE Journal on Selected Areas in Communications |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | Giampaolo Bella, Cristiano Longo, Lawrence C. Paulson |
Is the Verification Problem for Cryptographic Protocols Solved?. |
Security Protocols Workshop |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | Giampaolo Bella, Cristiano Longo, Lawrence C. Paulson |
Verifying Second-Level Security Protocols. |
TPHOLs |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | Tobias Nipkow, Lawrence C. Paulson, Markus Wenzel |
Isabelle/HOL - A Proof Assistant for Higher-Order Logic |
|
2002 |
DOI RDF |
|
| 1 | Lawrence C. Paulson |
The Reflection Theorem: A Study in Meta-theoretic Reasoning. |
CADE |
2002 |
DBLP DOI BibTeX RDF |
|
| 1 | Sidi O. Ehmety, Lawrence C. Paulson |
Program Composition in Isabelle/UNITY. (PDF / PS) |
IPDPS |
2002 |
DBLP DOI BibTeX RDF |
program composition, universal and existential properties, UNITY, Isabelle |
| 1 | Lawrence C. Paulson |
Verifying the SET Protocol: Overview. |
FASec |
2002 |
DBLP DOI BibTeX RDF |
|
| 1 | Giampaolo Bella, Lawrence C. Paulson |
Analyzing Delegation Properties. |
Security Protocols Workshop |
2002 |
DBLP DOI BibTeX RDF |
|
| 1 | 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 |
DBLP DOI BibTeX RDF |
inductive specifications, isabelle proof assistant, formal verification, electronic commerce, security protocols |
| 1 | Lawrence C. Paulson |
Relations Between Secrets: Two Formal Analyses of the Yahalom Protocol. |
Journal of Computer Security |
2001 |
DBLP BibTeX RDF |
|
| 1 | Lawrence C. Paulson |
A Simple Formalization and Proof for the Mutilated Chess Board. |
Logic Journal of the IGPL |
2001 |
DBLP DOI BibTeX RDF |
|
| 1 | Lawrence C. Paulson |
Mechanizing a theory of program composition for UNITY. |
ACM Trans. Program. Lang. Syst. |
2001 |
DBLP DOI BibTeX RDF |
concurrency, UNITY, Isabelle, compositional reasoning |
| 1 | Lawrence C. Paulson |
SET Cardholder Registration: The Secrecy Proofs. |
IJCAR |
2001 |
DBLP DOI BibTeX RDF |
|
| 1 | Giampaolo Bella, Lawrence C. Paulson |
A Proof of Non-repudiation. |
Security Protocols Workshop |
2001 |
DBLP DOI BibTeX RDF |
|
| 1 | Lawrence C. Paulson |
A Proof of Non-repudiation (Transcript of Discussion). |
Security Protocols Workshop |
2001 |
DBLP DOI BibTeX RDF |
|
| 1 | Giampaolo Bella, Lawrence C. Paulson |
Mechanical Proofs about a Non-repudiation Protocol. |
TPHOLs |
2001 |
DBLP DOI BibTeX RDF |
|
| 1 | Lawrence C. Paulson |
Mechanizing UNITY in Isabelle. |
ACM Trans. Comput. Log. |
2000 |
DBLP DOI BibTeX RDF |
concurrency, UNITY, Isabelle, compositional reasoning |
| 1 | Giampaolo Bella, Fabio Massacci, Lawrence C. Paulson, Piero Tramontano |
Making Sense of Specifications: The Formalization of SET. |
Security Protocols Workshop |
2000 |
DBLP DOI BibTeX RDF |
|
| 1 | Lawrence C. Paulson |
Making Sense of Specifications: The Formalization of SET (Transcript of Discussion). |
Security Protocols Workshop |
2000 |
DBLP DOI BibTeX RDF |
|
| 1 | Lawrence C. Paulson |
A fixedpoint approach to (co)inductive and (co)datatype definitions. |
Proof, Language, and Interaction |
2000 |
DBLP BibTeX RDF |
|
| 1 | Giampaolo Bella, Fabio Massacci, Lawrence C. Paulson, Piero Tramontano |
Formal Verification of Cardholder Registration in SET. |
ESORICS |
2000 |
DBLP DOI BibTeX RDF |
|
| 1 | Lawrence C. Paulson |
Final coalgebras as greatest fixed points in ZF set theory. |
Mathematical Structures in Computer Science |
1999 |
DBLP BibTeX RDF |
|
| 1 | Lawrence C. Paulson |
A Generic Tableau Prover and its Integration with Isabelle. |
J. UCS |
1999 |
DBLP BibTeX RDF |
|
| 1 | Leslie Lamport, Lawrence C. Paulson |
Should your specification language be typed. |
ACM Trans. Program. Lang. Syst. |
1999 |
DBLP DOI BibTeX RDF |
specification, types, set theory |
| 1 | Clemens Ballarin, Lawrence C. Paulson |
A Pragmatic Approach to Extending Provers by Computer Algebra - with Applications to Coding Theory. |
Fundam. Inform. |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | Florian Kammüller, Lawrence C. Paulson |
A Formal Proof of Sylow's Theorem. |
J. Autom. Reasoning |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | Lawrence C. Paulson |
Inductive Analysis of the Internet Protocol TLS. |
ACM Trans. Inf. Syst. Secur. |
1999 |
DBLP DOI BibTeX RDF |
inductive method, proof tools, authentication, TLS, Isabelle |
| 1 | Lawrence C. Paulson |
Relatios Between Secrets: The Yahalom Protocol. |
Security Protocols Workshop |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | Florian Kammüller, Markus Wenzel, Lawrence C. Paulson |
Locales - A Sectioning Concept for Isabelle. |
TPHOLs |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | Lawrence C. Paulson |
Proving Security Protocols Correct. |
LICS |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | Lawrence C. Paulson |
The Inductive Approach to Verifying Cryptographic Protocols. |
Journal of Computer Security |
1998 |
DBLP BibTeX RDF |
|
| 1 | Jacques D. Fleuriot, Lawrence C. Paulson |
A Combination of Nonstandard Analysis and Geometry Theorem Proving, with Application to Newton's Principia. |
CADE |
1998 |
DBLP BibTeX RDF |
|
| 1 | Jacques D. Fleuriot, Lawrence C. Paulson |
Proving Newton's Propositio Kepleriana Using Geometry and Nonstandard Analysis in Isabelle. |
Automated Deduction in Geometry |
1998 |
DBLP DOI BibTeX RDF |
|
| 1 | Lawrence C. Paulson |
Inductive Analysis of the Internet Protocol TLS (Position Paper). |
Security Protocols Workshop |
1998 |
DBLP DOI BibTeX RDF |
|
| 1 | Lawrence C. Paulson |
Inductive Analysis of the Internet Protocol TLS (Transcript of Discussion). |
Security Protocols Workshop |
1998 |
DBLP DOI BibTeX RDF |
|
| 1 | Clemens Ballarin, Lawrence C. Paulson |
Reasoning About Coding Theory: The Benefits We Get from Computer Algebra. |
AISC |
1998 |
DBLP DOI BibTeX RDF |
mechanised reasoning, combining systems, soundness of computer algebra systems, specialisation problem, AISC topics, Integration of logical reasoning and computer algebra, Computer algebra, coding theory, automated theorem provers |
| 1 | Giampaolo Bella, Lawrence C. Paulson |
Mechanising BAN Kerberos by the Inductive Method. |
CAV |
1998 |
DBLP DOI BibTeX RDF |
|
| 1 | Giampaolo Bella, Lawrence C. Paulson |
Kerberos Version 4: Inductive Analysis of the Secrecy Goals. |
ESORICS |
1998 |
DBLP DOI BibTeX RDF |
secure key, non-expired timestamp, inductive method, machine proof, secrecy |
| 1 | Lawrence C. Paulson |
Mechanizing Coinduction and Corecursion in Higher-Order Logic. |
J. Log. Comput. |
1997 |
DBLP DOI BibTeX RDF |
|
| 1 | Lawrence C. Paulson |
Mechanizing Coinduction and Corecursion in Higher-order Logic |
CoRR |
1997 |
DBLP BibTeX RDF |
|
| 1 | Lawrence C. Paulson |
Generic Automatic Proof Tools |
CoRR |
1997 |
DBLP BibTeX RDF |
|
| 1 | Lawrence C. Paulson |
Mechanized proofs for a recursive authentication protocol. |
CSFW |
1997 |
DBLP DOI BibTeX RDF |
mechanized proofs, recursive authentication protocol, inductive approach, message nesting, basic security theorem, adjacent pairs, honest agents, protocol complexity, agents, protocols, specification, symmetry, mutual authentication, Isabelle/HOL, session keys |
| 1 | Lawrence C. Paulson |
Proving Properties of Security Protocols by Induction. |
CSFW |
1997 |
DBLP DOI BibTeX RDF |
|
| 1 | Lawrence C. Paulson, Krzysztof Grabczewski |
Mechanizing Set Theory: Cardinal Arithmetic and the Axiom of Choice. |
CoRR |
1996 |
DBLP BibTeX RDF |
|
| 1 | Lawrence C. Paulson, Krzysztof Grabczewski |
Mechanizing Set Theory. |
J. Autom. Reasoning |
1996 |
DBLP DOI BibTeX RDF |
|
| 1 | Lawrence C. Paulson |
ML for the working programmer (2. ed.). |
|
1996 |
RDF |
|
| 1 | Lawrence C. Paulson |
Set Theory for Verification. II: Induction and Recursion. |
J. Autom. Reasoning |
1995 |
DBLP DOI BibTeX RDF |
|
| 1 | Lawrence C. Paulson |
Isabelle - A Generic Theorem Prover (with a contribution by T. Nipkow) |
|
1994 |
DOI RDF |
|
| 1 | Lawrence C. Paulson |
A Fixedpoint Approach to Implementing (Co)Inductive Definitions. |
CADE |
1994 |
DBLP DOI BibTeX RDF |
|
| 1 | Lawrence C. Paulson |
A Concrete Final Coalgebra Theorem for ZF Set Theory. |
TYPES |
1994 |
DBLP DOI BibTeX RDF |
|
| 1 | Lawrence C. Paulson |
Natural Deduction as Higher-Order Resolution |
CoRR |
1993 |
DBLP BibTeX RDF |
|
| 1 | Lawrence C. Paulson |
Set Theory for Verification: I. From Foundations to Functions |
CoRR |
1993 |
DBLP BibTeX RDF |
|
| 1 | Lawrence C. Paulson |
Constructing Recursion Operators in Intuitionistic Type Theory |
CoRR |
1993 |
DBLP BibTeX RDF |
|
| 1 | Lawrence C. Paulson |
Designing a Theorem Prover |
CoRR |
1993 |
DBLP BibTeX RDF |
|
| 1 | Lawrence C. Paulson, Andrew W. Smith |
Logic Programming, Functional Programming, and Inductive Definitions |
CoRR |
1993 |
DBLP BibTeX RDF |
|
| 1 | Lawrence C. Paulson |
Verifying the Unification Algorithm in LCF |
CoRR |
1993 |
DBLP BibTeX RDF |
|
| 1 | Lawrence C. Paulson |
A Formulation of the Simple Theory of Types (for Isabelle) |
CoRR |
1993 |
DBLP BibTeX RDF |
|
| 1 | Lawrence C. Paulson |
The Foundation of a Generic Theorem Prover |
CoRR |
1993 |
DBLP BibTeX RDF |
|
| 1 | Lawrence C. Paulson |
A Higher-Order Implementation of Rewriting |
CoRR |
1993 |
DBLP BibTeX RDF |
|
| 1 | Lawrence C. Paulson |
Proving Termination of Normalization Functions for Conditional Expressions |
CoRR |
1993 |
DBLP BibTeX RDF |
|
| 1 | Lawrence C. Paulson |
Isabelle: The Next 700 Theorem Provers |
CoRR |
1993 |
DBLP BibTeX RDF |
|
| 1 | Lawrence C. Paulson |
Set Theory for Verification: I. From Foundations to Functions. |
J. Autom. Reasoning |
1993 |
DBLP DOI BibTeX RDF |
|
| 1 | Tobias Nipkow, Lawrence C. Paulson |
Isabelle-91. |
CADE |
1992 |
DBLP DOI BibTeX RDF |
|
| 1 | Lawrence C. Paulson |
ML for the working programmer. |
|
1991 |
RDF |
|
| 1 | Lawrence C. Paulson |
The Foundation of a Generic Theorem Prover. |
J. Autom. Reasoning |
1989 |
DBLP DOI BibTeX RDF |
|
| 1 | Lawrence C. Paulson, Andrew W. Smith |
Logic Programming, Functional Programming, and Inductive Definitions. |
ELP |
1989 |
DBLP DOI BibTeX RDF |
|
| 1 | Lawrence C. Paulson |
Isabelle: The Next Seven Hundred Theorem Provers. |
CADE |
1988 |
DBLP DOI BibTeX RDF |
|
| 1 | Lawrence C. Paulson |
A formulation of the simple theory of types (for Isabelle). |
Conference on Computer Logic |
1988 |
DBLP DOI BibTeX RDF |
|
| 1 | Lawrence C. Paulson |
Natural Deduction as Higher-Order Resolution. |
J. Log. Program. |
1986 |
DBLP DOI BibTeX RDF |
|
![[Valid RSS]](Pics/valid-rss.png "Validate my RSS feed")