342.291, KV Special Topics, Mathias Fleury, 2020W

This course is a self-contained introduction to the proof assistant Isabelle/HOL. It is based on the first part of the book by Prof. Tobias Nipkow and Prof. Gerwin Klein, which is available both as a free PDF online and as a hardcover from Springer. Several exercise will be about reasoning on first order and propositional logic.

Proof assistants are tools that allow its users to carry out mathematical proofs rigorously, based on a logical foundation. Developing a proof in a proof assistant as opposed to using pen and paper is roughly the equivalent of programming on a computer as opposed to sketching pseudo-code on paper. Expertise with proof assistants is becoming an increasingly important skill, especially for software verification, which aims at proving the absence of bugs in programs. In the experience of many instructors, the use of a proof assistant helps students get a good grip on computer science topics.

Coq and Isabelle are the main two proof assistants in use. Isabelle's strength is that it is simple as 1-2-3: It offers (1) a simple yet powerful logic, (2) a convenient user interface, and (3) a lot of proof automation.

There are no formal prerequisites for taking the course. Familiarity with a typed functional programming language (such as Standard ML, OCaml, Haskell, or F#) is highly recommended.


Good reasons to not do this course:
  • theorem proving is too addictive for you;
  • you want to trust you own paper proofs;
  • you never understood how induction works.

The course corresponds roughly to the first part of another course I have taught with Sophie Tourret last year, with a different focus. That course itself is based on a course with Jasmin Blanchette and Daniel Wand, and that in turn is based on course given at TUM by Tobias Nipkow.


Depending how far we go and how interested you are, we might go into program refinement and try to produce (parts of ) a fully verified DPLL SAT solver in the line of this work (i.e., a less complicated version of IsaSAT).


UPDATE: The university has presented the COVID rules. Only 20 stundents are allowed to be in the room we are currently scheduled in. Unless too many student register, teaching will happen as follows: if the `ampel' is green or yellow, no remote. Otherwise (or if masks become mandatory in the rooms), teaching will be purely remote (no hybrid).