-
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.