Marienplatz (city centre)

Englischer Garten
The English Garden

Chinesischer Turm
Chinese Tower (famous beer garden)

Computer science building
The Computer Science building of the TUM

Main hall of the computer science building
The main hall in the CS-building

The river Isar
The Isar river

The conference poster

TPHOLs will be in Munich from 17 to 20 August 2009


TPHOLs is a series of international conferences that started in 1988 and brings together researchers working in all areas of interactive theorem proving. The Theorem Proving Group at the Technische Universität München is pleased to host the 22nd TPHOLs.
[Important Dates] [Committees] [Venue] [Programme] [Workshops] [Local Information] [Hotel Booking] [Our Sponsors] [History]

Pictures of the conference are now available

Important Dates

Submission for main proceedings: Now closed.
Submission for the emerging trends: Now closed.
Registration: Now closed
Conference: 17-20 August 2009

Committees and Invited Speakers

Invited Speakers:
David Basin ETH Zurich, Switzerland title/abstract
John Harrison Intel, USA title/abstract
Wolfram Schulte  Microsoft Research, USA
Invited Tutorials about/by:
Twelf Carsten Schürmann
HOL Light  John Harrison
Agda Ulf Norell
Mizar Adam Naumowicz
Programme Committee:
Thorsten Altenkirch Nottingham University, United Kingdom
David Aspinall Edinburgh University, United Kingdom
Jeremy Avigad Carnegie Mellon University, USA
Gilles Barthe IMDEA, Spain
Christoph Benzmüller Saarland University, Germany
Peter Dybjer Chalmers University, Sweden
Jean-Christophe Filliâtre CNRS, France
Georges Gonthier Microsoft Research, United Kingdom
Mike Gordon Cambridge University, United Kingdom
Jim Grundy Intel, USA
Reiner Hähnle Chalmers University, Sweden
Joe Hurd Galois, USA
Gerwin Klein NICTA, Australia
Xavier Leroy INRIA, France
Pete Manolios Northeastern University, USA
César Muñoz NASA, USA
Tobias Nipkow (co-chair) TU München, Germany
Michael Norrish NICTA, Australia
Sam Owre SRI International, USA
Larry Paulson Cambridge University, United Kingdom
Frank Pfenning Carnegie Mellon University, USA
Randy Pollack Edinburgh University, United Kingdom
Sofiène Tahar Concordia University, Canada
Laurent Théry INRIA, France
Christian Urban (co-chair)  TU München, Germany
Freek Wiedijk Radboud University Nijmegen, The Netherlands
Workshop Chair:
Makarius Wenzel
Local Organisation:
Tobias Nipkow, Makarius Wenzel, Stefan Berghofer, Christian Urban


The LNCS number of the proceedings will be 5674. You can find the accepted papers here. The programme is elsewhere. If you are an author and prepare your slides, please note that the contributed talks in the main conference are limited to 25 minutes (including time for questions). The talks in the poster session are limited to 7 minutes. The proceedings of the poster session is here.


Venue and Travelling

The conference will take place in the Novotel which is near the river Isar and close to the city centre. There are a number of beer gardens near the hotel.

Local Information

Munich is situated at the heart of Europe.

Munich's airport is an important European hub for international flights from around the world.

Novotel is close to the central station and in easy reach from the airport by public transportation. More detailed local information can be downloaded for

  • the main conference and the workshops on August 21 [pdf]
  • the Isabelle Developers Workshop on August 13 - 15 [pdf]

Hotel Booking

The registration deadline for the conference has passed. You can still book your hotel:

Our Sponsors

We are very grateful for the support provided by:

Last modified: Wed Oct 21 17:59:37 CEST 2009 [Validate this page.]