Isabelle/HOL: a proof assistant for higher-order logic T Nipkow, M Wenzel, LC Paulson Springer-Verlag, 2002 | 5006 | 2002 |
Term rewriting and all that F Baader, T Nipkow Cambridge University Press, 1998 | 4221 | 1998 |
A formal proof of the Kepler conjecture T Hales, M Adams, G Bauer, TD Dang, J Harrison, H Le Truong, ... Forum of mathematics, Pi 5, e2, 2017 | 462 | 2017 |
Higher-order critical pairs T Nipkow University of Cambridge, Computer Laboratory, 1991 | 410 | 1991 |
A machine-checked model for a Java-like language, virtual machine, and compiler G Klein, T Nipkow ACM Transactions on Programming Languages and Systems (TOPLAS) 28 (4), 619-695, 2006 | 370 | 2006 |
Nitpick: A counterexample generator for higher-order logic based on a relational model finder J Blanchette, T Nipkow Interactive Theorem Proving, 131-146, 2010 | 345 | 2010 |
A revision of the proof of the Kepler conjecture TC Hales, J Harrison, S McLaughlin, T Nipkow, S Obua, R Zumkeller The Kepler Conjecture, 341-376, 2011 | 337* | 2011 |
Code generation via higher-order rewrite systems F Haftmann, T Nipkow Functional and Logic Programming, 103-117, 2010 | 322* | 2010 |
Concrete semantics: with Isabelle/HOL T Nipkow, G Klein Springer International Publishing, 2014 | 319* | 2014 |
Higher-order rewrite systems and their confluence R Mayr, T Nipkow Theoretical Computer Science 192 (1), 3-29, 1998 | 273 | 1998 |
Java light is type-safe—definitely T Nipkow, D Von Oheimb Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of …, 1998 | 270 | 1998 |
The isabelle framework M Wenzel, L Paulson, T Nipkow Theorem Proving in Higher Order Logics, 33-38, 2008 | 229 | 2008 |
Sledgehammer: judgement day S Böhme, T Nipkow Automated Reasoning, 107-121, 2010 | 186 | 2010 |
Functional unification of higher-order patterns T Nipkow [1993] Proceedings Eighth Annual IEEE Symposium on Logic in Computer Science …, 1993 | 181 | 1993 |
Machine-checking the Java specification: Proving type-safety D Von Oheimb, T Nipkow Formal Syntax and Semantics of Java, 1998 | 151* | 1998 |
microJava: Embedding a Programming Language in a Theorem Prover C Pusch, T Nipkow, D von Oheimb Foundations of Secure Computation, IOS Press, 2000 | 150* | 2000 |
Boolean unification-the story so far U Martin, T Nipkow Journal of Symbolic Computation 7 (3-4), 275-293, 1989 | 144 | 1989 |
Verified bytecode verifiers G Klein, T Nipkow Theoretical Computer Science 298 (3), 583-626, 2003 | 141 | 2003 |
Automatic proof and disproof in Isabelle/HOL JC Blanchette, L Bulwahn, T Nipkow Frontiers of Combining Systems: 8th International Symposium, FroCoS 2011 …, 2011 | 139 | 2011 |
Structured proofs in Isar/HOL T Nipkow Types for Proofs and Programs, 619-620, 2003 | 139* | 2003 |