dblp.uni-trier.dewww.uni-trier.de

Lawrence C. Paulson Vis

List of publications from the DBLP Bibliography Server - FAQ
Coauthor Index - Ask others: ACM DL/Guide - CiteSeerX - CSB - MetaPress - Google - Bing - Yahoo
Home Page

*2009
97EEBehzad Akbarpour, Lawrence C. Paulson: Applications of MetiTarski in the Verification of Control and Hybrid Systems. HSCC 2009: 1-15
96EEChristoph Benzmüller, Lawrence C. Paulson: Quantified Multimodal Logics in Simple Type Theory CoRR abs/0905.2435: (2009)
95EEJia Meng, Lawrence C. Paulson: Lightweight relevance filtering for machine-generated resolution problems. J. Applied Logic 7(1): 41-57 (2009)
2008
94EEBehzad Akbarpour, Lawrence C. Paulson: MetiTarski: An Automatic Prover for the Elementary Functions. AISC/MKM/Calculemus 2008: 217-231
93EELawrence C. Paulson: The Relative Consistency of the Axiom of Choice - Mechanized Using Isabelle/ZF. CiE 2008: 486-490
92EEChristoph 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
91EEMakarius Wenzel, Lawrence C. Paulson, Tobias Nipkow: The Isabelle Framework. TPHOLs 2008: 33-38
90EEJia Meng, Lawrence C. Paulson: Translating Higher-Order Clauses to First-Order Clauses. J. Autom. Reasoning 40(1): 35-60 (2008)
2007
89EEBehzad Akbarpour, Lawrence C. Paulson: Extending a Resolution Prover for Inequalities on Elementary Functions. LPAR 2007: 47-61
88EELawrence C. Paulson, Kong Woei Susanto: Source-Level Proof Reconstruction for Interactive Theorem Proving. TPHOLs 2007: 232-245
87EEJia Meng, Lawrence C. Paulson, Gerwin Klein: A Termination Checker for Isabelle Hoare Logic. VERIFY 2007
86EEBernhard Beckert, Lawrence C. Paulson: Preface. J. Autom. Reasoning 38(1-3): 1-2 (2007)
2006
85EEMarkus Wenzel, Lawrence C. Paulson: Isabelle/Isar. The Seventeen Provers of the World 2006: 41-49
84EELawrence C. Paulson: Defining functions on equivalence classes. ACM Trans. Comput. Log. 7(4): 658-675 (2006)
83EEGiampaolo Bella, Lawrence C. Paulson: Accountability protocols: Formalized and verified. ACM Trans. Inf. Syst. Secur. 9(2): 138-161 (2006)
82EEJia Meng, Claire Quigley, Lawrence C. Paulson: Automation for interactive proof: First prototype. Inf. Comput. 204(10): 1575-1596 (2006)
81EEJia 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)
80EEGiampaolo Bella, Fabio Massacci, Lawrence C. Paulson: Verifying the SET Purchase Protocols. J. Autom. Reasoning 36(1-2): 5-37 (2006)
2005
79EETobias Nipkow, Lawrence C. Paulson: Proof Pearl: Defining Functions over Finite Sets. TPHOLs 2005: 385-396
78EESidi O. Ehmety, Lawrence C. Paulson: Mechanizing compositional reasoning for concurrent systems: some lessons. Formal Asp. Comput. 17(1): 58-68 (2005)
77EEGiampaolo Bella, Fabio Massacci, Lawrence C. Paulson: An overview of the verification of SET. Int. J. Inf. Sec. 4(1-2): 17-28 (2005)
2004
76EEJia Meng, Lawrence C. Paulson: Experiments on Supporting Interactive Proof Using Resolution. IJCAR 2004: 372-384
75EELawrence C. Paulson: Organizing Numerical Theories Using Axiomatic Type Classes. J. Autom. Reasoning 33(1): 29-49 (2004)
2003
74EEGiampaolo Bella, Cristiano Longo, Lawrence C. Paulson: Is the Verification Problem for Cryptographic Protocols Solved?. Security Protocols Workshop 2003: 183-189
73EEGiampaolo 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
71EEGiampaolo 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
70EELawrence C. Paulson: The Reflection Theorem: A Study in Meta-theoretic Reasoning. CADE 2002: 377-391
69EELawrence C. Paulson: Verifying the SET Protocol: Overview. FASec 2002: 4-14
68EESidi O. Ehmety, Lawrence C. Paulson: Program Composition in Isabelle/UNITY. IPDPS 2002
67EEGiampaolo Bella, Lawrence C. Paulson: Analyzing Delegation Properties. Security Protocols Workshop 2002: 120-127
2001
66EELawrence C. Paulson: SET Cardholder Registration: The Secrecy Proofs. IJCAR 2001: 5-12
65EEGiampaolo Bella, Lawrence C. Paulson: A Proof of Non-repudiation. Security Protocols Workshop 2001: 119-125
64EELawrence C. Paulson: A Proof of Non-repudiation (Transcript of Discussion). Security Protocols Workshop 2001: 126-133
63EEGiampaolo Bella, Lawrence C. Paulson: Mechanical Proofs about a Non-repudiation Protocol. TPHOLs 2001: 91-104
62EELawrence 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)
60EELawrence C. Paulson: A Simple Formalization and Proof for the Mutilated Chess Board. Logic Journal of the IGPL 9(3): (2001)
2000
59EEGiampaolo 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
57EEGiampaolo Bella, Fabio Massacci, Lawrence C. Paulson, Piero Tramontano: Making Sense of Specifications: The Formalization of SET. Security Protocols Workshop 2000: 74-81
56EELawrence C. Paulson: Making Sense of Specifications: The Formalization of SET (Transcript of Discussion). Security Protocols Workshop 2000: 82-86
55EELawrence C. Paulson: Mechanizing UNITY in Isabelle. ACM Trans. Comput. Log. 1(1): 3-32 (2000)
1999
54EELawrence 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
52EEFlorian Kammüller, Markus Wenzel, Lawrence C. Paulson: Locales - A Sectioning Concept for Isabelle. TPHOLs 1999: 149-166
51EELawrence C. Paulson: Inductive Analysis of the Internet Protocol TLS. ACM Trans. Inf. Syst. Secur. 2(3): 332-351 (1999)
50EELeslie 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)
47EELawrence 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
45EEClemens Ballarin, Lawrence C. Paulson: Reasoning About Coding Theory: The Benefits We Get from Computer Algebra. AISC 1998: 55-66
44EEJacques D. Fleuriot, Lawrence C. Paulson: Proving Newton's Propositio Kepleriana Using Geometry and Nonstandard Analysis in Isabelle. Automated Deduction in Geometry 1998: 47-66
43EEJacques D. Fleuriot, Lawrence C. Paulson: A Combination of Nonstandard Analysis and Geometry Theorem Proving, with Application to Newton's Principia. CADE 1998: 3-16
42EEGiampaolo Bella, Lawrence C. Paulson: Mechanising BAN Kerberos by the Inductive Method. CAV 1998: 416-427
41EEGiampaolo Bella, Lawrence C. Paulson: Kerberos Version 4: Inductive Analysis of the Secrecy Goals. ESORICS 1998: 361-375
40EELawrence C. Paulson: Inductive Analysis of the Internet Protocol TLS (Position Paper). Security Protocols Workshop 1998: 1-12
39EELawrence 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
37EELawrence C. Paulson: Proving Properties of Security Protocols by Induction. CSFW 1997: 70-83
36EELawrence C. Paulson: Mechanized proofs for a recursive authentication protocol. CSFW 1997: 84-95
35EELawrence C. Paulson: Mechanizing Coinduction and Corecursion in Higher-order Logic CoRR cs.LO/9711105: (1997)
34EELawrence 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
32EELawrence 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
28EELawrence 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
26EELawrence C. Paulson: Verifying the Unification Algorithm in LCF CoRR cs.LO/9301101: (1993)
25EELawrence C. Paulson: Constructing Recursion Operators in Intuitionistic Type Theory CoRR cs.LO/9301102: (1993)
24EELawrence C. Paulson: Proving Termination of Normalization Functions for Conditional Expressions CoRR cs.LO/9301103: (1993)
23EELawrence C. Paulson: Natural Deduction as Higher-Order Resolution CoRR cs.LO/9301104: (1993)
22EELawrence C. Paulson: The Foundation of a Generic Theorem Prover CoRR cs.LO/9301105: (1993)
21EELawrence C. Paulson: Isabelle: The Next 700 Theorem Provers CoRR cs.LO/9301106: (1993)
20EELawrence C. Paulson: A Formulation of the Simple Theory of Types (for Isabelle) CoRR cs.LO/9301107: (1993)
19EELawrence C. Paulson: A Higher-Order Implementation of Rewriting CoRR cs.LO/9301108: (1993)
18EELawrence C. Paulson, Andrew W. Smith: Logic Programming, Functional Programming, and Inductive Definitions CoRR cs.LO/9301109: (1993)
17EELawrence C. Paulson: Designing a Theorem Prover CoRR cs.LO/9301110: (1993)
16EELawrence 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
14EETobias Nipkow, Lawrence C. Paulson: Isabelle-91. CADE 1992: 673-676
1989
13EELawrence 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
11EELawrence C. Paulson: Isabelle: The Next Seven Hundred Theorem Provers. CADE 1988: 772-773
10EELawrence 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

Coauthor Index

1Behzad Akbarpour [89] [94] [97]
2Clemens Ballarin [45] [49]
3Bernhard Beckert [86]
4Giampaolo Bella [41] [42] [57] [59] [63] [65] [67] [71] [73] [74] [77] [80] [83]
5Christoph Benzmüller (Christoph Benzmueller) [92] [96]
6Sidi O. Ehmety [68] [78]
7Arnaud Fietzke [92]
8Jacques D. Fleuriot [43] [44]
9Krzysztof Grabczewski [31] [32]
10Florian Kammüller [48] [52]
11Gerwin Klein [87]
12Leslie Lamport [50]
13Cristiano Longo [73] [74]
14Fabio Massacci [57] [59] [71] [77] [80]
15Jia Meng [76] [81] [82] [87] [90] [95]
16Tobias Nipkow [14] [72] [79] [91]
17Claire Quigley [81] [82]
18Andrew W. Smith [13] [18]
19Kong Woei Susanto [88]
20Frank Theiss [92]
21Piero Tramontano [57] [59]
22Markus Wenzel (Makarius Wenzel) [52] [72] [85] [91]

Colors in the list of coauthors

Copyright © Tue Nov 3 08:52:44 2009 by Michael Ley (ley@uni-trier.de)