Lawrence C. Paulson

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

Coauthor Index

1	Behzad Akbarpour	[92] [98] [101] [102] [104] [106]
2	Clemens Ballarin	[47] [51]
3	Bernhard Beckert	[89]
4	Giampaolo Bella	[43] [44] [59] [61] [65] [67] [69] [73] [75] [76] [77] [80] [83] [86]
5	Christoph Benzmüller (Christoph Benzmueller)	[96] [100] [103]
6	Jasmin Christian Blanchette	[108]
7	Sascha Böhme	[108]
8	William Denman	[102]
9	Sidi O. Ehmety	[70] [81]
10	Arnaud Fietzke	[96]
11	Jacques D. Fleuriot	[45] [46]
12	Krzysztof Grabczewski	[32] [33]
13	Florian Kammüller	[50] [54]
14	Matt Kaufmann	[107]
15	Gerwin Klein	[90]
16	Leslie Lamport	[52]
17	Cristiano Longo	[76] [77]
18	Fabio Massacci	[59] [61] [73] [75] [80] [83]
19	Jia Meng	[79] [84] [85] [90] [93] [99]
20	Rajeev Narayanan	[106]
21	Tobias Nipkow	[15] [74] [82] [94] [95]
22	Claire Quigley	[84] [85]
23	Andrew W. Smith	[13] [19]
24	Kong Woei Susanto	[91]
25	Sofiène Tahar	[102] [106]
26	Frank Theiss	[96]
27	Piero Tramontano	[59] [61]
28	Markus Wenzel (Makarius Wenzel)	[54] [74] [88] [95]
29	Mohamed H. Zaki	[102] [106]

Colors in the list of coauthors

Last update Fri May 25 01:42:58 2012 CET by the DBLP Team — Data released under the ODC-BY 1.0 license — See also our legal information page