The Isabelle Workshop 2007
Thanks to Stefan Berghofer some photos from the Isabelle'07 workshop can be see here: http://www.in.tum.de/~berghofe/misc/isabelle07/index.html
is a popular generic theorem proving environment developed at
Cambridge University and TU
Munich. Developments in Isabelle are diverse and include ongoing
work in formalised mathematics, software verification, proof planning,
decision procedures and structured languages for proof representation
This workshop aims to provides an overview of ongoing developments in Isabelle for both researchers interested in knowing more about the system as well Isabelle's developers and users. With the increasing use of the system and its combination of many automated deduction techniques, it is important to foster collaboration between different researchers. For the developers of Isabelle, meeting users is an important part of focusing development of the system. The workshop will also provide a forum to discuss new technologies and to see a wide range of applications for automated reasoning. Discussion of formal theory developments also gives a chance to share knowledge and encourage improvements to the underlying proof tools and definitional machinery. Most formalisations in Isabelle's are in Higher-Order Logic, but we also encourage discussion of developments in other logics.
|Abstract submission:||28 May 2007|
|Acceptance notification:||5 June 2007|
|Early registration for attendance (via CADE):||10 June 2007|
|Final version due:||20 June 2007|
|Workshop:||16th of July 2007|
Authors are invited to submit abstracts for presentation at the workshop. These can concern finished work or work in progress and the length is up to the author. There will be a programme of short talks and demonstrations. A bound collection of abstracts will be circulated to participants and made available online. Submissions should be made via EasyChair http://www.easychair.org/ISABELLE2007/. To make the printed workshop proceedings consistent in style, please use the this latex template, or if you do not use latex, please make it look like this pdf, using an 11pt Time-Roman font. Although there will be no formal refereeing, if a large number of abstracts are received we may change the format so that some speakers give shorter talks. If you have any questions concerning submissions, please contact Moa Johansson.
The last Isabelle Users Workshop (1995) was a long time ago. This received 18 submissions. The intention is to start a regular workshop for Isabelle users.
You can also download the PDF containing the abstracts from all the talks. A printed copy of this will be handed out at CADE registration to workshop participants.
|9:40-10:40||Local proofs, local theories, and local everything||Makarius Wenzel (Invited Talk!)|
|10:40-11:00||Practical Proof Reconstruction for First-order Logic and Set-Theoretical Constructions||Clément Hurlin, Amine Chaieb, Pascal Fontaine, Stephan Merz and Tjark Weber|
|11:30-11:50||Translating from Haskell to Isabelle||Paolo Torrini, Christoph Lüth, Christian Maeder and Till Mossakowski|
|11:50-12:10||Checking XML-Specifications||Harald Hiss|
|12:10-12:30||Introducing Proof General Eclipse||David Aspinall and Christoph Lüth||12:30-14:00||LUNCH|
|14:00-14:20||Overview of Locales||Clemens Ballarin|
|14:20-14:50||Defining Recursive Functions in Isabelle/HOL 2007||Alexander Krauss|
|14:50-15:10||Nominal datatypes in Isabelle/HOL||Stefan Berghofer|
|15:10-15:30||Proof Critics for IsaPlanner||Moa Johansson|
|16:00-16:20||Concurrent/Distributed theorem proving in Isabelle/IsaPlanner||Priya Gopalan|
|16:20-16:40||Integration of local and reflective proof-procedures||Amine Chaieb|
|19:30....||CADE Welcome Reception @ Jacobs Faculty Club|