Isabelle Tutorial at CADE-25

(See also updated version with more details.)

A full-day tutorial on Isabelle is scheduled as associated event of the 25th International Conference on Automated Deduction (CADE-25), which will take place in Berlin at the start of August 2015.

More than 25 years ago, Isabelle was initiated by Larry Paulson as a logical framework for rapid prototyping of Natural-Deduction proof systems. Today, Isabelle is one of the major platforms for Interactive Theorem Proving (ITP), with notable support for automated reasoning tools (ATPs and SMTs). Isabelle/HOL is the main environment for applications; it is accompanied by the Archive of Formal Proofs (AFP) as repository for user-contributions. Isabelle supports logical tool development in Isabelle/ML and Isabelle/Scala, but it is also possible to connect external tools; this works routinely on Linux, Windows, and Mac OS X. The system presents itself to the end-user by an advanced Prover IDE: Isabelle/jEdit.

The purpose of the tutorial is to help participants to get acquainted with Isabelle: topics will cover specifications in HOL, proofs in Isar, use of automated provers via Sledgehammer etc. The target audience are doctoral students or researchers with an interest in formalized reasoning, application of reasoning tools for interactive and automated proof development, maybe even with an interest to develop their own tools with/for Isabelle.

There will be presentations by myself and one or two colleagues, with hands-on tutoring and exercises done by the participants on their own computers (with at least 2 cores and 4 GB memory).

Further organizational details will emerge sooner or later, as summer 2015 approaches. Watch this space, as well as the main CADE-25 website.