Isabelle/HOL: a proof assistant for higher-order logic T Nipkow, M Wenzel, LC Paulson Springer Berlin Heidelberg, 2002 | 4932 | 2002 |
Isabelle: A generic theorem prover LC Paulson Springer Berlin Heidelberg, 1994 | 2035 | 1994 |
ML for the Working Programmer LC Paulson Cambridge University Press, 1996 | 1386 | 1996 |
The inductive approach to verifying cryptographic protocols LC Paulson Journal of computer security 6 (1-2), 85-128, 1998 | 1326 | 1998 |
The foundation of a generic theorem prover LC Paulson Journal of Automated Reasoning 5, 363-397, 1989 | 632 | 1989 |
Logic and computation: interactive proof with Cambridge LCF LC Paulson Cambridge University Press, 1987 | 609 | 1987 |
Isabelle: The next 700 theorem provers LC Paulson Logic and computer science 31, 361-386, 1990 | 469 | 1990 |
Proving properties of security protocols by induction LC Paulson Proceedings 10th Computer Security Foundations Workshop, 70-83, 1997 | 423 | 1997 |
Metitarski: Past and future LC Paulson International Conference on Interactive Theorem Proving, 1-10, 2012 | 366 | 2012 |
Inductive analysis of the internet protocol TLS LC Paulson ACM Transactions on Information and System Security (TISSEC) 2 (3), 332-351, 1999 | 361 | 1999 |
Extending Sledgehammer with SMT solvers JC Blanchette, S Böhme, LC Paulson Journal of automated reasoning 51 (1), 109-128, 2013 | 308 | 2013 |
Natural deduction as higher-order resolution LC Paulson The Journal of Logic Programming 3 (3), 237-258, 1986 | 249 | 1986 |
The isabelle framework M Wenzel, LC Paulson, T Nipkow Theorem Proving in Higher Order Logics: 21st International Conference …, 2008 | 223 | 2008 |
Hammering towards QED JC Blanchette, C Kaliszyk, LC Paulson, J Urban Journal of Formalized Reasoning 9 (1), 101-148, 2016 | 216 | 2016 |
The Isabelle reference manual LC Paulson University of Cambridge, Computer Laboratory, 1993 | 204 | 1993 |
Kerberos version IV: Inductive analysis of the secrecy goals G Bella, LC Paulson Computer Security—ESORICS 98: 5th European Symposium on Research in …, 1998 | 194 | 1998 |
Mechanized proofs for a recursive authentication protocol LC Paulson Proceedings 10th Computer Security Foundations Workshop, 84-94, 1997 | 193 | 1997 |
Should your specification language be typed L Lamport, LC Paulson ACM Transactions on Programming Languages and Systems (TOPLAS) 21 (3), 502-526, 1999 | 191 | 1999 |
MetiTarski: An automatic theorem prover for real-valued special functions B Akbarpour, LC Paulson Journal of Automated Reasoning 44 (3), 175-205, 2010 | 161 | 2010 |
Translating higher-order clauses to first-order clauses J Meng, LC Paulson Journal of Automated Reasoning 40, 35-60, 2008 | 161 | 2008 |