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.
Makarius Wenzel (Univ. Paris-Sud, LRI)
Gudmund Grov (Heriot-Watt University)
Grant Passmore (University of Edinburgh)
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.
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
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
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
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.
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.
The Isabelle Framework — extended abstract and overview of main literature (2008).
The bulky Isabelle/Isar reference manual.
Some tutorial on Isabelle/HOL.
How to prove it: overview of common informal techniques.