Lawrence Paulson
TitoloCitata daAnno
Isabelle/HOL: a proof assistant for higher-order logic
T Nipkow, LC Paulson, M Wenzel
Springer Science & Business Media, 2002
34852002
Isabelle: A generic theorem prover
LC Paulson
Springer Science & Business Media, 1994
2144*1994
ML for the Working Programmer
LC Paulson, LC Paulson
Cambridge University Press, 1996
12611996
The inductive approach to verifying cryptographic protocols
LC Paulson
Journal of computer security 6 (1-2), 85-128, 1998
12001998
Logic and computation: interactive proof with Cambridge LCF
LC Paulson
Cambridge University Press, 1990
5631990
The foundation of a generic theorem prover
LC Paulson
Journal of Automated Reasoning 5 (3), 363-397, 1989
5211989
Proving properties of security protocols by induction
LC Paulson
Proceedings 10th Computer Security Foundations Workshop, 70-83, 1997
3861997
Inductive analysis of the Internet protocol TLS
LC Paulson
ACM Transactions on Information and System Security (TISSEC) 2 (3), 332-351, 1999
3021999
Metitarski: Past and future
LC Paulson
International Conference on Interactive Theorem Proving, 1-10, 2012
2152012
Natural deduction as higher-order resolution
LC Paulson
The Journal of Logic Programming 3 (3), 237-258, 1986
2041986
The Isabelle reference manual
LC Paulson
University of Cambridge, Computer Laboratory, 1993
1871993
Kerberos version IV: Inductive analysis of the secrecy goals
G Bella, LC Paulson
European Symposium on Research in Computer Security, 361-375, 1998
1801998
Mechanized proofs for a recursive authentication protocol
LC Paulson
Proceedings 10th Computer Security Foundations Workshop, 84-94, 1997
1771997
A higher-order implementation of rewriting
LC Paulson
arXiv preprint cs/9301108, 2001
1512001
Should your specification language be typed
L Lamport, LC Paulson
ACM Transactions on Programming Languages and Systems (TOPLAS) 21 (3), 502-526, 1999
1451999
Translating higher-order clauses to first-order clauses
J Meng, LC Paulson
Journal of Automated Reasoning 40 (1), 35-60, 2008
142*2008
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
1362008
Set theory for verification: I. From foundations to functions
LC Paulson
Journal of Automated Reasoning 11 (3), 353-389, 1993
1301993
The isabelle framework
M Wenzel, LC Paulson, T Nipkow
International Conference on Theorem Proving in Higher Order Logics, 33-38, 2008
1272008
MetiTarski: An automatic theorem prover for real-valued special functions
B Akbarpour, LC Paulson
Journal of Automated Reasoning 44 (3), 175-205, 2010
1222010
Il sistema al momento non può eseguire l'operazione. Riprova più tardi.
Articoli 1–20