Marienplatz (city centre)
The English Garden
Chinese Tower (famous beer garden)
The Computer Science building of the TUM
The main hall in the CS-building
The Isar river
Isabelle Developers Workshop13 - 15 August in Munich,affiliated with TPHOLs 2009 |
 |
Programme
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.
Venue
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 |
Schedule
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
- 9:15 - 10:00 Stefan Berghofer: Simplifier / Simprocs / Conversions [theory]
- 10:30 - 11:15 Makarius Wenzel: Proof Contexts [slides] [Ex3] [Ex4]
- 11:45 - 12:30 Makarius Wenzel: Local Theories [slides] [Ex5] [Ex6]
- 14:30 - 15:15 Stefan Berghofer: How to write a Definitional Package for Isabelle? [slides | construction | internals | package code | theory for loading package | examples | Emacs keyword file]
Saturday, August 15
- 9:15 - 10:00 Alexander Krauss: Mercurial [slides] [hgrc] [session]
- 10:30 - 11:15 Fabian Immler: Sledgehammer / Threads / External Processes [slides] [thy]
- 11:45 - 12:30 Makarius Wenzel: Isabelle/Scala System Programming
[slides]
[ex.scala]
For this tutorial, please have installed the Java 1.6 runtime environment (for Linux) or the official version for MacOSX by Apple; and also Scala 2.7.5 final. - 14:30 - 15:15 Christian Urban LaTeX-Hacking with Isabelle [slides]