Follow
Lawrence Paulson
Title
Cited by
Cited by
Year
Isabelle/HOL: a proof assistant for higher-order logic
T Nipkow, M Wenzel, LC Paulson
Springer Berlin Heidelberg, 2002
46772002
Isabelle: A generic theorem prover
LC Paulson
Springer Berlin Heidelberg, 1994
2400*1994
ML for the Working Programmer
LC Paulson, LC Paulson
Cambridge University Press, 1996
13701996
The inductive approach to verifying cryptographic protocols
LC Paulson
Journal of computer security 6 (1-2), 85-128, 1998
13071998
The foundation of a generic theorem prover
LC Paulson
Journal of Automated Reasoning 5, 363-397, 1989
6161989
Logic and computation: interactive proof with Cambridge LCF
LC Paulson
Cambridge University Press, 1987
5951987
Proving properties of security protocols by induction
LC Paulson
Proceedings 10th Computer Security Foundations Workshop, 70-83, 1997
4171997
Inductive analysis of the internet protocol TLS
LC Paulson
ACM Transactions on Information and System Security (TISSEC) 2 (3), 332-351, 1999
3481999
Metitarski: Past and future
LC Paulson
Interactive Theorem Proving: Third International Conference, ITP 2012 …, 2012
3192012
Extending Sledgehammer with SMT solvers
JC Blanchette, S Böhme, LC Paulson
Journal of automated reasoning 51 (1), 109-128, 2013
2902013
Natural deduction as higher-order resolution
LC Paulson
The Journal of Logic Programming 3 (3), 237-258, 1986
2291986
The isabelle framework
M Wenzel, LC Paulson, T Nipkow
Theorem Proving in Higher Order Logics: 21st International Conference …, 2008
1992008
The Isabelle reference manual
LC Paulson
University of Cambridge, Computer Laboratory, 1993
1971993
Hammering towards QED
JC Blanchette, C Kaliszyk, LC Paulson, J Urban
Journal of Formalized Reasoning 9 (1), 101-148, 2016
1912016
Kerberos version IV: Inductive analysis of the secrecy goals
G Bella, LC Paulson
Lecture notes in computer science 1485, 361-376, 1998
1911998
Mechanized proofs for a recursive authentication protocol
LC Paulson
Proceedings 10th Computer Security Foundations Workshop, 84-94, 1997
1901997
Should your specification language be typed
L Lamport, LC Paulson
ACM Transactions on Programming Languages and Systems (TOPLAS) 21 (3), 502-526, 1999
1821999
A higher-order implementation of rewriting
LC Paulson
arXiv preprint cs/9301108, 2001
1642001
Translating higher-order clauses to first-order clauses
J Meng, LC Paulson
Journal of Automated Reasoning 40, 35-60, 2008
1622008
LEO-II-a cooperative automatic theorem prover for classical higher-order logic (system description)
C Benzmüller, LC Paulson, F Theiss, A Fietzke
Automated Reasoning: 4th International Joint Conference, IJCAR 2008 Sydney …, 2008
1532008
The system can't perform the operation now. Try again later.
Articles 1–20