!!Tobias Nipkow - Selected Publications
\\
__Books:__\\
\\
Franz Baader and Tobias Nipkow. Term Rewriting and All That. Cambridge University Press, 1998. 301 pp.\\
\\
Tobias Nipkow, Lawrence Paulson, and Markus Wenzel. Isabelle/HOL - A Proof Assistant for Higher-Order Logic. LNCS 2283 Springer, 2002. 218 pp.\\
\\
Tobias Nipkow and Gerwin Klein. Concrete Semantics with Isabelle/HOL. Springer, 2014. 298 pp.\\
\\
Tobias Nipkow, Jasmin Blanchette, Manuel Eberl, Alejandro Gomez-Londono, Peter Lammich, Christian Sternagel, Simon Wimmer, and Bohua Zhan. Functional Algorithms, Verified! 2021. 276 pp.\\
\\
Published online at [https://functional-algorithms-verified.org].\\
\\
__Conference and journal publications:__\\
\\
Tobias Nipkow. Higher-order critical pairs. IEEE Symp. Logic in Computer Science, 342–349, 1991\\
\\
Gerwin Klein, and Tobias Nipkow. A machine-checked model for a Java-like language, virtual machine, and compiler.\\
ACM Transactions on Programming Languages and Systems (TOPLAS) 28 (4), 619-695, 2006\\
\\
Thomas Hales and 21 co-authors, incl. Tobias Nipkow. A formal proof of the Kepler conjecture.\\
Forum of mathematics, 2017\\
\\
Makarius Wenzel and Lawrence Paulson and Tobias Nipkow. The Isabelle framework.\\
Theorem Proving in Higher Order Logics, 33-38, LNCS 5170, Springer, 2008.\\
\\
J Esparza, P Lammich, R Neumann, T Nipkow, A Schimpf, JG Smaus. A fully verified executable LTL model checker.\\
Computer Aided Verification, 463-478, LNCS 8044, Springer, 2013\\
\\
Ursula Martin and Tobias Nipkow. Boolean unification.\\
Journal of Symbolic Computation 7 (3-4), 275-293, 1989