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

    • Aspects of Isabelle (Slides)

    • Makarius material

      • ML.thy

        • Notepad.thy, Calculation.thy, Predicate_Logic.thy

        • ex1: Curry.thy, De_Morgan_Pred.thy, De_Morgan_Prop.thy, Frobenius.thy, Principia_Mathematica.thy

        • Natural_Deduction.thy, Induction.thy

        • ex2: Closure.thy, Parentheses.thy

    • Gudmund material

      • Non_Empty_List.thy (session 2)

        • solution: Non_Empty_List_sol.thy

        • Non_Empty_List_Sledge.thy (for session 8)

      • Compiler case study (session 4)

        • (Partial) solutions (least complete version first): Compiler0.thy, Compiler1.thy, Compiler2.thy, Compiler3.thy

        • Solution: Compiler.thy

      • Disproof.thy (session 8)

    • Grant material

    • TrySledgehammer.thy

    • slides

    • Synopsis of Isabelle/Isar proof language elements.

    • Specifications in Isabelle/HOL.

    • Compact overview of Isabelle/HOL Main library.

    • The extremely dense Isabelle/Isar quick reference card.

Further documentation