IJCAR 2004 - Tutorial

Clemens Ballarin

Gerwin Klein

Time and Location: 5 July 2004, Cork, Ireland. Part of IJCAR-2004.

Overview:
This one-day tutorial gives an overview of the state-of-the-art proof assistant Isabelle and its use. The tutorial aims at researchers in computer science and mathematics who want to use Isabelle for a particular formalisation task, or who want to get an overview of current proof assistant technology. The following themes will be covered: introduction to natural deduction, specification tools, automated proof tools, readable proofs, Isabelle's module system, applications from verification and mathematical algebra. The tutorial is limited to 20 participants.

Larry Paulson will be present at one of the sessions and will be ready to address any questions about Isabelle and its development you might have.

Programme:
The tutorial will comprise four lectures, each followd by sessions where participants work with Isabelle. Isabelle supports various logics including Higher-Order Logic (HOL) and Zermelo-Fraenkel Set Theory (ZF). The tutorial is based on HOL, but most of the presented material also applies to ZF.

• Session I: Basics
  A brief introduction to Isabelle's basic calculus of natural deduction is followed by Isabelle's general automation for classical proofs and term rewriting. This session will also cover essential technicalities needed to get started with Isabelle.
• Session II: Specification Tools & Readable Proofs
  Strong proof tools do not automatically make a proof assistant an effective tool for specification and verification. What is needed is support for routine specification tasks. Isabelle supports datatypes, general recursive functions and inductive definitions. An other important issue is readability of proofs. Since a specification of a device or the formalisation of a mathematical entity typically evolves over time, proofs change and proof scripts must be maintainable. Isabelle supports this through the ISAR proof format.
• Session III: More Readable Proofs & Modules
  The more advanced concepts of ISAR include calculational reasoning chains and derived operators that make writing proofs more convenient. Another tool for managing maintenance complexity and readability is the module system. Unlike other provers where modules are centered around theories, Isabelle's modules (called locales) are based on contexts. These can be seen as light-weight theories and, since they are key to ISAR, they can be interpreted not only at the level of theories, but within proofs, providing much finer granularity. Besides interpretation, locales provide operations for rename and merge.
• Session IV: Applications
  We will present two medium sized applications of readable proofs in Isabelle from the areas of verification (a small expression compiler) and mathematical algebra (universal property of polynomial rings).

Target audience:
Doctoral students and researchers in computer science or mathematics who want to use Isabelle for a particular formalisation task, or who want to get an overview of the capabilities of a state-of-the-art proof assistant. Standard mathematical knowledge but no previous experience with formal methods is required. The number of participants is limited to 20.

Registration:
Registration is through the IJCAR web page. Note that tutorial participants are not required to register for the full conference.

Location and Accommodation:
See IJCAR web page [http://4c.ucc.ie/ijcar/site.html].