Isabelle Course Material

• Semantics via Isabelle, Tobias Nipkow, 15 weeks with two 90 minute lectures per week

  This is an MSc course on Semantics via Isabelle based on the Concrete Semantics book.

• Functional Data Structures, Tobias Nipkow, 15 weeks with one 90 minute lecture per week

  This is a course about functional data structures using Isabelle, based on material in the Functional Algorithms, Verified! book.

• Isabelle/HOL + Isar course, Christian Sternagel, 4 sessions of 3 hours

  This course is loosely based on Tobias Nipkow’s courses but avoids apply-style and concentrates on Isar.

• ACF: Software Formal Analysis and Design, Thomas Genet, 6 lectures and 10 lab sessions

  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 lecture notes are (almost) in English, the lab notes are in French. 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.