Prof. Tobias Nipkow, Ph.D.
Academic Career and Research Areas
Prof. Nipkow (*1958) works in the area of logic in computer science. He focuses on interactive and automatic theorem proving, programming language sematics, type systems and functional programming. His chair is developing the interactive proof assistant Isabelle.
Prof. Nipkow received his Diplom (MSc) in Informatik from the Technische Hochschule Darmstadt in 1982 and his PhD from the University of Manchester in 1987. Having held research positions at MIT (1987-1989) and Cambridge University (1989-1992), he was appointed Professor for the Theory of Programming at TUM in 1992. Since 2011 he has held the chair of Logic and Verification at TUM.
Key Publications (all publications)
Hales T, Adams M, Bauer G, Dang TD, ...: "A formal proof of the Kepler conjecture". Forum of Mathematics, Pi. 2017; 5: e2.
AbstractNipkow T, Klein G: Concrete Semantics. Springer International Publishing, 2014.
AbstractKlein G, Nipkow T: “A machine-checked model for a java-like language, virtual machine and compiler”. ACM Transactions on Programming Languages and Systems. 2006; 28: 619-695.
AbstractNipkow T, Paulson L, Wenzel M: Isabelle/HOL. A proof assistant for higher-order logic. Springer, 2002.
AbstractBaader F, Nipkow T: Term Rewriting and All That. Cambridge: Cambridge University Press, 1998.
Abstract