Computer Laboratory in Cambridge

King's College
King's College, Cambridge

Isabelle Developers Workshop

17 and 18 June in Cambridge, UK


The Isabelle Developers Workshop will be held in Cambridge this year. Like the last one in Munich, 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 and the latest developments around Isabelle. We like to reach out to new people to help them to become part of the Isabelle developer community.

There is no registration fee for this workshop. If you want to participate, please let me know as soon as possible (email: urbanc at in tum de).


The workshop will take place in the Computer Laboratory in Cambridge (location). The room is FW11 on the first floor inside the "public" part of the Computer Laboratory. There will be signs leading the way.


There is free wifi in the Computer Lab. The network name is wgb.


We will hand out some files during the workshop. The release candidate of Isabelle is available here. Although incomplete, you might find the Isabelle Programming Tutorial (draft) helpful.


Larry Paulson University of Cambridge, UK
Christian Urban TU Munich, Germany

Confirmed Participants

Stefan Berghofer TU Munich, Germany
Jasmin Blanchette TU Munich, Germany
Achim Brucker SAP, Germany
Abdou Feliachi Univ. Paris Sud, France
Holger Gast University of Tübingen, Germany
Bogdan Grechuk University of Edinburgh, UK
Gudmund Grov University of Edinburgh, UK
Cezary Kaliszyk TU Munich, Germany
Matthias Krieger LRI / Univ. Paris Sud, France
Andreas Lochbihler KIT Karlsruhe, Germany
Magnus Myreen University of Cambridge, UK
Walther Neuper TU Graz, Austria
Omar Montano Rivas University of Edinburgh, UK
Jaroslav Sevcik University of Cambridge, UK
Thomas Sewell NICTA, Australia
Christian Sternagel University of Innsbruck, Austria
Nik Sultana University of Cambridge, UK
Rene Thiemann University of Innsbruck, Austria
Matej Urbas University of Cambridge, UK
Viktor Vafeiadis University of Cambridge, UK
Tjark Weber University of Cambridge, UK
Makarius Wenzel LRI / Univ. Paris Sud, France
Burkhart Wolff LRI / Univ. Paris Sud, France


Wednesday, June 16
For anybody who is present, we will meet at 5 o'clock in the afternoon in the Eagle Pub (8 Benet St, Cambridge CB2 3QN; location). This pub is in a side street not far from King's College.
Thursday, June 17
  • 9:30 - 10:30 Isabelle Programming Introduction I (Makarius Wenzel / Christian Urban) [T01_Intro.thy]
  • 11:00 - 12:00 Isabelle Programming Introduction II (Jasmin Blanchette / Christian Urban) [T02_Intro.thy]
  • 14:00 - 15:00 Tactics and Conversions (Christian Urban / Stefan Berghofer) [T03_Tactics.thy]
  • 15:30 - 16:30 Contexts and Local Theories (Makarius Wenzel) [T04_Contexts.thy]
  • 17:00 - 18:00 Contributed Talks: I3P for Developers: How to Represent Your Tool in the UI (Holger Gast) [slides], HOL-Boogie - An Interactive Verification Backend for VCC (Burkhart Wolff), [slides1, slides2]
Friday, June 18
  • 9:30 - 10:30 Parsing and Methods (Stefan Berghofer) [T05_Methods.thy]
  • 11:00 - 12:00 ML and Scala (Makarius Wenzel) [T06_System.thy]
  • 14:00 - 15:00 Isabelle and LaTeX (Christian Urban) [T07_Latex.thy, T07_Latex.tex, slides]
  • 15:30 - 16:30 Contributed Talks: Monad Syntax (Christian Sternagel) [Monad_Syntax.thy, HG repository, slides], Encoding Object-oriented Datatypes in HOL: Extensible Records Revisited (Achim Brucker)
  • 17:00 - 17:30 Contributed Talk: HOL-TestGen - A Testcase Generation Environment (Burkhart Wolff) [slides]
If there is interest, Nik Sultana will show after the workshop the highlights of Cambridge in a tourist tour.

Accommodation, Travelling etc

Some information about accommodation in Cambridge is available here. There are two convenient options for travelling to Cambridge from continental Europe: one is by Eurostar and train from London; the other is via plane to London Stansted and by train or bus from there.

Last modified: Wed Jul 21 11:46:56 CEST 2010 [Validate this page.]