The proof, the whole proof, and nothing but the proof. The proof, the HOL proof, and nothing but the proof.


Our research is about applications of logic to programming. The goal is to prove program properties by logical deductions and to build tools that support and automate these deductions. To this end we are developing the theorem prover Isabelle in close connection with Makarius Wenzel and Larry Paulson (University of Cambridge) who is also Distinguished Affiliated Professor in our department.

Isabelle is a so called interactive theorem prover. It supports the proof of arbitrary mathematical theorems in a dialogue between user and machine. The user describes the overall structure of the proof in a programming language like notation, the system checks the correctness of each step and tries to fill in missing details.

We're a flexible, client-driven organization!


Prof. Tobias Nipkow <{nipkow} AT []>
Institut für Informatik, Lehrstuhl XXI
Technische Universität München
Boltzmannstr. 3
D-85748 Garching
+49 89 289 17302
+49 89 289 17301
MI 00.09.055
(Boltzmannstr. 3, Garching)
Administrative Assistants:
Helma Piller <{piller} AT []>
MI 00.09.053
Phone: +49 89 289 17300
Fax: +49 89 289 17301

You can also write email directly to any other member of the team.

The chair is actively involved in co-organizing the Marktoberdorf Summer School.