A Practical Introduction to Theorem Proving with Isabelle/HOL

21-23 August 2015 in Nanjing, preceding ITP 2015

You would like to learn how to use the proof assistant Isabelle/HOL? This intensive 3-day tutorial is aimed both at theorem proving novices and at people already familiar with another proof assistant who want to learn about Isabelle. The tutorial consists of a mixture of interactive lectures and hands-on lab sessions where the participants solve theorem proving problems with Isabelle. The following material is covered: The tutorial (given by Tobias Nipkow) will be based on Part I of the book Concrete Semantics that is freely availble online (and is also available as this separate document). Participants should bring their own laptops with Isabelle already installed on it (or share with a fellow student - the latter is encouraged for the practical exercises.)

This tutorial can also serve as a pre-ITP introduction to the field of interactive theorem proving for novices.