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
45382002
Isabelle: A generic theorem prover
LC Paulson
Springer Berlin Heidelberg, 1994
2349*1994
ML for the Working Programmer
LC Paulson, LC Paulson
Cambridge University Press, 1996
13541996
The inductive approach to verifying cryptographic protocols
LC Paulson
Journal of computer security 6 (1-2), 85-128, 1998
12911998
The foundation of a generic theorem prover
LC Paulson
Journal of Automated Reasoning 5 (3), 363-397, 1989
5981989
Logic and computation: interactive proof with Cambridge LCF
LC Paulson
Cambridge University Press, 1990
5791990
Proving properties of security protocols by induction
LC Paulson
Proceedings 10th Computer Security Foundations Workshop, 70-83, 1997
4141997
Inductive analysis of the internet protocol TLS
LC Paulson
ACM Transactions on Information and System Security (TISSEC) 2 (3), 332-351, 1999
3451999
Metitarski: Past and future
LC Paulson
International Conference on Interactive Theorem Proving, 1-10, 2012
3022012
Natural deduction as higher-order resolution
LC Paulson
The Journal of Logic Programming 3 (3), 237-258, 1986
2221986
The Isabelle reference manual
LC Paulson
University of Cambridge, Computer Laboratory, 1993
1951993
Kerberos version IV: Inductive analysis of the secrecy goals
G Bella, LC Paulson
European Symposium on Research in Computer Security, 361-375, 1998
1911998
The isabelle framework
M Wenzel, LC Paulson, T Nipkow
International Conference on Theorem Proving in Higher Order Logics, 33-38, 2008
1892008
Mechanized proofs for a recursive authentication protocol
LC Paulson
Proceedings 10th Computer Security Foundations Workshop, 84-94, 1997
1871997
Should your specification language be typed
L Lamport, LC Paulson
ACM Transactions on Programming Languages and Systems (TOPLAS) 21 (3), 502-526, 1999
1811999
Hammering towards QED
JC Blanchette, C Kaliszyk, LC Paulson, J Urban
Journal of Formalized Reasoning 9 (1), 101-148, 2016
1802016
A higher-order implementation of rewriting
LC Paulson
arXiv preprint cs/9301108, 2001
1632001
Translating higher-order clauses to first-order clauses
J Meng, LC Paulson
Journal of Automated Reasoning 40 (1), 35-60, 2008
1602008
Extending Sledgehammer with SMT solvers
JC Blanchette, S Böhme, LC Paulson
Journal of automated reasoning 51 (1), 109-128, 2013
1582013
LEO-II-a cooperative automatic theorem prover for classical higher-order logic (system description)
C Benzmüller, LC Paulson, F Theiss, A Fietzke
International Joint Conference on Automated Reasoning, 162-170, 2008
1522008
The system can't perform the operation now. Try again later.
Articles 1–20