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

Isabelle Developers Workshop

13 - 15 August in Munich,

affiliated with TPHOLs 2009



The Nominal Group is organising the Isabelle Developers Workshop in 2009. The workshop is very much meant to be an informal meeting where developers can talk to developers. It is also a place where you can learn about Isabelle programming.

There is no registration for this workshop. If you want to participate, please let me know (email: urbanc at in tum de). Please let me also know which projects you are working on and which parts of Isabelle you are interested in.


The workshop will take place at the Campus Garching of the TU Munich. Details about travelling are below:

Confirmed Participants

Maksym Bortin DFKI, Germany
Burkhart Wolff LRI, France
Jeremy Dawson Australian National University, Australia
Lucas Dixon Edinburgh University, United Kingdom (only 13th and 14th)
Cameron Freer MIT, USA
Gerwin Klein NICTA, Australia
Peter Homeier Department of Defense, USA
Brian Huffman Portland State University, USA
Cezary Kaliszyk Radboud University, Netherlands
Rafal Kolanski NICTA, Australia
Yongjian Li Chinese Academy of Sciences, China
Christoph Lüth DFKI, Germany
Walther Neuper TU Graz, Austria
Gabriel Dos Reis Texas A&M University, USA
Christian Sternagel University of Innsbruck, Austria
Nik Sultana University of Cambridge, UK
Denis Walter DFKI, Germany
Stefan Berghofer TU Munich, Germany
Jasmin Blanchette TU Munich, Germany
Sascha Böhme TU Munich, Germany
Lukas Bulwahn TU Munich, Germany
Florian Haftmann TU Munich, Germany
Johannes Hölzl TU Munich, Germany
Fabian Immler TU Munich, Germany
Alexander Krauss TU Munich, Germany
Markus Wenzel TU Munich, Germany
Christian Urban TU Munich, Germany


A detailed schedule is here: [pdf]
Thursday, August 13
  • 9:15 - 9:30 Short Intro [slides]
  • 9:30 - 10:15 Florian Haftmann: Isabelle/ML, Fundamental Isabelle Types, Antiquotations, Passing States, Accumulating Results, Name Space [thy1]
  • 10:30 - 11:15 Makarius Wenzel: Proof Methods [slides] [Ex1] [Ex2]
  • 11:45 - 12:30 Christian Urban: Tactics and Generic Proof Procedures [slides] [Ex]
  • 14:30 - 15:15 Sascha Böhme: Parsing and New Commands [Calc.thy] [Method.thy]
Friday, August 14
Saturday, August 15

Last modified: Sun Aug 16 12:54:19 CEST 2009 [Validate this page.]