Computer Laboratory in Cambridge
King's College, Cambridge
Isabelle Developers Workshop17 and 18 June in Cambridge, UK |
Programme
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).
Venue
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.Wifi
There is free wifi in the Computer Lab. The network name is wgb.Material
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.Organisers
| 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 |
Schedule
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]