Isabelle Users Workshop 2012

Call for Papers

This informal workshop is intended to bring together Isabelle users and developers. Participants are invited to present their research and projects, including applications of Isabelle, internal developments, add-on tools, etc. Well-argued position papers (e.g. describing proposed extensions) are also welcome, and reports on work in progress.

Please submit a paper (or extended abstract) of up to 20 pages. These will be reviewed informally and accepted papers will form part of the programme. Time permitting, the workshop will include demonstrations or briefings by the development team. There will also be opportunities to discuss issues of interest to the Isabelle community.

Papers should be submitted (in PDF) using EasyChair. No formal proceedings will be published, but accepted papers will be available on the workshop website.

Draft Timetable

SESSION 1, 13:45-15:15
13:45-14:15 Christian Sternagel: Getting Started with Isabelle/jEdit
14:15-14:45 Brian Huffman, Ondřej Kunčar: Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
14:45-15:15 Christian Sternagel: A Locale for Minimal Bad Sequences
BREAK, 15:15-15:45
SESSION 2, 15:45-17:15
15:45-16:15 René Thiemann: Towards the Certification of Complexity Proofs
16:15-16:45 Ralph Romanos, Larry Paulson: Proving the impossibility of trisecting an angle and doubling the cube
16:45-17:15 Evgeny Dantsin, Jan-Georg Smaus and Sergei Soloviev: Algorithms in Games Evolving in Time: Winning Strategies Based on Testing
RECEPTION, 18:00-?


Tobias Nipkow, Larry Paulson and Makarius Wenzel