Isabelle Short Course

Date: Thursday 2nd May and Friday 3rd May 2013
Time:
9:30 to 17:00
Venue: Appleton Tower, Edinburgh, room AT 4.12

The aim is to give participants a working knowledge of formal specifications and proofs in the Isabelle theorem prover. There will be presentations by the instructors, with interactive examples and exercises for the participants on their own laptops (min. 2 cores and 2 GB RAM).
The course is over two days:

  • The first day targets beginners with no or little experience with theorem provers. Some basic acquaintance with logic, proofs, or functional programming (ML, Haskell) will be helpful.
  • The second day continues at a more advanced level. Users of other proof assistants may jump in here, but people are welcome to attend both days.

The target audience are researchers and doctoral students who want to learn about Isabelle, specifications in HOL, structured proofs in Isar, integration of interactive and automated reasoning etc.

The course is sponsored by EPSRC grant EP/J001058: The Integration and Interaction for Multiple Mathematical Reasoning Processes and will be free to attend.

Instructors

Preliminary Schedule

Here is a preliminary schedule which will be updated closer to the date of the course. Minor changes to the start/end times for each session are also possible.

Thursday May 2nd, 2013

    9:30  - 11:00 : session 1
    11:00 - 11:30 : coffee/tea break
    11:30 - 13:00 : session 2
    13:00 - 13:45 : lunch
    13:45 - 15:15 : session 3
    15:15 - 15:45 : coffee/tea break
    15:45 - 17:00 : session 4

Friday May 3rd, 2013

    9:30  - 11:00 : session 5
    11:00 - 11:30 : coffee/tea break
    11:30 - 13:00 : session 6
    13:00 - 14:00 : lunch
    14:00 - 15:00 : session 7
    15:00 - 15:30 : coffee/tea break
    15:30 - 17:00 : session 8 

Confirmed participants

Thu / Fri  Gabrielle Anderson, University of Aberdeen
Thu / Fri  Chris Banks, University of Edinburgh
Thu / Fri  Evgenij Belikov, Heriot-Watt University
Thu / Fri  Brian Campbell, University of Edinburgh
Thu / Fri  Colin Farquhar, Heriot-Watt University
Thu        Leo Freitas, Newcastle University
Thu        Lilia Georgieva, Heriot-Watt University
Thu / Fri  Jonathan Heras, University of Dundee
Thu / Fri  Alexei Iliasov, Newcastle University
Thu / Fri  Paul Jackson, University of Edinburgh
        Fri   Ben Kavanagh, University of Edinburgh
Thu / Fri  Ekaterina Komendantskaya, University of Dundee
Thu        Anthony Widjaja Lin, Oxford University
Thu / Fri  Yuhui Lin, University of Edinburgh
Thu / Fri  Hans-Wolfgang Loidl, Heriot-Watt University
Thu        Yu Lu, University of Glasgow
Thu        David Matthews, Prolingua Ltd
Thu / Fri  Iain McGinniss, University of Glasgow
Thu / Fri  James McKinna, University of Edinburgh
Thu / Fri  Dulani Meedeniya, University of St-Andrews
Thu / Fri  Rajiv Murali, Heriot-Watt University
Thu / Fri  John Pirie, Heriot-Watt University
Thu / Fri  Daniel Raggi, University of Edinburgh
Thu / Fri  Prabhat Totoo, Heriot-Watt University
Thu / Fri  Patrick Totzke, University of Edinburgh

System installation

  • Get Isabelle2013 from the official website. Please ignore any mentioning of Proof General / Emacs, as we are using Isabelle/jEdit in the tutorial. It can be started via the main Isabelle executable or via isabelle jedit on the command line (for Windows this is the Cygwin Terminal).

  • Quick start example: open Seq.thy via Isabelle/jEdit. The screenshot shows the situation after activating the Output and Sidekick panels, and hovering with the mouse over the occurrence of Seq in the text, while holding CONTROL (on Linux/Windows) or COMMAND (on Mac OS X) to make the tooltip window appear.

Course materials

Further documentation