Prof. Tobias Nipkow, Ph.D.

Professur

Logik und Verifikation in der Informatik
Professor im Ruhestand seit 31.03.2024

Wissenschaftliche Laufbahn und Forschungsgebiete

Prof. Nipkow (*1958) arbeitet auf dem Gebiet der Logik in der Informatik. Seine Schwerpunkte sind interaktives und automatisches Theorembeweisen, Programmiersprachensematik, Typsysteme und funktionale Programmierung. An seinem Lehrstuhl wird der interaktive Beweisassistent Isabelle entwickelt.

Prof. Nipkow erwarb 1982 sein Diplom (MSc) in Informatik an der Technischen Hochschule Darmstadt und promovierte 1987 an der University of Manchester. Nach Forschungsaufenthalten am MIT (1987-1989) und an der Universität Cambridge (1989-1992) wurde er 1992 als Professor für Programmiertheorie an die TUM berufen. Seit 2011 ist er Inhaber des Lehrstuhls für Logik und Verifikation an der TUM.

Hales T, Adams M, Bauer G, Dang TD, ...: "A formal proof of the Kepler conjecture". Forum of Mathematics, Pi. 2017; 5: e2.

Abstract

Nipkow T, Klein G: Concrete Semantics. Springer International Publishing, 2014.

Abstract

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