Course Material

This page contains slides, demos, exercises, and other material for a growing number of courses on the theorem prover Isabelle. It is meant as a resource for people who would like to learn Isabelle as well as for those who would like to teach it.

• Semantics via Isabelle, Tobias Nipkow
  This is an MSc course on Semantics via Isabelle, 15 weeks with two 90 minutes lectures per week. The first 4 weeks (approx. seven 90 minutes lectures) introduce Isabelle based on the tutorial Programming and Proving in Isabelle/HOL.
• Exercises
  This is a collection of exercises for getting acquainted with the proof assistant Isabelle/HOL. The individual exercises come out of an annual Isabelle/HOL lab course taught at the TU München.
• Isabelle/HOL course, Tobias Nipkow, 8 sessions of 90min
  This course is loosely based on the material in Isabelle/HOL - A Proof Assistant for Higher-Order Logic.
• Full day tutorial, Clemens Ballarin and Gerwin Klein, 4 sessions of 90min
  This course is suitable for a conference tutorial. It covers basic Isabelle, structured Isar proofs, and locales and was presented by the authors at IJCAR'04.
• Isabelle/HOL + Isar course, Christian Sternagel, 4 sessions of 3h
  This is the course materials for a blocked Isabelle course that Christian Sternagel held in Innsbruck several times. The course is loosely based on Tobias Nipkow's course and the Tutorial but avoids apply-style and concentrates on Isar.
• ACF: Software Formal Analysis and Design, Thomas Genet, 6 lectures and 10 lab sessions
  The lecture notes are (almost) in english, the lab notes are in french. This course focuses on functional programming (Isabelle/HOL and Scala), first order logic (for defining program properties) and on counterexample finding (rather than on proof). The final objective is to run Java+Scala programs with verified blocks, i.e. whose formally defined properties have been checked on the Isabelle theory using counterexample finders.
• Isabelle Primer for Mathematicians, Bogdan Grechuk
  This is a quick introduction to the Isabelle/HOL proof assistant, aimed at mathematicians who would like to use it for the formalization of mathematical results.