Persönlicher Status und Werkzeuge

Prof. Tobias Nipkow, Ph.D.



Contact Details

Visitenkarte in TUMonline

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)

Klein 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.


Nipkow T, Paulson L, Wenzel M: Isabelle/HOL. A proof assistant for higher-order logic. Springer, 2002.


Baader F, Nipkow T: Term Rewriting and All That. Cambridge: Cambridge University Press, 1998.


Nipkow T: “Higher-order critical pairs. Proceedings 6th IEEE Symposium Logic in Computer Science. 1991; 342-349.


Nipkow T: “Unification in primal algebras, their powers and their varieties”. Journal of the ACM. 1990; 37: 742-776.