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)
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.Abstract
Nipkow T, Paulson L, Wenzel M: Isabelle/HOL. A proof assistant for higher-order logic. Springer, 2002.Abstract
Baader F, Nipkow T: Term Rewriting and All That. Cambridge: Cambridge University Press, 1998.Abstract
Nipkow T: “Higher-order critical pairs. Proceedings 6th IEEE Symposium Logic in Computer Science. 1991; 342-349.Abstract
Nipkow T: “Unification in primal algebras, their powers and their varieties”. Journal of the ACM. 1990; 37: 742-776.Abstract