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